The split octonions

The split octonions over a commutative ring R are realized here as Zorn vector matrices: an element is a formal 2 × 2 matrix

⟨a, b, v, w⟩ = [[a, v], [w, b]]

with scalar diagonal a b : R and vector off-diagonal v w : Fin 3 → R, multiplied by

[[a, v], [w, b]] * [[a', v'], [w', b']] = [[a * a' + v ⬝ᵥ w', a • v' + b' • v - w ⨯₃ w'], [a' • w + b • w' + v ⨯₃ v', b * b' + w ⬝ᵥ v']]

using the dot and cross products of Fin 3 → R. This is an 8-dimensional unital R-algebra carrying the multiplicative norm N ⟨a, b, v, w⟩ = a * b - v ⬝ᵥ w, the determinant of the vector matrix: it is the split Cayley algebra, the split form of the octonions. It is alternative, and the worked examples at the end of the file exhibit an R — namely ℤ — over which it is neither commutative nor associative; no such failure is claimed for every base ring, since over the zero ring Octonion R is trivial and hence both.

Zorn's model is used rather than a Cayley--Dickson doubling of the split quaternions because the two produce the same algebra while the vector matrices carry the norm form on their sleeve: N is a determinant, and its multiplicativity reduces to Mathlib's scalar quadruple product identity Matrix.cross_dot_cross.

The algebra structure, the conjugation, and the norm are stated over a commutative ring; no field, characteristic or closedness hypothesis is needed for them. The additive and module structures and the coordinate isomorphism need only an additive commutative monoid of coefficients. Only the two dimension counts TauCeti.Octonion.finrank_eq_eight and TauCeti.Octonion.finrank_imaginary ask for a base over which ranks are well behaved, and each asks for it as StrongRankCondition and nothing more.

Main definitions

• TauCeti.Octonion: the split octonions over R, as Zorn vector matrices, with their NonAssocRing and Module R structure and the two scalar towers.
• TauCeti.Octonion.conj: octonion conjugation ⟨a, b, v, w⟩ ↦ ⟨b, a, -v, -w⟩, an R-linear involution.
• TauCeti.Octonion.trace and TauCeti.Octonion.norm: the trace a + b and the norm a * b - v ⬝ᵥ w of the composition algebra.
• TauCeti.Octonion.imaginary: the imaginary octonions, the kernel of the trace.

Main results

• TauCeti.Octonion.finrank_eq_eight: the split octonions are 8-dimensional.
• TauCeti.Octonion.self_mul_conj and TauCeti.Octonion.conj_mul_self: x * conj x = conj x * x = N x • 1.
• TauCeti.Octonion.norm_mul: the norm is multiplicative, so 𝕆 is a composition algebra.
• TauCeti.Octonion.normQuadraticForm: the norm, bundled as a QuadraticForm, so that Mathlib's QuadraticMap.polar API supplies the associated symmetric bilinear form. That form is visible inside the algebra as TauCeti.Octonion.mul_conj_add_mul_conj, x * conj y + y * conj x = QuadraticMap.polar (normQuadraticForm R) x y • 1, and it is the trace form of the composition algebra, TauCeti.Octonion.trace_mul_conj.
• TauCeti.Octonion.left_alternative, TauCeti.Octonion.right_alternative and TauCeti.Octonion.flexible: 𝕆 is alternative and flexible.
• TauCeti.Octonion.moufang_left, TauCeti.Octonion.moufang_right and TauCeti.Octonion.moufang_middle: the three Moufang identities.
• TauCeti.Octonion.mul_self: every octonion satisfies its rank-two equation x * x = trace x • x - norm x • 1.
• TauCeti.Octonion.finrank_imaginary: the imaginary octonions, the trace-zero subspace, are 7-dimensional. The derivation algebra Der 𝕆 is TauCeti.derivationLieAlgebra R (Octonion R) (TauCeti/Algebra/Lie/Derivation/Basic.lean), of rank 14 by TauCeti.Octonion.finrank_derivationLieAlgebra. Over a field in which 2 is nonzero the imaginary octonions are an irreducible representation of Der 𝕆 (TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule, in TauCeti/Algebra/Octonion/Fundamental.lean), so there they are its 7-dimensional fundamental representation; only the isomorphism of Der 𝕆 with LieAlgebra.g₂ still waits.

