The first two rungs are mathlib's `ℂ` and `ℍ` #

The Cayley–Dickson tower over ℝ at μᵢ = -1 produces algebras of dimension 2 and 4 which are the complex numbers and the quaternions. mathlib has both, so the identification is a theorem, not a definition: this file builds the two AlgEquivs and checks that they carry the conic norm to Complex.normSq and Quaternion.normSq and the conic conjugation to star.

Nothing else in the project depends on this file. It exists so that the tower is anchored to mathlib's objects rather than merely resembling them, and so that a reader who knows Complex.normSq can recognize ConicAlgebra.norm.

The dictionary #

Cay₂ ℝ (-1) is ℝ × ℝ with (a, b)(c, d) = (ac - db, da + bc) — the conjugation of the base ring being the identity — which is multiplication of a + bi. So (a, b) ↦ ⟨a, b⟩.

Cay₄ ℝ (-1) (-1) is ℂ × ℂ with (u₁, v₁)(u₂, v₂) = (u₁u₂ - (conj v₂)v₁, v₂u₁ + v₁(conj u₂)), which is multiplication of u + vj. Writing u = a + bi and v = c + di gives a + bi + cj + dk with k = ij, so ((a, b), (c, d)) ↦ ⟨a, b, c, d⟩. mathlib's Quaternion ℝ is QuaternionAlgebra ℝ (-1) 0 (-1), whose structure constants are exactly i² = j² = -1.

⚠ These are equivalences at μ₁ = μ₂ = -1 over ℝ specifically. Cay₄ k μ₁ μ₂ and QuaternionAlgebra k a b c are not comparable in general — see overview trap 3: QuaternionAlgebra takes arbitrary structure constants and always produces a free module, while Cay₄ k μ₁ μ₂ is a composition algebra when 2 and the μᵢ are units (ConicAlgebra.isComposition_cay₄, which needs Invertible (2 : k): in characteristic 2 the polar form of the norm of Cay₄ k μ₁ μ₂ is identically zero, so it is never a composition algebra).

Main results #

ConicAlgebra.realComplexAlgEquiv : Cay₂ ℝ (-1) ≃ₐ[ℝ] ℂ.
ConicAlgebra.realQuaternionAlgEquiv : Cay₄ ℝ (-1) (-1) ≃ₐ[ℝ] ℍ[ℝ].
ConicAlgebra.norm_realComplexAlgEquiv, ConicAlgebra.norm_realQuaternionAlgEquiv : the equivalences are isometries for Complex.normSq and Quaternion.normSq.
ConicAlgebra.conj_realComplexAlgEquiv, ConicAlgebra.conj_realQuaternionAlgEquiv : they carry ConicAlgebra.conj to star.

References #

[GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 18.4, 19.18.

`Cay₂ ℝ (-1) = ℂ` #

source

def ConicAlgebra.realComplexAlgEquiv :

RealComplex ≃ₐ[ℝ ] ℂ

The rank-two rung is ℂ. (a, b) ↦ a + bi.

Equations

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

Instances For

source

@[simp]

theorem ConicAlgebra.realComplexAlgEquiv_apply (x : RealComplex) :

realComplexAlgEquiv x = { re := x.1, im := x.2 }

source

theorem ConicAlgebra.norm_realComplexAlgEquiv (x : RealComplex) :

(cay₂ ℝ (-1)).norm x = Complex.normSq (realComplexAlgEquiv x)

The equivalence is an isometry: the conic norm of Cay₂ ℝ (-1) is Complex.normSq.

source

theorem ConicAlgebra.conj_realComplexAlgEquiv (x : RealComplex) :

realComplexAlgEquiv ((cay₂ ℝ (-1)).conj x) = star (realComplexAlgEquiv x)

The equivalence carries the conic conjugation to complex conjugation.

`Cay₄ ℝ (-1) (-1) = ℍ` #

⚠ Two elaboration hazards meet here, and the proofs are shaped around both.

The first is the one documented in Conic/CayleyDicksonAlternative.lean: ConicAlgebra.cay_conj_apply produces a pair literal, whose inferred type is ℝ × ℝ rather than Cay₂ ℝ μ, and once such a literal sits inside a product the Cay simp lemmas no longer unify. So the conjugation is only ever rewritten through its components, and cay_conj_apply is removed from the default simp set with -cay_conj_apply.

The second is that ℍ[ℝ] is a def wrapping QuaternionAlgebra ℝ (-1) 0 (-1). A goal mixing that spelling with RealQuaternion is not type-correct at rw's transparency, so each quaternion computation first changes its goal into the ℍ[ℝ, -1, 0, -1] spelling and only then rewrites with QuaternionAlgebra.mk_mul_mk or QuaternionAlgebra.star_mk.