The Cayley–Dickson double as an external type former

Composition/Doubling.lean doubles inside a composition algebra C: given a composition subalgebra A ≤ C and a unit u ⊥ A, the submodule A ⊕ A u is again a composition subalgebra. That is all Hurwitz's dimension bound needs, and it is cheap because the composition law of C is already available.

The classification needs the other half: a functor D ↦ CD D producing a new algebra, so that the chain of subalgebras can be identified with concrete carriers rather than merely counted. This file builds it.

Main definitions

• CompositionAlgebra.CD D — the double D × D with (a,b)(c,d) = (a c - d* b, d a + b c*) and 1 = (1,0).
• CompositionAlgebra.CD.bilin — the form ⟪(a,b), (c,d)⟫ = ⟪a,c⟫ + ⟪b,d⟫.

Main results

• CD.instNonAssocRing, CD.instModule, and the two bilinearity classes — CD D is a bilinear unital ring over ℝ whenever D is.
• CD.instCompositionAlgebra — CD D is a Euclidean composition algebra when D is nontrivial and associative. Associativity is used exactly once, in the cross term of the composition law: expanding N((a,b)(c,d)) = N(a,b) N(c,d) leaves the residue ⟪d a, b c*⟫ = ⟪a c, d* b⟫, and the two adjoint identities turn each side into ⟪a, (d* b) c*⟫ and ⟪a, d* (b c*)⟫ respectively.

★ This is the same mechanism as IsCompSubalgebra.forced_assoc, read in the other direction: there, multiplicativity of the norm on A ⊕ A u is free (it is inherited from C) and forces A associative; here, D associative is a hypothesis and buys multiplicativity of the norm on the new type.

Note on the conjugation

CD is built over CompositionAlgebra D, whose conjugation cstar is derived from the form rather than supplied as a Star structure. An upstreamed version would take [Star D] and a StarRing hypothesis; here the derived conjugation keeps the four concrete instantiations free of bridging lemmas.

Scope

Substrate for the classification. The headline declaration is the instance CD.instCompositionAlgebra; the classification itself is Composition/Classification.lean.

def CompositionAlgebra.CD (D : Type u) : Type u

The Cayley–Dickson double of D: the module D × D with the product (a,b)(c,d) = (a c - d* b, d a + b c*) and unit (1,0).

Kept as a type synonym rather than a structure so that the additive and ℝ-module structure transfer from Prod verbatim; the product and the unit are the only new data.

Equations

• CompositionAlgebra.CD D = (D × D)

@[instance_reducible]

instance CompositionAlgebra.CD.instAddCommGroup {D : Type u} [NonAssocRing D] : AddCommGroup (CD D)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance CompositionAlgebra.CD.instModule {D : Type u} [NonAssocRing D] [Module ℝ D] : Module ℝ (CD D)

Equations