Implementation notes

Almost every identity below is proved without ever looking at a coordinate: Octonion.ext splits an equation of octonions into its four entries, a file-local simp set pushes the dot and cross products of Fin 3 → R through the linear combinations that make up an entry of a product and reduces the compound products that survive by Mathlib's Matrix.cross_dot_cross, Matrix.cross_cross_eq_smul_sub_smul and Matrix.cross_cross_eq_smul_sub_smul', and module or ring finishes. The two Moufang identities proved directly are the exception: they need relations special to three coordinates that Mathlib does not name, so they — and the worked examples — expand the vector entries into coordinates through Matrix.vec3_dotProduct and Matrix.cross_apply, with a private coordinate extensionality lemma splitting an equation of octonions into its eight scalar coordinates.

No definition here is exposed: consumers work through the projection simp lemmas rather than through any definition body. The additive and module structures are transported from R × R × (Fin 3 → R) × (Fin 3 → R) along the injective map to the four entries, and TauCeti.Octonion.linearEquivProd packages a vector matrix as the tuple of those entries, a linear isomorphism over any semiring acting on the coefficients; the dimension count runs through it with R acting on itself.

The norm is available both as the bare map Octonion R → R and, through TauCeti.Octonion.normQuadraticForm, as a QuadraticForm R (Octonion R); the bundled form is what gives its polarization Mathlib's bilinearity and symmetry API for free. The derivation algebra Der 𝕆 is TauCeti.derivationLieAlgebra R (Octonion R), built in TauCeti/Algebra/Lie/Derivation/Basic.lean.

References

The model is M. Zorn, Alternativkörper und quadratische Systeme, Abh. Math. Sem. Univ. Hamburg 9 (1933); see also T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, §1.8, and J. C. Baez, The octonions, Bull. Amer. Math. Soc. 39 (2002), §2.

structure TauCeti.Octonion (R : Type u_1) : Type u_1

The split octonions over R, as Zorn vector matrices: the element ⟨a, b, v, w⟩ is the formal matrix [[a, v], [w, b]] with scalar diagonal and vector off-diagonal entries.

• a : R

  The top-left, scalar entry of the vector matrix.

• b : R

  The bottom-right, scalar entry of the vector matrix.

• v : Fin 3 → R

  The top-right, vector entry of the vector matrix.

• w : Fin 3 → R

  The bottom-left, vector entry of the vector matrix.

theorem TauCeti.Octonion.ext {R : Type u_1} {x y : Octonion R} (a : x.a = y.a) (b : x.b = y.b) (v : x.v = y.v) (w : x.w = y.w) : x = y

theorem TauCeti.Octonion.ext_iff {R : Type u_1} {x y : Octonion R} : x = y ↔ x.a = y.a ∧ x.b = y.b ∧ x.v = y.v ∧ x.w = y.w

The additive and module structure

@[instance_reducible]

instance TauCeti.Octonion.instZero {R : Type u_1} [Zero R] : Zero (Octonion R)

Equations

• TauCeti.Octonion.instZero = { zero := { a := 0, b := 0, v := 0, w := 0 } }

@[simp]

theorem TauCeti.Octonion.zero_a {R : Type u_1} [Zero R] : a 0 = 0

@[simp]

theorem TauCeti.Octonion.zero_b {R : Type u_1} [Zero R] : b 0 = 0

@[simp]

theorem TauCeti.Octonion.zero_v {R : Type u_1} [Zero R] : v 0 = 0

@[simp]

theorem TauCeti.Octonion.zero_w {R : Type u_1} [Zero R] : w 0 = 0

@[instance_reducible]

instance TauCeti.Octonion.instInhabitedOfZero {R : Type u_1} [Zero R] : Inhabited (Octonion R)

