The Cayley–Dickson construction (GPR 18.3, GPR 18.4)

Given a conic algebra B over k and a scalar μ ∈ k, the Cayley–Dickson double Cay(B, μ) is the k-module B ⊕ B, written u + v j, with

(u₁ + v₁ j)(u₂ + v₂ j) = (u₁u₂ + μ (conj v₂)v₁) + (v₂u₁ + v₁(conj u₂)) j, 1 = 1_B + 0 j, n(u + v j) = n_B(u) - μ n_B(v).

It is again a conic algebra (ConicAlgebra.cay, GPR 18.4), and its trace and conjugation are

t(u + v j) = t_B(u), conj (u + v j) = conj u - v j.

Main definitions

• ConicAlgebra.Cay C μ : the underlying k-module B ⊕ B, as a type synonym carrying the Cayley–Dickson multiplication rather than the componentwise one.
• ConicAlgebra.cay : GPR 18.4 — the conic algebra structure on Cay C μ.

Main results

• ConicAlgebra.cay_norm_apply, ConicAlgebra.cay_trace_apply, ConicAlgebra.cay_conj_apply : the formulas GPR 18.4(3), (5), (6).
• ConicAlgebra.cayIsometryEquiv : a norm isometry acts componentwise on doubles; if it is unital and multiplicative, so is the doubled equivalence.
• ConicAlgebra.cayIsometryEquivOfEq : transport between doubles whose parameters are equal.
• ConicAlgebra.inl : the embedding B ↪ Cay C μ of GPR 18.3, a unital algebra map.

Implementation notes

μ is an arbitrary scalar, not a unit. Everything here holds for every μ ∈ k, including 0; hypotheses that μ be invertible belong to later theorems (GPR 18.11 ff.), never to the construction.

No hypotheses on B beyond conic. The degree-two identity for Cay(B, μ) needs exactly two facts about B: (conj v)v = n(v) · 1 (ConicAlgebra.conj_mul_self) and u + conj u = t(u) · 1 (ConicAlgebra.add_conj), both of which hold in every conic algebra with no regularity, projectivity, alternativity or assumption on 2. In particular the norm is written down directly, so — unlike ConicAlgebra.baseChangeOfProjective — nothing here needs B to be projective.

Why a type synonym. B × B already carries the componentwise ring structure from mathlib, and the Cayley–Dickson multiplication is a different one, so it must live on a synonym. The synonym depends on the conic structure C, not just on B, because the multiplication uses the conjugation of B; two conic structures on the same B double to genuinely different algebras.

External, not internal. GPR 18.1 builds B + Bl inside an ambient algebra; GPR 18.2 warns that this sum need not be direct. The external construction on B ⊕ B has no such problem and is the one used here and in GPR 18.3 ff.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 18.1–18.4.

