The split composition algebras (GPR 21.19)

GPR 21.19 lists one composition algebra in each of the ranks 1, 2, 4, 8 and calls it the split algebra of that rank:

rank	algebra	norm	trace	conjugation
1	k	x ↦ x²	2x	x
2	k × k	(a, b) ↦ ab	a + b	(a, b) ↦ (b, a)
4	Mat₂(k)	det	trace	adjugate
8	Zor(k)	ρ₁ρ₂ + u₁ᵀu₂	ρ₁ + ρ₂	diagonal swap

Ranks 1 and 8 are already available — ConicAlgebra.baseRing and ConicAlgebra.zor — and this file supplies the two in between: the split quadratic étale algebra k × k and the split quaternion algebra Mat₂(k). As with Zor(k), and in contrast with the Cayley–Dickson tower of Composition/Octonion.lean, each is a composition algebra over an arbitrary commutative ring, with no hypothesis on 2: their norms are hyperbolic, and hyperbolic forms are regular in every characteristic.

Main definitions

• ConicAlgebra.splitEtale k : k × k with norm the hyperbolic plane (a, b) ↦ ab (GPR 21.19(b)). The norm is mathlib-free but not new — it is QuadraticForm.plane k.
• ConicAlgebra.splitQuaternionNorm k, ConicAlgebra.splitQuaternion k : Mat₂(k) with norm the determinant (GPR 21.19(c)).

Main results

• ConicAlgebra.isComposition_splitEtale, ConicAlgebra.isComposition_splitQuaternion : both are composition algebras over every commutative ring.
• ConicAlgebra.finrank_splitEtale, ConicAlgebra.finrank_splitQuaternion : of ranks 2 and 4.
• ConicAlgebra.conj_splitEtale_apply : the conjugation of k × k is the exchange involution.
• ConicAlgebra.conj_splitQuaternion_apply : the conjugation of Mat₂(k) is the adjugate, so the conic identity x (conj x) = n(x) 1 is the classical A · adj A = det A · 1.

Implementation notes

Neither algebra needs a type synonym: unlike the Cayley–Dickson double and Zor(k), the multiplication is the one mathlib already puts on k × k and on Matrix (Fin 2) (Fin 2) k, so the conic structure is extra data on an existing algebra and nothing has to be redefined. Both are associative, so the four typeclasses a conic algebra needs come from their Algebra k instances.

The degree-two identity is, in the two cases, the componentwise identity a² = (a + b)a - ab and the Cayley–Hamilton theorem for 2 × 2 matrices; the latter is proved here entrywise rather than by invoking mathlib's general Matrix.aeval_self_charpoly, since at size 2 the entrywise computation is four applications of ring and needs no characteristic-polynomial API.

Non-singularity is, in both cases, the observation that the norm is a sum of hyperbolic planes: (a, b) ↦ ab is the pairing of k against k, and det = a₀₀a₁₁ - a₀₁a₁₀ is the pairing of (a₀₀, a₀₁) against (a₁₁, -a₁₀). QuadraticForm.isGPRNonsingular_of_basis_pairing and its equivalence-composed form read these off; no determinant criterion and no hypothesis on 2 enters.

References

• [GPR] Garibaldi, Petersson, Racine, Albert Algebras over Commutative Rings, 21.18, 21.19.

Rank two: the split quadratic étale algebra k × k

The norm of k × k is mathlib-free but not new: it is the hyperbolic plane QuadraticForm.plane k of QuadraticForm/HyperbolicPair.lean, (a, b) ↦ ab. Nothing is redefined here.

def ConicAlgebra.splitEtale (k : Type u) [CommRing k] : ConicAlgebra k (k × k)

GPR 21.19(b): k × k is a conic algebra with norm (a, b) ↦ ab and trace a + b.

Equations