Equations

• TauCeti.Octonion.instInhabitedOfZero = { default := 0 }

@[instance_reducible]

instance TauCeti.Octonion.instOneOfZero {R : Type u_1} [Zero R] [One R] : One (Octonion R)

Equations

• TauCeti.Octonion.instOneOfZero = { one := { a := 1, b := 1, v := 0, w := 0 } }

@[simp]

theorem TauCeti.Octonion.one_a {R : Type u_1} [Zero R] [One R] : a 1 = 1

@[simp]

theorem TauCeti.Octonion.one_b {R : Type u_1} [Zero R] [One R] : b 1 = 1

@[simp]

theorem TauCeti.Octonion.one_v {R : Type u_1} [Zero R] [One R] : v 1 = 0

@[simp]

theorem TauCeti.Octonion.one_w {R : Type u_1} [Zero R] [One R] : w 1 = 0

@[instance_reducible]

instance TauCeti.Octonion.instAdd {R : Type u_1} [Add R] : Add (Octonion R)

Equations

• TauCeti.Octonion.instAdd = { add := fun (x y : TauCeti.Octonion R) => { a := x.a + y.a, b := x.b + y.b, v := x.v + y.v, w := x.w + y.w } }

@[simp]

theorem TauCeti.Octonion.add_a {R : Type u_1} [Add R] (x y : Octonion R) : (x + y).a = x.a + y.a

@[simp]

theorem TauCeti.Octonion.add_b {R : Type u_1} [Add R] (x y : Octonion R) : (x + y).b = x.b + y.b

@[simp]

theorem TauCeti.Octonion.add_v {R : Type u_1} [Add R] (x y : Octonion R) : (x + y).v = x.v + y.v

@[simp]

theorem TauCeti.Octonion.add_w {R : Type u_1} [Add R] (x y : Octonion R) : (x + y).w = x.w + y.w

@[instance_reducible]

instance TauCeti.Octonion.instNeg {R : Type u_1} [Neg R] : Neg (Octonion R)

Equations

• TauCeti.Octonion.instNeg = { neg := fun (x : TauCeti.Octonion R) => { a := -x.a, b := -x.b, v := -x.v, w := -x.w } }

@[simp]

theorem TauCeti.Octonion.neg_a {R : Type u_1} [Neg R] (x : Octonion R) : (-x).a = -x.a

@[simp]

theorem TauCeti.Octonion.neg_b {R : Type u_1} [Neg R] (x : Octonion R) : (-x).b = -x.b

@[simp]

theorem TauCeti.Octonion.neg_v {R : Type u_1} [Neg R] (x : Octonion R) : (-x).v = -x.v

@[simp]

theorem TauCeti.Octonion.neg_w {R : Type u_1} [Neg R] (x : Octonion R) : (-x).w = -x.w

@[instance_reducible]

instance TauCeti.Octonion.instSub {R : Type u_1} [Sub R] : Sub (Octonion R)

Equations

• TauCeti.Octonion.instSub = { sub := fun (x y : TauCeti.Octonion R) => { a := x.a - y.a, b := x.b - y.b, v := x.v - y.v, w := x.w - y.w } }

@[simp]

theorem TauCeti.Octonion.sub_a {R : Type u_1} [Sub R] (x y : Octonion R) : (x - y).a = x.a - y.a

@[simp]

theorem TauCeti.Octonion.sub_b {R : Type u_1} [Sub R] (x y : Octonion R) : (x - y).b = x.b - y.b

@[simp]

theorem TauCeti.Octonion.sub_v {R : Type u_1} [Sub R] (x y : Octonion R) : (x - y).v = x.v - y.v

@[simp]

theorem TauCeti.Octonion.sub_w {R : Type u_1} [Sub R] (x y : Octonion R) : (x - y).w = x.w - y.w

@[instance_reducible]

instance TauCeti.Octonion.instSMul {R : Type u_1} {S : Type u_2} [SMul S R] : SMul S (Octonion R)

Equations

