Zorn vector matrices (GPR 21.18)

The algebra of Zorn vector matrices Zor(k) is the k-module of formal matrices

[ρ₁ u₂] [u₁ ρ₂], ρᵢ ∈ k, uᵢ ∈ k³,

with the multiplication built from the dot and cross products of k³ (GPR (21.18.4))

[ρ₁ u₂] [σ₁ v₂] [ ρ₁σ₁ - u₂ᵀv₁ ρ₁v₂ + σ₂u₂ + u₁ ⨯ v₁ ] [u₁ ρ₂] [v₁ σ₂] = [ σ₁u₁ + ρ₂v₁ + u₂ ⨯ v₂ ρ₂σ₂ - u₁ᵀv₂ ],

the norm n = ρ₁ρ₂ + u₁ᵀu₂, the trace t = ρ₁ + ρ₂ and the conjugation exchanging the diagonal and negating the off-diagonal entries.

This is the split octonion algebra, and it exists over every commutative ring. That is the point of the file: the Cayley–Dickson tower of Composition/Octonion.lean produces composition algebras only when 2 is invertible — in characteristic 2 its very first rung Cay(k, μ) has identically zero polar form, so its norm becomes degenerate over some extension field and is never non-singular in the sense of GPR 19.5 (GPR 19.4) — whereas Zor(k) is a composition algebra of rank 8 over an arbitrary base, in every characteristic, with no unit scalars to choose. It is therefore the first octonion algebra in this development available over, say, 𝔽₂, and it is the object the classification of reduced composition algebras (GPR 22.15) is stated in terms of.

Coordinates

Zor k is a type synonym for (k × k³) × (k × k³), with x.1 = (ρ₁, u₁) the first column of the matrix above and x.2 = (ρ₂, u₂) the second. The grouping is chosen so that the norm is literally the pairing of x.1 against x.2, which is what makes it visibly hyperbolic — the norm form of Zor(k) is four hyperbolic planes, and that is the whole content of its non-singularity.

Main definitions

• ConicAlgebra.Zor k : the underlying k-module of the algebra of Zorn vector matrices, with its multiplication.
• ConicAlgebra.zorNorm k : the norm ρ₁ρ₂ + u₁ᵀu₂ (GPR (21.18.6)).
• ConicAlgebra.zor k : the conic structure (GPR 21.18).

Main results

• ConicAlgebra.isMultiplicative_zor : the norm permits composition, n(xy) = n(x) n(y).
• ConicAlgebra.isGPRNonsingular_zorNorm : the norm is non-singular, because it is hyperbolic.
• ConicAlgebra.isComposition_zor : Zor(k) is a composition algebra over every commutative ring, with no hypothesis on 2.
• ConicAlgebra.finrank_zor : it has rank 8, so it is an octonion algebra.
• ConicAlgebra.instIsAlternativeZor : it is alternative.
• ConicAlgebra.trace_zor_apply, ConicAlgebra.conj_zor_apply : GPR (21.18.7), (21.18.8).

Implementation notes

The multiplication is not obtained from GPR's ternary hermitian construction Ter(D; D³, h, Δ), of which GPR 21.18 computes it to be a special case; it is taken as the definition, and the identities GPR 21.18 derives are proved here directly. Everything reduces to polynomial identities in the sixteen coordinates of a pair of vector matrices, and the only two facts about k³ that are used are u ⬝ᵥ (u ⨯₃ v) = 0 and the Binet–Cauchy identity (a ⨯₃ b) ⬝ᵥ (c ⨯₃ d) = (a ⬝ᵥ c) (b ⬝ᵥ d) - (a ⬝ᵥ d) (b ⬝ᵥ c) — both of which ring supplies after Fin 3 is expanded.

⚠ No hypothesis on 2 anywhere in this file, and none is available: the whole reason for constructing Zor(k) by hand rather than as Cay(Cay(Cay(k, 1), 1), 1) is that the Cayley–Dickson double Cay(k, 1) is not the split quadratic étale algebra k × k when 2 = 0 — it is k[ε], whose norm has a radical. Splitting the hyperbolic plane ⟨1⟩ ⊥ ⟨-1⟩ off as xy needs 2 invertible, and Zor(k) is precisely the object that does not.

