Euclidean composition algebras

A Euclidean composition algebra is a real vector space C carrying a unital, not necessarily associative or commutative, bilinear product, together with a symmetric positive-definite bilinear form B whose associated quadratic form N x = B x x is multiplicative: N (x * y) = N x * N y.

The four examples are ℝ, ℂ, ℍ, 𝕆 (Composition/Instances.lean), and Hurwitz's theorem says there are no others. This file is the ground floor: the class, and the identity toolkit that every later argument runs on.

Design

• The form is carried as a symmetric bilinear map B : C →ₗ[ℝ] C →ₗ[ℝ] ℝ rather than as a Mathlib QuadraticForm. Over ℝ the two are interchangeable (2 is invertible), and the substantive arguments below are polarisation arguments, i.e. are about the bilinear form. Carrying B directly removes an API layer from the middle of those proofs.
• The ambient algebra is [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C]: unital, distributive, ℝ-bilinear multiplication, no associativity and no commutativity. Algebra ℝ C is not usable here — it presupposes associativity.
• B is a class field. There is at most one composition-algebra structure of interest per carrier, so class inference is the right vehicle and it keeps ip/nf argument-inferred.

Main results

Everything below is derived from the four class fields alone.

• ip_mul_left_left, ip_mul_right_right, ip_exchange — the three polarisations of the composition law. ip_exchange is the workhorse: ⟪xy, wz⟫ + ⟪wy, xz⟫ = 2⟪x,w⟫⟪y,z⟫.
• ip_mul_adj_left, ip_mul_adj_right — conjugation is the adjoint of multiplication: ⟪xy, z⟫ = ⟪y, x* z⟫ and ⟪xy, z⟫ = ⟪x, z y*⟫.
• sq_eq — every element is quadratic: x * x = 2⟪x,1⟫ • x - N x • 1. This is the single most useful consequence; mul_cstar_self, cstar_mul_self and both alternativity laws come off it directly.
• cstar_mul — conjugation is an anti-automorphism.
• left_alternative, right_alternative — x (x y) = (x x) y and (y x) x = y (x x).
• pure_mul_pure_add — for x, y orthogonal to 1, x y + y x = -2⟪x,y⟫ • 1; in particular a unit imaginary squares to -1.

Scope

Substrate for the two Hurwitz theorems. It states neither of them.

class CompositionAlgebra (C : Type u) [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] : Type u

A Euclidean composition algebra: a unital, ℝ-bilinear, not necessarily associative product together with a symmetric positive-definite bilinear form whose quadratic form is multiplicative.

• B : C →ₗ[ℝ] C →ₗ[ℝ] ℝ

  The defining bilinear form.

• B_symm (x y : C) : (B x) y = (B y) x

  The form is symmetric.

• B_pos (x : C) : x ≠ 0 → 0 < (B x) x

  The form is positive definite.

• B_comp (x y : C) : (B (x * y)) (x * y) = (B x) x * (B y) y

  The composition law: the associated quadratic form is multiplicative.