• TauCeti.Octonion.instSMul = { smul := fun (s : S) (x : TauCeti.Octonion R) => { a := s • x.a, b := s • x.b, v := s • x.v, w := s • x.w } }

@[simp]

theorem TauCeti.Octonion.smul_a {R : Type u_1} {S : Type u_2} [SMul S R] (s : S) (x : Octonion R) : (s • x).a = s • x.a

@[simp]

theorem TauCeti.Octonion.smul_b {R : Type u_1} {S : Type u_2} [SMul S R] (s : S) (x : Octonion R) : (s • x).b = s • x.b

@[simp]

theorem TauCeti.Octonion.smul_v {R : Type u_1} {S : Type u_2} [SMul S R] (s : S) (x : Octonion R) : (s • x).v = s • x.v

@[simp]

theorem TauCeti.Octonion.smul_w {R : Type u_1} {S : Type u_2} [SMul S R] (s : S) (x : Octonion R) : (s • x).w = s • x.w

@[instance_reducible]

instance TauCeti.Octonion.instAddCommMonoid {R : Type u_1} [AddCommMonoid R] : AddCommMonoid (Octonion R)

Equations

• TauCeti.Octonion.instAddCommMonoid = Function.Injective.addCommMonoid (fun (x : TauCeti.Octonion R) => (x.a, x.b, x.v, x.w)) ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.Octonion.instAddCommGroup {R : Type u_1} [AddCommGroup R] : AddCommGroup (Octonion R)

Equations

• TauCeti.Octonion.instAddCommGroup = Function.Injective.addCommGroup (fun (x : TauCeti.Octonion R) => (x.a, x.b, x.v, x.w)) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[instance_reducible]

instance TauCeti.Octonion.instDistribMulAction {R : Type u_1} {S : Type u_2} [Monoid S] [AddCommMonoid R] [DistribMulAction S R] : DistribMulAction S (Octonion R)

Equations