• CompositionAlgebra.CD.instModule = { smul := CompositionAlgebra.CD.instModule._aux_1, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

def CompositionAlgebra.CD.mk {D : Type u} (a b : D) : CD D

Assemble an element of the double from its two components.

Equations

• CompositionAlgebra.CD.mk a b = (a, b)

def CompositionAlgebra.CD.fst {D : Type u} (x : CD D) : D

The first component of an element of the double.

Equations

• x.fst = x.1

def CompositionAlgebra.CD.snd {D : Type u} (x : CD D) : D

The second component of an element of the double.

Equations

• x.snd = x.2

@[simp]

theorem CompositionAlgebra.CD.fst_mk {D : Type u} (a b : D) : (mk a b).fst = a

@[simp]

theorem CompositionAlgebra.CD.snd_mk {D : Type u} (a b : D) : (mk a b).snd = b

theorem CompositionAlgebra.CD.ext {D : Type u} {x y : CD D} (h1 : x.fst = y.fst) (h2 : x.snd = y.snd) : x = y

theorem CompositionAlgebra.CD.ext_iff {D : Type u} {x y : CD D} : x = y ↔ x.fst = y.fst ∧ x.snd = y.snd

@[simp]

theorem CompositionAlgebra.CD.fst_zero {D : Type u} [NonAssocRing D] : fst 0 = 0

@[simp]

theorem CompositionAlgebra.CD.snd_zero {D : Type u} [NonAssocRing D] : snd 0 = 0

@[simp]

theorem CompositionAlgebra.CD.fst_add {D : Type u} [NonAssocRing D] (x y : CD D) : (x + y).fst = x.fst + y.fst

@[simp]

theorem CompositionAlgebra.CD.snd_add {D : Type u} [NonAssocRing D] (x y : CD D) : (x + y).snd = x.snd + y.snd

@[simp]

theorem CompositionAlgebra.CD.fst_neg {D : Type u} [NonAssocRing D] (x : CD D) : (-x).fst = -x.fst

@[simp]

theorem CompositionAlgebra.CD.snd_neg {D : Type u} [NonAssocRing D] (x : CD D) : (-x).snd = -x.snd

@[simp]

theorem CompositionAlgebra.CD.fst_sub {D : Type u} [NonAssocRing D] (x y : CD D) : (x - y).fst = x.fst - y.fst

@[simp]

theorem CompositionAlgebra.CD.snd_sub {D : Type u} [NonAssocRing D] (x y : CD D) : (x - y).snd = x.snd - y.snd

@[simp]

theorem CompositionAlgebra.CD.fst_smul {D : Type u} [NonAssocRing D] [Module ℝ D] (r : ℝ) (x : CD D) : (r • x).fst = r • x.fst

@[simp]

theorem CompositionAlgebra.CD.snd_smul {D : Type u} [NonAssocRing D] [Module ℝ D] (r : ℝ) (x : CD D) : (r • x).snd = r • x.snd

@[instance_reducible]

instance CompositionAlgebra.CD.instOne {D : Type u} [NonAssocRing D] : One (CD D)

Equations

• CompositionAlgebra.CD.instOne = { one := CompositionAlgebra.CD.mk 1 0 }

@[simp]

theorem CompositionAlgebra.CD.fst_one {D : Type u} [NonAssocRing D] : fst 1 = 1

@[simp]

theorem CompositionAlgebra.CD.snd_one {D : Type u} [NonAssocRing D] : snd 1 = 0

@[instance_reducible]

instance CompositionAlgebra.CD.instMul {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] : Mul (CD D)

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CompositionAlgebra.CD.fst_mul {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (x y : CD D) : (x * y).fst = x.fst * y.fst - cstar y.snd * x.snd

@[simp]

theorem CompositionAlgebra.CD.snd_mul {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (x y : CD D) : (x * y).snd = y.snd * x.fst + x.snd * cstar y.fst

theorem CompositionAlgebra.CD.mul_def {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (a b c d : D) : mk a b * mk c d = mk (a * c - cstar d * b) (d * a + b * cstar c)

The ring structure

instance CompositionAlgebra.CD.instNontrivial {D : Type u} [NonAssocRing D] [Nontrivial D] : Nontrivial (CD D)

@[instance_reducible]

instance CompositionAlgebra.CD.instNonAssocRing {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] : NonAssocRing (CD D)

Equations

• One or more equations did not get rendered due to their size.

instance CompositionAlgebra.CD.instIsScalarTower {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] : IsScalarTower ℝ (CD D) (CD D)

instance CompositionAlgebra.CD.instSMulCommClass {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] : SMulCommClass ℝ (CD D) (CD D)

The form

def CompositionAlgebra.CD.bilin {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] : CD D →ₗ[ℝ] CD D →ₗ[ℝ] ℝ

The form of the double: ⟪(a,b), (c,d)⟫ = ⟪a,c⟫ + ⟪b,d⟫.

Equations

• CompositionAlgebra.CD.bilin = LinearMap.mk₂ ℝ (fun (x y : CompositionAlgebra.CD D) => CompositionAlgebra.ip x.fst y.fst + CompositionAlgebra.ip x.snd y.snd) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CompositionAlgebra.CD.bilin_apply {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (x y : CD D) : (bilin x) y = ip x.fst y.fst + ip x.snd y.snd

The composition law

Associativity of D enters exactly here, and exactly once: in cross.

theorem CompositionAlgebra.CD.cross {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] (hassoc : ∀ (p q r : D), p * q * r = p * (q * r)) (a b c d : D) : ip (d * a) (b * cstar c) = ip (a * c) (cstar d * b)

The cross term of the composition law. This is the only step of compositionAlgebraOfAssoc that uses associativity of D, and it is the same identity that IsCompSubalgebra.forced_assoc reads in the opposite direction.

@[instance_reducible]

def CompositionAlgebra.CD.compositionAlgebraOfAssoc {D : Type u} [NonAssocRing D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (hassoc : ∀ (p q r : D), p * q * r = p * (q * r)) : CompositionAlgebra (CD D)

The Cayley–Dickson double of an associative composition algebra is a composition algebra. Stated as a def taking associativity as an explicit hypothesis; the instance for [Ring D] is instCompositionAlgebra below.

Equations

• CompositionAlgebra.CD.compositionAlgebraOfAssoc hassoc = { B := CompositionAlgebra.CD.bilin, B_symm := ⋯, B_pos := ⋯, B_comp := ⋯ }

The double of an associative composition algebra

@[instance_reducible]

instance CompositionAlgebra.CD.instCompositionAlgebra {D : Type u} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] : CompositionAlgebra (CD D)

CD D is a Euclidean composition algebra whenever D is an associative one.

Equations

• CompositionAlgebra.CD.instCompositionAlgebra = CompositionAlgebra.CD.compositionAlgebraOfAssoc ⋯

@[simp]

theorem CompositionAlgebra.CD.nf_eq {D : Type u} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (x : CD D) : nf x = nf x.fst + nf x.snd

@[simp]

theorem CompositionAlgebra.CD.ip_eq {D : Type u} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (x y : CD D) : ip x y = ip x.fst y.fst + ip x.snd y.snd

theorem CompositionAlgebra.CD.cstar_eq {D : Type u} [Ring D] [Module ℝ D] [IsScalarTower ℝ D D] [SMulCommClass ℝ D D] [CompositionAlgebra D] [Nontrivial D] (x : CD D) : cstar x = mk (cstar x.fst) (-x.snd)

The conjugation of the double negates the second component.