• ConicAlgebra.splitEtale k = { norm := QuadraticForm.plane k, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.splitEtale_norm {k : Type u} [CommRing k] : (splitEtale k).norm = QuadraticForm.plane k

@[simp]

theorem ConicAlgebra.trace_splitEtale_apply {k : Type u} [CommRing k] (x : k × k) : (splitEtale k).trace x = x.1 + x.2

The trace of k × k is the sum of the two coordinates.

@[simp]

theorem ConicAlgebra.conj_splitEtale_apply {k : Type u} [CommRing k] (x : k × k) : (splitEtale k).conj x = (x.2, x.1)

The conjugation of k × k is the exchange involution (a, b) ↦ (b, a), as GPR 21.18 requires of the split quadratic étale algebra.

theorem ConicAlgebra.isMultiplicative_splitEtale {k : Type u} [CommRing k] : (splitEtale k).IsMultiplicative

The norm of k × k permits composition: it is multiplicative because multiplication is componentwise.

theorem ConicAlgebra.isComposition_splitEtale (k : Type u) [CommRing k] : (splitEtale k).IsComposition

GPR 21.19(b): k × k is a composition algebra over every commutative ring, the split one of rank two.

theorem ConicAlgebra.finrank_splitEtale (k : Type u) [CommRing k] [Nontrivial k] : Module.finrank k (k × k) = 2

k × k has rank 2. (Not a simp lemma: mathlib's Module.finrank_prod already reduces the left-hand side, to 1 + 1.)

Rank four: the split quaternion algebra Mat₂(k)

def ConicAlgebra.splitQuaternionBilin (k : Type u) [CommRing k] : LinearMap.BilinForm k (Matrix (Fin 2) (Fin 2) k)

The bilinear form (A, B) ↦ a₀₀b₁₁ - a₀₁b₁₀ on Mat₂(k), whose associated quadratic form is the determinant.

Equations

• ConicAlgebra.splitQuaternionBilin k = LinearMap.mk₂ k (fun (A B : Matrix (Fin 2) (Fin 2) k) => A 0 0 * B 1 1 - A 0 1 * B 1 0) ⋯ ⋯ ⋯ ⋯

def ConicAlgebra.splitQuaternionNorm (k : Type u) [CommRing k] : QuadraticForm k (Matrix (Fin 2) (Fin 2) k)

The norm of the split quaternion algebra Mat₂(k) (GPR 21.19(c)): the determinant.

Equations

• ConicAlgebra.splitQuaternionNorm k = LinearMap.BilinMap.toQuadraticMap (ConicAlgebra.splitQuaternionBilin k)

theorem ConicAlgebra.splitQuaternionNorm_apply' {k : Type u} [CommRing k] (A : Matrix (Fin 2) (Fin 2) k) : (splitQuaternionNorm k) A = A 0 0 * A 1 1 - A 0 1 * A 1 0

@[simp]

theorem ConicAlgebra.splitQuaternionNorm_apply {k : Type u} [CommRing k] (A : Matrix (Fin 2) (Fin 2) k) : (splitQuaternionNorm k) A = A.det

The norm of Mat₂(k) is the determinant.

theorem ConicAlgebra.polar_splitQuaternionNorm {k : Type u} [CommRing k] (A B : Matrix (Fin 2) (Fin 2) k) : QuadraticMap.polar (⇑(splitQuaternionNorm k)) A B = A 0 0 * B 1 1 + B 0 0 * A 1 1 - A 0 1 * B 1 0 - B 0 1 * A 1 0

@[simp]

theorem ConicAlgebra.polar_splitQuaternionNorm_one {k : Type u} [CommRing k] (A : Matrix (Fin 2) (Fin 2) k) : QuadraticMap.polar (⇑(splitQuaternionNorm k)) 1 A = A.trace

theorem ConicAlgebra.mul_self_eq_trace_smul_sub_det_smul {k : Type u} [CommRing k] (A : Matrix (Fin 2) (Fin 2) k) : A * A = A.trace • A - A.det • 1

Cayley–Hamilton at size two: A² = tr(A)·A - det(A)·1. Proved entrywise; this is the degree-two identity that makes Mat₂(k) a conic algebra.

def ConicAlgebra.splitQuaternion (k : Type u) [CommRing k] : ConicAlgebra k (Matrix (Fin 2) (Fin 2) k)

GPR 21.19(c): Mat₂(k) is a conic algebra with norm the determinant and trace the matrix trace. The degree-two identity is Cayley–Hamilton at size two.

Equations

• ConicAlgebra.splitQuaternion k = { norm := ConicAlgebra.splitQuaternionNorm k, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.splitQuaternion_norm {k : Type u} [CommRing k] : (splitQuaternion k).norm = splitQuaternionNorm k

@[simp]

theorem ConicAlgebra.trace_splitQuaternion_apply {k : Type u} [CommRing k] (A : Matrix (Fin 2) (Fin 2) k) : (splitQuaternion k).trace A = A.trace

The trace of the conic algebra Mat₂(k) is the trace of the matrix.

@[simp]

theorem ConicAlgebra.conj_splitQuaternion_apply {k : Type u} [CommRing k] (A : Matrix (Fin 2) (Fin 2) k) : (splitQuaternion k).conj A = A.adjugate

The conjugation of Mat₂(k) is the adjugate. Consequently the conic identity x (conj x) = n(x) 1 specializes to A · adj A = det A · 1.

theorem ConicAlgebra.isMultiplicative_splitQuaternion {k : Type u} [CommRing k] : (splitQuaternion k).IsMultiplicative

The norm of Mat₂(k) permits composition: this is multiplicativity of the determinant.

def ConicAlgebra.splitQuaternionEquiv (k : Type u) [CommRing k] : Matrix (Fin 2) (Fin 2) k ≃ₗ[k] (Fin 2 → k) × (Fin 2 → k)

Mat₂(k) presented as k² ⊕ k², by reading off the pair (a₀₀, a₀₁) and the pair (a₁₁, -a₁₀). Under this equivalence the determinant becomes the standard pairing of the two factors, which is what exhibits it as two hyperbolic planes.

Equations

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

theorem ConicAlgebra.isGPRNonsingular_splitQuaternionNorm (k : Type u) [CommRing k] : (splitQuaternionNorm k).IsGPRNonsingular

The norm of Mat₂(k) is non-singular: the determinant is two hyperbolic planes, pairing (a₀₀, a₀₁) against (a₁₁, -a₁₀). No hypothesis on 2, and no determinant criterion — the determinant here is the form, not the tool.

theorem ConicAlgebra.isComposition_splitQuaternion (k : Type u) [CommRing k] : (splitQuaternion k).IsComposition

GPR 21.19(c): Mat₂(k) is a composition algebra over every commutative ring, the split one of rank four.

@[simp]

theorem ConicAlgebra.finrank_splitQuaternion (k : Type u) [CommRing k] [Nontrivial k] : Module.finrank k (Matrix (Fin 2) (Fin 2) k) = 4

Mat₂(k) has rank 4.