• TauCeti.Octonion.instDistribMulAction = Function.Injective.distribMulAction { toFun := fun (x : TauCeti.Octonion R) => (x.a, x.b, x.v, x.w), map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[instance_reducible]

instance TauCeti.Octonion.instModule {R : Type u_1} {S : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] : Module S (Octonion R)

Equations

• TauCeti.Octonion.instModule = Function.Injective.module S { toFun := fun (x : TauCeti.Octonion R) => (x.a, x.b, x.v, x.w), map_zero' := ⋯, map_add' := ⋯ } ⋯ ⋯

@[instance_reducible]

instance TauCeti.Octonion.instAddCommGroupWithOneOfAddCommGroupOfOne {R : Type u_1} [AddCommGroup R] [One R] : AddCommGroupWithOne (Octonion R)

Equations

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

def TauCeti.Octonion.linearEquivProd (S : Type u_3) (R : Type u_4) [Semiring S] [AddCommMonoid R] [Module S R] : Octonion R ≃ₗ[S] R × R × (Fin 3 → R) × (Fin 3 → R)

The components of a vector matrix, as a linear isomorphism with the tuple of its four entries, over any semiring acting on the coefficients.

Equations

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

@[simp]

theorem TauCeti.Octonion.linearEquivProd_apply {R : Type u_1} {S : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] (x : Octonion R) : (linearEquivProd S R) x = (x.a, x.b, x.v, x.w)

@[simp]

theorem TauCeti.Octonion.linearEquivProd_symm_apply {R : Type u_1} {S : Type u_2} [Semiring S] [AddCommMonoid R] [Module S R] (p : R × R × (Fin 3 → R) × (Fin 3 → R)) : (linearEquivProd S R).symm p = { a := p.1, b := p.2.1, v := p.2.2.1, w := p.2.2.2 }

instance TauCeti.Octonion.instFree {R : Type u_1} [Semiring R] : Module.Free R (Octonion R)

instance TauCeti.Octonion.instFinite {R : Type u_1} [Semiring R] : Module.Finite R (Octonion R)

theorem TauCeti.Octonion.finrank_eq_eight (R : Type u_3) [Semiring R] [StrongRankCondition R] : Module.finrank R (Octonion R) = 8

The split octonions are 8-dimensional: two scalar and two vector entries.

The multiplication

@[instance_reducible]

instance TauCeti.Octonion.instMul {R : Type u_1} [CommRing R] : Mul (Octonion R)

The Zorn vector-matrix product: the matrix product of [[a, v], [w, b]] and [[a', v'], [w', b']], with the vector entries paired by the dot product and corrected by a cross product.

Equations

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

@[simp]

theorem TauCeti.Octonion.mul_a {R : Type u_1} [CommRing R] (x y : Octonion R) : (x * y).a = x.a * y.a + x.v ⬝ᵥ y.w

@[simp]

theorem TauCeti.Octonion.mul_b {R : Type u_1} [CommRing R] (x y : Octonion R) : (x * y).b = x.b * y.b + x.w ⬝ᵥ y.v

@[simp]

theorem TauCeti.Octonion.mul_v {R : Type u_1} [CommRing R] (x y : Octonion R) : (x * y).v = x.a • y.v + y.b • x.v - (crossProduct x.w) y.w

@[simp]

theorem TauCeti.Octonion.mul_w {R : Type u_1} [CommRing R] (x y : Octonion R) : (x * y).w = y.a • x.w + x.b • y.w + (crossProduct x.v) y.v

@[instance_reducible]

instance TauCeti.Octonion.instNonAssocRing {R : Type u_1} [CommRing R] : NonAssocRing (Octonion R)

Equations

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

instance TauCeti.Octonion.instSMulCommClass {R : Type u_1} [CommRing R] : SMulCommClass R (Octonion R) (Octonion R)

instance TauCeti.Octonion.instIsScalarTower {R : Type u_1} [CommRing R] : IsScalarTower R (Octonion R) (Octonion R)

Conjugation, trace and norm

def TauCeti.Octonion.conj {R : Type u_1} [CommRing R] : Octonion R →ₗ[R] Octonion R

Octonion conjugation ⟨a, b, v, w⟩ ↦ ⟨b, a, -v, -w⟩: it exchanges the two diagonal entries and negates the two vector entries, so it fixes 1 and negates the imaginary part.

Equations

• TauCeti.Octonion.conj = { toFun := fun (x : TauCeti.Octonion R) => { a := x.b, b := x.a, v := -x.v, w := -x.w }, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Octonion.conj_a {R : Type u_1} [CommRing R] (x : Octonion R) : (conj x).a = x.b

@[simp]

theorem TauCeti.Octonion.conj_b {R : Type u_1} [CommRing R] (x : Octonion R) : (conj x).b = x.a

@[simp]

theorem TauCeti.Octonion.conj_v {R : Type u_1} [CommRing R] (x : Octonion R) : (conj x).v = -x.v

@[simp]

theorem TauCeti.Octonion.conj_w {R : Type u_1} [CommRing R] (x : Octonion R) : (conj x).w = -x.w

@[simp]

theorem TauCeti.Octonion.conj_conj {R : Type u_1} [CommRing R] (x : Octonion R) : conj (conj x) = x

@[simp]

theorem TauCeti.Octonion.conj_one {R : Type u_1} [CommRing R] : conj 1 = 1

@[simp]

theorem TauCeti.Octonion.conj_mul {R : Type u_1} [CommRing R] (x y : Octonion R) : conj (x * y) = conj y * conj x

Conjugation is an anti-automorphism: it reverses products.

def TauCeti.Octonion.trace {R : Type u_1} [CommRing R] : Octonion R →ₗ[R] R

The trace ⟨a, b, v, w⟩ ↦ a + b of a vector matrix, the coefficient of the rank-two equation TauCeti.Octonion.mul_self.

Equations

• TauCeti.Octonion.trace = { toFun := fun (x : TauCeti.Octonion R) => x.a + x.b, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem TauCeti.Octonion.trace_apply {R : Type u_1} [CommRing R] (x : Octonion R) : trace x = x.a + x.b

theorem TauCeti.Octonion.trace_one {R : Type u_1} [CommRing R] : trace 1 = 2

The trace of 1 is 2, not 1: the identity vector matrix has two diagonal entries. Not a simp lemma, because TauCeti.Octonion.trace_apply already takes its left-hand side apart.

theorem TauCeti.Octonion.add_conj {R : Type u_1} [CommRing R] (x : Octonion R) : x + conj x = trace x • 1

An octonion and its conjugate add up to a scalar: the trace.

theorem TauCeti.Octonion.conj_eq_trace_smul_one_sub {R : Type u_1} [CommRing R] (x : Octonion R) : conj x = trace x • 1 - x

Conjugation is reflection in the trace: conj x = trace x • 1 - x.

theorem TauCeti.Octonion.trace_conj {R : Type u_1} [CommRing R] (x : Octonion R) : trace (conj x) = trace x

Conjugation preserves the trace: it only exchanges the two diagonal entries. Not a simp lemma, for the same reason as TauCeti.Octonion.trace_one.

theorem TauCeti.Octonion.trace_mul_comm {R : Type u_1} [CommRing R] (x y : Octonion R) : trace (x * y) = trace (y * x)

The trace is symmetric in a product: trace (x * y) = trace (y * x), since the two dot products of a Zorn product are exchanged when the factors are. Not a simp lemma, for the same reason as TauCeti.Octonion.trace_one.

def TauCeti.Octonion.norm {R : Type u_1} [CommRing R] (x : Octonion R) : R

The norm ⟨a, b, v, w⟩ ↦ a * b - v ⬝ᵥ w of a vector matrix: the determinant of the matrix, and the norm form of the composition algebra 𝕆.

Equations

• x.norm = x.a * x.b - x.v ⬝ᵥ x.w

theorem TauCeti.Octonion.norm_def {R : Type u_1} [CommRing R] (x : Octonion R) : x.norm = x.a * x.b - x.v ⬝ᵥ x.w

@[simp]

theorem TauCeti.Octonion.norm_one {R : Type u_1} [CommRing R] : norm 1 = 1

@[simp]

theorem TauCeti.Octonion.norm_zero {R : Type u_1} [CommRing R] : norm 0 = 0

@[simp]

theorem TauCeti.Octonion.norm_conj {R : Type u_1} [CommRing R] (x : Octonion R) : (conj x).norm = x.norm

@[simp]

theorem TauCeti.Octonion.norm_neg {R : Type u_1} [CommRing R] (x : Octonion R) : (-x).norm = x.norm

The norm is even: negating an octonion negates both its scalar and both its vector entries, so each of the two products making up the norm is unchanged.

@[simp]

theorem TauCeti.Octonion.norm_smul {R : Type u_1} [CommRing R] (r : R) (x : Octonion R) : (r • x).norm = r ^ 2 * x.norm

The norm is homogeneous of degree two: rescaling an octonion by r rescales its norm by r ^ 2.

@[simp]

theorem TauCeti.Octonion.self_mul_conj {R : Type u_1} [CommRing R] (x : Octonion R) : x * conj x = x.norm • 1

x * conj x = N x • 1: conjugation inverts an octonion up to its norm.

@[simp]

theorem TauCeti.Octonion.conj_mul_self {R : Type u_1} [CommRing R] (x : Octonion R) : conj x * x = x.norm • 1

conj x * x = N x • 1, the mirror of TauCeti.Octonion.self_mul_conj.

theorem TauCeti.Octonion.mul_self {R : Type u_1} [CommRing R] (x : Octonion R) : x * x = trace x • x - x.norm • 1

The rank-two equation. Every split octonion satisfies x² - trace x · x + N x · 1 = 0, so it generates a subalgebra of dimension at most 2.

@[simp]

theorem TauCeti.Octonion.norm_mul {R : Type u_1} [CommRing R] (x y : Octonion R) : (x * y).norm = x.norm * y.norm

The norm of a split octonion is multiplicative, so 𝕆 is a composition algebra.

The norm as a quadratic form

def TauCeti.Octonion.normQuadraticForm (R : Type u_3) [CommRing R] : QuadraticForm R (Octonion R)

The norm is a quadratic form. Its companion is the bilinear map (x, y) ↦ a b' + a' b - v ⬝ᵥ w' - v' ⬝ᵥ w, the polarization of the determinant of a vector matrix. Packaging the norm this way makes Mathlib's QuadraticMap.polar API — symmetry, bilinearity in each argument, and QuadraticMap.polar_self — available for the associated symmetric form, which is what the Hermitian matrix algebras over 𝕆 are built from.

Equations

• TauCeti.Octonion.normQuadraticForm R = QuadraticMap.ofPolar TauCeti.Octonion.norm ⋯ ⋯ ⋯

@[simp]

theorem TauCeti.Octonion.normQuadraticForm_apply {R : Type u_1} [CommRing R] (x : Octonion R) : (normQuadraticForm R) x = x.norm

theorem TauCeti.Octonion.polar_normQuadraticForm {R : Type u_1} [CommRing R] (x y : Octonion R) : QuadraticMap.polar (⇑(normQuadraticForm R)) x y = x.a * y.b + y.a * x.b - x.v ⬝ᵥ y.w - y.v ⬝ᵥ x.w

The polar form of the norm, read off the entries of the two vector matrices. Stated for QuadraticMap.polar rather than for QuadraticMap.polarBilin, which simp unfolds to it. Not a simp lemma: the polar form and its half QuadraticMap.associated are the interface the Hermitian matrix algebras are stated against, and simp should not take it apart into coordinates behind their backs.

theorem TauCeti.Octonion.polar_normQuadraticForm_conj {R : Type u_1} [CommRing R] (x y : Octonion R) : QuadraticMap.polar (⇑(normQuadraticForm R)) (conj x) (conj y) = QuadraticMap.polar (⇑(normQuadraticForm R)) x y

The polar form of the norm is unchanged by conjugating both arguments: conjugation is additive and preserves the norm.

theorem TauCeti.Octonion.trace_mul_conj {R : Type u_1} [CommRing R] (x y : Octonion R) : trace (x * conj y) = QuadraticMap.polar (⇑(normQuadraticForm R)) x y

The polar form of the norm is the trace form (x, y) ↦ trace (x * conj y): the two descriptions of the symmetric bilinear form of a composition algebra agree.

theorem TauCeti.Octonion.mul_conj_add_mul_conj {R : Type u_1} [CommRing R] (x y : Octonion R) : x * conj y + y * conj x = QuadraticMap.polar (⇑(normQuadraticForm R)) x y • 1

The polar form of the norm is visible inside the algebra: x * conj y + y * conj x is the scalar QuadraticMap.polar (normQuadraticForm R) x y · 1. Together with TauCeti.Octonion.self_mul_conj, which is the case y = x up to a factor of 2, this is what makes the symmetric form of a composition algebra an algebraic, not merely a quadratic, datum.

The mirror form conj x * y + conj y * x is this identity at (conj x, conj y), read through TauCeti.Octonion.conj_conj and TauCeti.Octonion.polar_normQuadraticForm_conj: simpa [polar_normQuadraticForm_conj] using mul_conj_add_mul_conj (conj x) (conj y).

Alternativity

@[simp]

theorem TauCeti.Octonion.left_alternative {R : Type u_1} [CommRing R] (x y : Octonion R) : x * x * y = x * (x * y)

The split octonions are left alternative: x * x * y = x * (x * y).

@[simp]

theorem TauCeti.Octonion.right_alternative {R : Type u_1} [CommRing R] (x y : Octonion R) : x * y * y = x * (y * y)

The split octonions are right alternative: x * y * y = x * (y * y).

The Moufang identities

The two Moufang identities proved directly are the one place where the vector simp set above does not suffice. Reducing them with it leaves obligations that hold only because the vector entries have three coordinates and that Mathlib does not name: the vanishing of v ⬝ᵥ u ⨯₃ w + w ⬝ᵥ u ⨯₃ v at the scalar entries, and a relation between a triple product and the entries themselves at the vector entries. Both are therefore proved in coordinates: dot products are expanded by Mathlib's Matrix.vec3_dotProduct, cross products by Mathlib's Matrix.cross_apply. The latter rewrites u ⨯₃ t to a ![…] literal, and such a literal meeting the generic vector entries of a product fires Matrix.sub_cons, Matrix.head_add and Matrix.dotProduct_cons, which re-express the coordinates as vecHead/vecTail towers; unfolding those two definitions turns the towers back into the coordinates u 0, u 1, u 2, so that ring sees one atom per coordinate.

theorem TauCeti.Octonion.moufang_left {R : Type u_1} [CommRing R] (x y z : Octonion R) : z * x * z * y = z * (x * (z * y))

The left Moufang identity: (z * x * z) * y = z * (x * (z * y)).

theorem TauCeti.Octonion.flexible {R : Type u_1} [CommRing R] (x y : Octonion R) : x * y * x = x * (y * x)

The flexible law: x * y * x = x * (y * x), so the two bracketings of x * y * x agree.

theorem TauCeti.Octonion.moufang_right {R : Type u_1} [CommRing R] (x y z : Octonion R) : x * (z * y * z) = x * z * y * z

The right Moufang identity: x * (z * y * z) = ((x * z) * y) * z.

theorem TauCeti.Octonion.moufang_middle {R : Type u_1} [CommRing R] (x y z : Octonion R) : z * x * (y * z) = z * (x * y) * z

The middle Moufang identity: (z * x) * (y * z) = (z * (x * y)) * z.

Worked examples: Octonion ℤ is neither commutative nor associative

Alternativity is as much associativity as 𝕆 has, and the two vector entries are what break the rest: [[0, e₀], [0, 0]] · [[0, e₁], [0, 0]] picks up the cross product e₀ ⨯₃ e₁ = e₂ in its bottom-left entry, and the opposite product picks up e₁ ⨯₃ e₀ = -e₂. The two examples below run this over ℤ, so they witness both failures for that base ring rather than for every R; over the zero ring Octonion R is of course commutative and associative.

The imaginary octonions

def TauCeti.Octonion.imaginary (R : Type u_3) [CommRing R] : Submodule R (Octonion R)

The imaginary octonions, the trace-zero subspace of 𝕆. It is 7-dimensional (TauCeti.Octonion.finrank_imaginary) and, over a field in which 2 is nonzero, an irreducible representation of G₂ = Der 𝕆 by TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule -- where Der 𝕆 is TauCeti.derivationLieAlgebra R (Octonion R), of rank 14 by TauCeti.Octonion.finrank_derivationLieAlgebra. The isomorphism of Der 𝕆 with LieAlgebra.g₂ is not proved in the repository.

Equations

• TauCeti.Octonion.imaginary R = TauCeti.Octonion.trace.ker

@[simp]

theorem TauCeti.Octonion.mem_imaginary {R : Type u_1} [CommRing R] {x : Octonion R} : x ∈ imaginary R ↔ trace x = 0

theorem TauCeti.Octonion.mem_imaginary_iff_conj_eq_neg {R : Type u_1} [CommRing R] {x : Octonion R} : x ∈ imaginary R ↔ conj x = -x

Conjugation negates exactly the imaginary octonions: conj x = -x if and only if x has vanishing trace. Not a simp lemma, because TauCeti.Octonion.mem_imaginary already takes its left-hand side apart.

theorem TauCeti.Octonion.trace_surjective {R : Type u_1} [CommRing R] : Function.Surjective ⇑trace

The trace is a surjection onto the base ring: it already is on the scalar diagonal.

theorem TauCeti.Octonion.finrank_imaginary (R : Type u_3) [CommRing R] [StrongRankCondition R] : Module.finrank R ↥(imaginary R) = 7

The imaginary split octonions are 7-dimensional: a vanishing trace pins the second diagonal entry to b = -a, leaving the entries a, v and w free.