def ConicAlgebra.Cay {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (_C : ConicAlgebra k B) (_μ : k) : Type v

The underlying k-module B ⊕ B of the Cayley–Dickson double Cay(B, μ), as a type synonym: B × B already has the componentwise multiplication, and this one is different. The element (u, v) is GPR's u + v j.

The parameters C and μ are part of the type even though the underlying module does not depend on them: the multiplication does, so distinct parameters must give distinct types for instance resolution to be sound.

Equations

• _C.Cay _μ = (B × B)

@[instance_reducible]

instance ConicAlgebra.Cay.instAddCommGroup {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : AddCommGroup (C.Cay μ)

Equations

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

@[instance_reducible]

instance ConicAlgebra.Cay.instModule {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : Module k (C.Cay μ)

Equations

• ConicAlgebra.Cay.instModule C μ = { smul := ConicAlgebra.Cay.instModule._aux_1 C μ, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance ConicAlgebra.Cay.instFinite {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) [Module.Finite k B] : Module.Finite k (C.Cay μ)

The double of a finitely generated module is finitely generated: rank doubles, so a composition algebra of rank d doubles to one of rank 2d.

instance ConicAlgebra.Cay.instProjective {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) [Module.Projective k B] : Module.Projective k (C.Cay μ)

The double of a projective module is projective, which is what keeps the Cayley–Dickson tower inside the composition algebras.

instance ConicAlgebra.Cay.instFree {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) [Module.Free k B] : Module.Free k (C.Cay μ)

The double of a free module is free.

theorem ConicAlgebra.Cay.finrank_cay {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) [Nontrivial k] [Module.Free k B] [Module.Finite k B] : Module.finrank k (C.Cay μ) = 2 * Module.finrank k B

The rank doubles. This is what makes the Cayley–Dickson tower run through ranks 1, 2, 4, 8 (GPR 19.18).

@[simp]

theorem ConicAlgebra.Cay.fst_add {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : (x + y).1 = x.1 + y.1

@[simp]

theorem ConicAlgebra.Cay.snd_add {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : (x + y).2 = x.2 + y.2

@[simp]

theorem ConicAlgebra.Cay.fst_zero {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} : 0.1 = 0

@[simp]

theorem ConicAlgebra.Cay.snd_zero {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} : 0.2 = 0

@[simp]

theorem ConicAlgebra.Cay.fst_neg {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x : C.Cay μ) : (-x).1 = -x.1

@[simp]

theorem ConicAlgebra.Cay.snd_neg {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x : C.Cay μ) : (-x).2 = -x.2

@[simp]

theorem ConicAlgebra.Cay.fst_sub {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : (x - y).1 = x.1 - y.1

@[simp]

theorem ConicAlgebra.Cay.snd_sub {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : (x - y).2 = x.2 - y.2

@[simp]

theorem ConicAlgebra.Cay.fst_smul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (c : k) (x : C.Cay μ) : (c • x).1 = c • x.1

@[simp]

theorem ConicAlgebra.Cay.snd_smul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (c : k) (x : C.Cay μ) : (c • x).2 = c • x.2

theorem ConicAlgebra.Cay.ext {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} {x y : C.Cay μ} (h₁ : x.1 = y.1) (h₂ : x.2 = y.2) : x = y

def ConicAlgebra.Cay.mk {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (u v : B) : C.Cay μ

The element u + v j of Cay(B, μ), with components u and v. Writing explicit elements with Cay.mk rather than as a bare pair keeps their type Cay C μ visible, so that the lemmas about the doubled multiplication apply to them.

Equations

• ConicAlgebra.Cay.mk u v = (u, v)

@[simp]

theorem ConicAlgebra.Cay.fst_mk {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (u v : B) : (mk u v).1 = u

@[simp]

theorem ConicAlgebra.Cay.snd_mk {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (u v : B) : (mk u v).2 = v

@[instance_reducible]

instance ConicAlgebra.Cay.instMul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : Mul (C.Cay μ)

The Cayley–Dickson multiplication GPR 18.3: (u₁ + v₁j)(u₂ + v₂j) = (u₁u₂ + μ (conj v₂)v₁) + (v₂u₁ + v₁(conj u₂)) j.

Equations

• ConicAlgebra.Cay.instMul C μ = { mul := fun (x y : C.Cay μ) => (x.1 * y.1 + μ • (C.conj y.2 * x.2), y.2 * x.1 + x.2 * C.conj y.1) }

@[instance_reducible]

instance ConicAlgebra.Cay.instOne {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : One (C.Cay μ)

Equations

• ConicAlgebra.Cay.instOne C μ = { one := (1, 0) }

@[simp]

theorem ConicAlgebra.Cay.fst_mul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : (x * y).1 = x.1 * y.1 + μ • (C.conj y.2 * x.2)

@[simp]

theorem ConicAlgebra.Cay.snd_mul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : (x * y).2 = y.2 * x.1 + x.2 * C.conj y.1

@[simp]

theorem ConicAlgebra.Cay.fst_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} : 1.1 = 1

@[simp]

theorem ConicAlgebra.Cay.snd_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} : 1.2 = 0

@[instance_reducible]

instance ConicAlgebra.Cay.instNonAssocRing {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : NonAssocRing (C.Cay μ)

Equations

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

instance ConicAlgebra.Cay.instSMulCommClass {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) : SMulCommClass k (C.Cay μ) (C.Cay μ)

instance ConicAlgebra.Cay.instIsScalarTower {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) : IsScalarTower k (C.Cay μ) (C.Cay μ)

The conic structure

noncomputable def ConicAlgebra.cayNorm {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : QuadraticForm k (C.Cay μ)

The Cayley–Dickson norm n(u + v j) = n_B(u) - μ n_B(v), i.e. n_B ⊥ ⟨-μ⟩ n_B.

Equations

• C.cayNorm μ = QuadraticMap.prod C.norm (-μ • C.norm)

@[simp]

theorem ConicAlgebra.cayNorm_apply {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x : C.Cay μ) : (C.cayNorm μ) x = C.norm x.1 - μ * C.norm x.2

theorem ConicAlgebra.polar_cayNorm {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (x y : C.Cay μ) : QuadraticMap.polar (⇑(C.cayNorm μ)) x y = QuadraticMap.polar (⇑C.norm) x.1 y.1 - μ * QuadraticMap.polar (⇑C.norm) x.2 y.2

noncomputable def ConicAlgebra.cay {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] (C : ConicAlgebra k B) (μ : k) : ConicAlgebra k (C.Cay μ)

GPR 18.4: the Cayley–Dickson double of a conic algebra is a conic algebra.

The first component of x * x is u² + μ (conj v)v = t(u)·u - n(u)·1 + μ n(v)·1, and the second is vu + v(conj u) = v(u + conj u) = t(u)·v. No hypothesis on B or on μ.

Equations

• C.cay μ = { norm := C.cayNorm μ, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.cay_norm_apply {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} (x : C.Cay μ) : (C.cay μ).norm x = C.norm x.1 - μ * C.norm x.2

@[simp]

theorem ConicAlgebra.cay_trace_apply {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} (x : C.Cay μ) : (C.cay μ).trace x = C.trace x.1

GPR 18.4(5). The trace of Cay(B, μ) is the trace of B on the first component.

@[simp]

theorem ConicAlgebra.cay_conj_apply {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} (x : C.Cay μ) : (C.cay μ).conj x = (C.conj x.1, -x.2)

GPR 18.4(6). The conjugation of Cay(B, μ) is u + v j ↦ conj u - v j.

theorem ConicAlgebra.cay_conj_mk {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} (u v : B) : (C.cay μ).conj (Cay.mk u v) = Cay.mk (C.conj u) (-v)

GPR 18.4(6) on an explicit element: the conjugate of u + v j is conj u - v j.

Not a simp lemma, since cay_conj_apply already rewrites its left-hand side; it is for simp only calls that keep elements in Cay.mk form.

Functoriality

noncomputable def ConicAlgebra.cayIsometryEquivOfEq {k : Type u} [CommRing k] {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') {a b : k} (h : a = b) : QuadraticMap.IsometryEquiv (D.cay a).norm (D.cay b).norm

Equal Cayley–Dickson parameters give canonically isometric doubles. This explicit transport is needed because the parameter is part of the type Cay C μ.

Equations

• D.cayIsometryEquivOfEq h = h ▸ QuadraticMap.IsometryEquiv.refl (D.cay a).norm

@[simp]

theorem ConicAlgebra.cayIsometryEquivOfEq_map_one {k : Type u} [CommRing k] {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') {a b : k} (h : a = b) : (D.cayIsometryEquivOfEq h) 1 = 1

theorem ConicAlgebra.cayIsometryEquivOfEq_map_mul {k : Type u} [CommRing k] {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') {a b : k} (h : a = b) (x y : D.Cay a) : (D.cayIsometryEquivOfEq h) (x * y) = (D.cayIsometryEquivOfEq h) x * (D.cayIsometryEquivOfEq h) y

noncomputable def ConicAlgebra.cayIsometryEquiv {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') (e : QuadraticMap.IsometryEquiv C.norm D.norm) : QuadraticMap.IsometryEquiv (C.cay μ).norm (D.cay μ).norm

A norm isometry acts componentwise on Cayley–Dickson doubles with the same parameter.

No unitality or multiplicativity is needed for this statement: the doubled norm is the orthogonal product n ⊥ (-μ)n.

Equations

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

@[simp]

theorem ConicAlgebra.cayIsometryEquiv_apply {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') (e : QuadraticMap.IsometryEquiv C.norm D.norm) (x : C.Cay μ) : (cayIsometryEquiv D e) x = (e x.1, e x.2)

theorem ConicAlgebra.cayIsometryEquiv_map_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) : (cayIsometryEquiv D e) 1 = 1

The componentwise equivalence of doubles is unital when the original equivalence is.

theorem ConicAlgebra.cayIsometryEquiv_map_mul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} {B' : Type w} [NonAssocRing B'] [Module k B'] [SMulCommClass k B' B'] [IsScalarTower k B' B'] (D : ConicAlgebra k B') (e : QuadraticMap.IsometryEquiv C.norm D.norm) (h1 : e 1 = 1) (hmul : ∀ (x y : B), e (x * y) = e x * e y) (x y : C.Cay μ) : (cayIsometryEquiv D e) (x * y) = (cayIsometryEquiv D e) x * (cayIsometryEquiv D e) y

The componentwise equivalence of doubles is multiplicative when the original equivalence is unital and multiplicative.

GPR 18.11: the conjugation of the double

theorem ConicAlgebra.ConjIsInvolution.cay {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} (hconj : C.ConjIsInvolution) : (C.cay μ).ConjIsInvolution

GPR 18.11. If the conjugation of B is an involution then so is the conjugation of Cay(B, μ). No associativity and no hypothesis on μ: the verification is the two component identities conj(u₁u₂ + μ (conj v₂)v₁) = (conj u₂)(conj u₁) + μ (conj v₁)v₂ and -(v₂u₁ + v₁(conj u₂)) = -v₂u₁ - v₁(conj u₂).

The embedding of B

def ConicAlgebra.inl {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] (C : ConicAlgebra k B) (μ : k) : B →ₗ[k] C.Cay μ

GPR 18.3. The embedding u ↦ u + 0 j of B into Cay(B, μ). It is injective, unital and multiplicative, so B is a unital subalgebra of its double.

Equations

• C.inl μ = { toFun := fun (u : B) => (u, 0), map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem ConicAlgebra.inl_apply {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (u : B) : (C.inl μ) u = (u, 0)

theorem ConicAlgebra.inl_one {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} : (C.inl μ) 1 = 1

theorem ConicAlgebra.inl_mul {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} (u u' : B) : (C.inl μ) (u * u') = (C.inl μ) u * (C.inl μ) u'

theorem ConicAlgebra.inl_injective {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] {C : ConicAlgebra k B} {μ : k} : Function.Injective ⇑(C.inl μ)

theorem ConicAlgebra.norm_inl {k : Type u} {B : Type v} [CommRing k] [NonAssocRing B] [Module k B] [SMulCommClass k B B] [IsScalarTower k B B] {C : ConicAlgebra k B} {μ : k} (u : B) : (C.cay μ).norm ((C.inl μ) u) = C.norm u