References

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

def ConicAlgebra.Zor (k : Type u) : Type u

The k-module underlying the algebra of Zorn vector matrices Zor(k) (GPR (21.18.5)), as a type synonym for (k × k³) × (k × k³): the element x is the matrix

[x.1.1 x.2.2] [x.1.2 x.2.1]

whose first column is x.1 = (ρ₁, u₁) and whose second column is x.2 = (ρ₂, u₂). The synonym is needed because the multiplication below is not the componentwise one.

Equations

• ConicAlgebra.Zor k = ((k × (Fin 3 → k)) × k × (Fin 3 → k))

@[instance_reducible]

instance ConicAlgebra.Zor.instAddCommGroup (k : Type u) [CommRing k] : AddCommGroup (Zor k)

Equations

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

@[instance_reducible]

instance ConicAlgebra.Zor.instModule (k : Type u) [CommRing k] : Module k (Zor k)

Equations

• ConicAlgebra.Zor.instModule k = { smul := ConicAlgebra.Zor.instModule._aux_1 k, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance ConicAlgebra.Zor.instFinite (k : Type u) [CommRing k] : Module.Finite k (Zor k)

instance ConicAlgebra.Zor.instProjective (k : Type u) [CommRing k] : Module.Projective k (Zor k)

instance ConicAlgebra.Zor.instFree (k : Type u) [CommRing k] : Module.Free k (Zor k)

theorem ConicAlgebra.Zor.ext {k : Type u} {x y : Zor k} (h₁ : x.1.1 = y.1.1) (h₂ : x.1.2 = y.1.2) (h₃ : x.2.1 = y.2.1) (h₄ : x.2.2 = y.2.2) : x = y

Two Zorn vector matrices agree as soon as their four entries do.

@[simp]

theorem ConicAlgebra.Zor.fst_add {k : Type u} [CommRing k] (x y : Zor k) : (x + y).1 = x.1 + y.1

@[simp]

theorem ConicAlgebra.Zor.snd_add {k : Type u} [CommRing k] (x y : Zor k) : (x + y).2 = x.2 + y.2

@[simp]

theorem ConicAlgebra.Zor.fst_zero {k : Type u} [CommRing k] : 0.1 = 0

@[simp]

theorem ConicAlgebra.Zor.snd_zero {k : Type u} [CommRing k] : 0.2 = 0

@[simp]

theorem ConicAlgebra.Zor.fst_neg {k : Type u} [CommRing k] (x : Zor k) : (-x).1 = -x.1

@[simp]

theorem ConicAlgebra.Zor.snd_neg {k : Type u} [CommRing k] (x : Zor k) : (-x).2 = -x.2

@[simp]

theorem ConicAlgebra.Zor.fst_sub {k : Type u} [CommRing k] (x y : Zor k) : (x - y).1 = x.1 - y.1

@[simp]

theorem ConicAlgebra.Zor.snd_sub {k : Type u} [CommRing k] (x y : Zor k) : (x - y).2 = x.2 - y.2

@[simp]

theorem ConicAlgebra.Zor.fst_smul {k : Type u} [CommRing k] (c : k) (x : Zor k) : (c • x).1 = c • x.1

@[simp]

theorem ConicAlgebra.Zor.snd_smul {k : Type u} [CommRing k] (c : k) (x : Zor k) : (c • x).2 = c • x.2

@[instance_reducible]

instance ConicAlgebra.Zor.instMul (k : Type u) [CommRing k] : Mul (Zor k)

The multiplication of Zorn vector matrices, GPR (21.18.4).

Equations

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

@[instance_reducible]

instance ConicAlgebra.Zor.instOne (k : Type u) [CommRing k] : One (Zor k)

The identity matrix diag(1, 1).

Equations

• ConicAlgebra.Zor.instOne k = { one := ((1, 0), 1, 0) }

@[simp]

theorem ConicAlgebra.Zor.mul_fst_fst {k : Type u} [CommRing k] (x y : Zor k) : (x * y).1.1 = x.1.1 * y.1.1 - x.2.2 ⬝ᵥ y.1.2

@[simp]

theorem ConicAlgebra.Zor.mul_fst_snd {k : Type u} [CommRing k] (x y : Zor k) : (x * y).1.2 = y.1.1 • x.1.2 + x.2.1 • y.1.2 + (crossProduct x.2.2) y.2.2

@[simp]

theorem ConicAlgebra.Zor.mul_snd_fst {k : Type u} [CommRing k] (x y : Zor k) : (x * y).2.1 = x.2.1 * y.2.1 - x.1.2 ⬝ᵥ y.2.2

@[simp]

theorem ConicAlgebra.Zor.mul_snd_snd {k : Type u} [CommRing k] (x y : Zor k) : (x * y).2.2 = x.1.1 • y.2.2 + y.2.1 • x.2.2 + (crossProduct x.1.2) y.1.2

@[simp]

theorem ConicAlgebra.Zor.one_fst_fst {k : Type u} [CommRing k] : 1.1.1 = 1

@[simp]

theorem ConicAlgebra.Zor.one_fst_snd {k : Type u} [CommRing k] : 1.1.2 = 0

@[simp]

theorem ConicAlgebra.Zor.one_snd_fst {k : Type u} [CommRing k] : 1.2.1 = 1

@[simp]

theorem ConicAlgebra.Zor.one_snd_snd {k : Type u} [CommRing k] : 1.2.2 = 0

@[instance_reducible]

instance ConicAlgebra.Zor.instNonAssocRing (k : Type u) [CommRing k] : NonAssocRing (Zor k)

Equations

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

instance ConicAlgebra.Zor.instSMulCommClass (k : Type u) [CommRing k] : SMulCommClass k (Zor k) (Zor k)

instance ConicAlgebra.Zor.instIsScalarTower (k : Type u) [CommRing k] : IsScalarTower k (Zor k) (Zor k)

@[simp]

theorem ConicAlgebra.finrank_zor (k : Type u) [CommRing k] [Nontrivial k] : Module.finrank k (Zor k) = 8

Zor(k) has rank 8: it is an octonion algebra.

The norm

The norm n(x) = ρ₁ρ₂ + u₁ᵀu₂ (GPR (21.18.6)) is the pairing of the two columns of the matrix against each other, so it is built here from that pairing rather than written out as a polynomial: this is what QuadraticForm.isGPRNonsingular_of_basis_pairing consumes, and it is why the norm is hyperbolic.

def ConicAlgebra.zorPairing (k : Type u) [CommRing k] : LinearMap.BilinForm k (k × (Fin 3 → k))

The coordinate pairing ⟪(ρ, u), (σ, v)⟫ = ρσ + uᵀv on k × k³.

Equations

• ConicAlgebra.zorPairing k = LinearMap.mk₂ k (fun (m n : k × (Fin 3 → k)) => m.1 * n.1 + m.2 ⬝ᵥ n.2) ⋯ ⋯ ⋯ ⋯

def ConicAlgebra.zorBilin (k : Type u) [CommRing k] : LinearMap.BilinForm k (Zor k)

The bilinear form pairing the first column of a Zorn vector matrix against its second.

Equations

• ConicAlgebra.zorBilin k = LinearMap.compl₁₂ (ConicAlgebra.zorPairing k) (LinearMap.fst k (k × (Fin 3 → k)) (k × (Fin 3 → k))) (LinearMap.snd k (k × (Fin 3 → k)) (k × (Fin 3 → k)))

def ConicAlgebra.zorNorm (k : Type u) [CommRing k] : QuadraticForm k (Zor k)

The norm of a Zorn vector matrix, n(x) = ρ₁ρ₂ + u₁ᵀu₂ (GPR (21.18.6)): the determinant-like pairing of the two columns.

Equations

• ConicAlgebra.zorNorm k = LinearMap.BilinMap.toQuadraticMap (ConicAlgebra.zorBilin k)

@[simp]

theorem ConicAlgebra.zorNorm_apply {k : Type u} [CommRing k] (x : Zor k) : (zorNorm k) x = x.1.1 * x.2.1 + x.1.2 ⬝ᵥ x.2.2

theorem ConicAlgebra.polar_zorNorm {k : Type u} [CommRing k] (x y : Zor k) : QuadraticMap.polar (⇑(zorNorm k)) x y = x.1.1 * y.2.1 + y.1.1 * x.2.1 + x.1.2 ⬝ᵥ y.2.2 + y.1.2 ⬝ᵥ x.2.2

@[simp]

theorem ConicAlgebra.polar_zorNorm_one {k : Type u} [CommRing k] (x : Zor k) : QuadraticMap.polar (⇑(zorNorm k)) 1 x = x.1.1 + x.2.1

def ConicAlgebra.zor (k : Type u) [CommRing k] : ConicAlgebra k (Zor k)

GPR 21.18: the Zorn vector matrices form a conic algebra, with norm ρ₁ρ₂ + u₁ᵀu₂ and trace ρ₁ + ρ₂. Over an arbitrary commutative ring, with no hypothesis on 2.

Equations

• ConicAlgebra.zor k = { norm := ConicAlgebra.zorNorm k, norm_one := ⋯, mul_self := ⋯ }

@[simp]

theorem ConicAlgebra.zor_norm {k : Type u} [CommRing k] : (zor k).norm = zorNorm k

@[simp]

theorem ConicAlgebra.trace_zor_apply {k : Type u} [CommRing k] (x : Zor k) : (zor k).trace x = x.1.1 + x.2.1

The trace of a Zorn vector matrix is the trace of the matrix, GPR (21.18.7).

@[simp]

theorem ConicAlgebra.conj_zor_apply {k : Type u} [CommRing k] (x : Zor k) : (zor k).conj x = ((x.2.1, -x.1.2), x.1.1, -x.2.2)

The conjugation exchanges the diagonal entries and negates the off-diagonal ones, GPR (21.18.8).

Multiplicativity of the norm

n(xy) = n(x) n(y) is a polynomial identity in the sixteen coordinates; after Fin 3 is expanded it is exactly the Binet–Cauchy identity plus the vanishing of u ⬝ᵥ (u ⨯₃ v), and ring finds both.

theorem ConicAlgebra.isMultiplicative_zor {k : Type u} [CommRing k] : (zor k).IsMultiplicative

The norm of Zor(k) permits composition (GPR 19.1 for this algebra): n(xy) = n(x) n(y) over any commutative ring.

Alternativity

instance ConicAlgebra.instIsAlternativeZor {k : Type u} [CommRing k] : IsAlternative (Zor k)

Zor(k) is alternative. Both alternative laws are polynomial identities in the sixteen coordinates of two vector matrices; no regularity and no hypothesis on 2 is used, so this is independent of GPR 19.3.

Non-singularity, and the composition algebra

The norm pairs the two columns of the matrix against each other in the coordinates of the standard basis of k × k³, so it is a sum of four hyperbolic planes; that is all QuadraticForm.isGPRNonsingular_of_basis_pairing needs.

noncomputable def ConicAlgebra.zorColumnBasis (k : Type u) [CommRing k] : Module.Basis (Unit ⊕ Fin 3) k (k × (Fin 3 → k))

The standard basis of k × k³, indexed by Unit ⊕ Fin 3.

Equations

• ConicAlgebra.zorColumnBasis k = (Module.Basis.singleton Unit k).prod (Pi.basisFun k (Fin 3))

theorem ConicAlgebra.isGPRNonsingular_zorNorm (k : Type u) [CommRing k] : (zorNorm k).IsGPRNonsingular

The norm of Zor(k) is non-singular — indeed hyperbolic, being the pairing of the first column of the matrix against the second. No hypothesis on 2.

theorem ConicAlgebra.isComposition_zor (k : Type u) [CommRing k] : (zor k).IsComposition

Zor(k) is a composition algebra over every commutative ring (GPR 21.18, 21.19(d)): the split octonion algebra. Unlike ConicAlgebra.isComposition_cay₈ this needs no hypothesis on 2 and no choice of unit scalars.