def CompositionAlgebra.ip {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : ℝ

The inner product ⟪x, y⟫ of a composition algebra.

Equations

• CompositionAlgebra.ip x y = (CompositionAlgebra.B x) y

def CompositionAlgebra.nf {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : ℝ

The norm form N x = ⟪x, x⟫. Positive definite, and multiplicative by comp.

Equations

• CompositionAlgebra.nf x = (CompositionAlgebra.B x) x

theorem CompositionAlgebra.nf_eq_ip {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : nf x = ip x x

theorem CompositionAlgebra.ip_symm {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : ip x y = ip y x

@[simp]

theorem CompositionAlgebra.ip_add_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip (x + y) z = ip x z + ip y z

@[simp]

theorem CompositionAlgebra.ip_add_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip x (y + z) = ip x y + ip x z

@[simp]

theorem CompositionAlgebra.ip_sub_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip (x - y) z = ip x z - ip y z

@[simp]

theorem CompositionAlgebra.ip_sub_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip x (y - z) = ip x y - ip x z

@[simp]

theorem CompositionAlgebra.ip_smul_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (r : ℝ) (x y : C) : ip (r • x) y = r * ip x y

@[simp]

theorem CompositionAlgebra.ip_smul_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (r : ℝ) (x y : C) : ip x (r • y) = r * ip x y

@[simp]

theorem CompositionAlgebra.ip_zero_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (y : C) : ip 0 y = 0

@[simp]

theorem CompositionAlgebra.ip_zero_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : ip x 0 = 0

@[simp]

theorem CompositionAlgebra.ip_neg_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : ip (-x) y = -ip x y

@[simp]

theorem CompositionAlgebra.ip_neg_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : ip x (-y) = -ip x y

theorem CompositionAlgebra.nf_nonneg {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : 0 ≤ nf x

theorem CompositionAlgebra.nf_pos {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {x : C} (hx : x ≠ 0) : 0 < nf x

theorem CompositionAlgebra.nf_eq_zero_iff {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {x : C} : nf x = 0 ↔ x = 0

@[simp]

theorem CompositionAlgebra.nf_neg {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : nf (-x) = nf x

theorem CompositionAlgebra.nf_smul {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (r : ℝ) (x : C) : nf (r • x) = r ^ 2 * nf x

theorem CompositionAlgebra.nf_add {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : nf (x + y) = nf x + 2 * ip x y + nf y

theorem CompositionAlgebra.nf_sub {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : nf (x - y) = nf x - 2 * ip x y + nf y

theorem CompositionAlgebra.comp {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : nf (x * y) = nf x * nf y

The composition law, in nf form.

theorem CompositionAlgebra.eq_zero_of_ip_eq_zero {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {v : C} (h : ∀ (z : C), ip v z = 0) : v = 0

Positive definiteness as nondegeneracy.

theorem CompositionAlgebra.eq_of_ip_eq {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {u v : C} (h : ∀ (z : C), ip u z = ip v z) : u = v

The form separates points: this is how every identity below is proved.

The three polarisations of the composition law

theorem CompositionAlgebra.ip_mul_left_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip (x * y) (x * z) = nf x * ip y z

First polarisation: ⟪x y, x z⟫ = N x ⟪y, z⟫.

theorem CompositionAlgebra.ip_mul_right_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip (x * z) (y * z) = ip x y * nf z

Second polarisation: ⟪x z, y z⟫ = ⟪x, y⟫ N z.

theorem CompositionAlgebra.ip_exchange {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y w z : C) : ip (x * y) (w * z) + ip (w * y) (x * z) = 2 * ip x w * ip y z

Third polarisation (the exchange identity): ⟪x y, w z⟫ + ⟪w y, x z⟫ = 2 ⟪x, w⟫ ⟪y, z⟫.

Almost everything in this file is a specialisation of this one identity.

Conjugation

def CompositionAlgebra.cstar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : C

The conjugation x* = 2⟪x, 1⟫ • 1 - x, i.e. reflection in the line ℝ ∙ 1.

Equations

• CompositionAlgebra.cstar x = (2 * CompositionAlgebra.ip x 1) • 1 - x

theorem CompositionAlgebra.cstar_apply {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : cstar x = (2 * ip x 1) • 1 - x

theorem CompositionAlgebra.cstar_add {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : cstar (x + y) = cstar x + cstar y

theorem CompositionAlgebra.cstar_smul {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (r : ℝ) (x : C) : cstar (r • x) = r • cstar x

@[simp]

theorem CompositionAlgebra.cstar_zero {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] : cstar 0 = 0

theorem CompositionAlgebra.cstar_neg {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : cstar (-x) = -cstar x

theorem CompositionAlgebra.cstar_sub {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : cstar (x - y) = cstar x - cstar y

theorem CompositionAlgebra.nf_one {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] : nf 1 = 1

N 1 = 1: the unit is a unit vector.

@[simp]

theorem CompositionAlgebra.ip_one_one {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] : ip 1 1 = 1

@[simp]

theorem CompositionAlgebra.cstar_one {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] : cstar 1 = 1

theorem CompositionAlgebra.ip_cstar_one {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] (x : C) : ip (cstar x) 1 = ip x 1

@[simp]

theorem CompositionAlgebra.cstar_cstar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] (x : C) : cstar (cstar x) = x

theorem CompositionAlgebra.nf_cstar {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] (x : C) : nf (cstar x) = nf x

Conjugation is the adjoint of multiplication

theorem CompositionAlgebra.ip_mul_adj_left {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip (x * y) z = ip y (cstar x * z)

⟪x y, z⟫ = ⟪y, x* z⟫.

theorem CompositionAlgebra.ip_mul_adj_right {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y z : C) : ip (x * y) z = ip x (z * cstar y)

⟪x y, z⟫ = ⟪x, z y*⟫.

theorem CompositionAlgebra.ip_self_mul {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x z : C) : ip x (z * x) = ip 1 z * nf x

⟪x, z x⟫ = ⟪1, z⟫ N x.

theorem CompositionAlgebra.ip_mul_one {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : ip (x * y) 1 = 2 * ip x 1 * ip y 1 - ip x y

⟪x y, 1⟫ = 2⟪x,1⟫⟪y,1⟫ - ⟪x,y⟫: the real part of a product.

Every element is quadratic

theorem CompositionAlgebra.sq_eq {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : x * x = (2 * ip x 1) • x - nf x • 1

Every element of a composition algebra satisfies a real quadratic equation: x * x = 2⟪x, 1⟫ • x - N x • 1.

theorem CompositionAlgebra.mul_cstar_self {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : x * cstar x = nf x • 1

x x* = N x • 1.

theorem CompositionAlgebra.cstar_mul_self {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : cstar x * x = nf x • 1

x* x = N x • 1.

theorem CompositionAlgebra.mul_add_mul {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : x * y + y * x = (2 * ip x 1) • y + (2 * ip y 1) • x - (2 * ip x y) • 1

The polarised quadratic relation: x y + y x = 2⟪x,1⟫ • y + 2⟪y,1⟫ • x - 2⟪x,y⟫ • 1.

theorem CompositionAlgebra.cstar_mul {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : cstar (x * y) = cstar y * cstar x

Conjugation is an anti-automorphism: (x y)* = y* x*.

Alternativity

theorem CompositionAlgebra.left_alternative {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : x * (x * y) = x * x * y

Left alternativity: x (x y) = (x x) y.

theorem CompositionAlgebra.right_alternative {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x y : C) : y * x * x = y * (x * x)

Right alternativity: (y x) x = y (x x).

Imaginary elements

def CompositionAlgebra.IsPure {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : Prop

x is imaginary (pure) when it is orthogonal to the unit.

Equations

• CompositionAlgebra.IsPure x = (CompositionAlgebra.ip x 1 = 0)

theorem CompositionAlgebra.cstar_of_pure {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {x : C} (hx : IsPure x) : cstar x = -x

theorem CompositionAlgebra.sq_of_pure {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {x : C} (hx : IsPure x) : x * x = -nf x • 1

A pure element squares to a nonpositive real multiple of the unit.

theorem CompositionAlgebra.pure_mul_pure_add {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] {x y : C} (hx : IsPure x) (hy : IsPure y) : x * y + y * x = -(2 * ip x y) • 1

Two pure elements anticommute up to their inner product: x y + y x = -2⟪x, y⟫ • 1. This is the Clifford relation.

def CompositionAlgebra.impart {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : C

The imaginary part of x.

Equations

• CompositionAlgebra.impart x = x - CompositionAlgebra.ip x 1 • 1

theorem CompositionAlgebra.isPure_impart {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] [Nontrivial C] (x : C) : IsPure (impart x)

theorem CompositionAlgebra.impart_add_re {C : Type u} [NonAssocRing C] [Module ℝ C] [IsScalarTower ℝ C C] [SMulCommClass ℝ C C] [CompositionAlgebra C] (x : C) : ip x 1 • 1 + impart x = x