The octonions as a real vector space

CompositionAlgebras/Octonions.lean gives Octonion bare Zero/Add/Neg/SMul ℝ and Mul instances and no bundled algebraic class (no AddCommGroup, no Module). This file supplies AddCommGroup Octonion, Module ℝ Octonion, FiniteDimensional ℝ Octonion, finrank ℝ 𝕆 = 8, linearity of conjugation, and the Euclidean form octIp.

Every module data field is the pre-existing instance on the nose, so no +, • or 0 in the octonion file changes meaning and its @[simp] coordinate lemmas keep firing. They live here rather than in Octonions.lean only to keep that file untouched.

Composition/Instances.lean needs exactly this: without AddCommGroup and Module ℝ there is no Module ℝ Octonion for CompositionAlgebra Octonion to be stated over.

Main definitions

• Octonion.octIp -- the Euclidean inner product on 𝕆
• Octonion.coordsEquiv -- 𝕆 ≃ₗ[ℝ] (Fin 8 → ℝ)

Main results

• Octonion.octIp_eq_re -- ⟨x, y⟩ = re (x * conj y), the bridge to OctonionTrace.lean
• Octonion.re_three_cyc -- cyclic invariance of re ((x y) z)
• Octonion.finrank_eq_eight -- finrank ℝ 𝕆 = 8

Octonion as an ℝ-module

@[instance_reducible]

instance Octonion.instAddCommGroup : AddCommGroup Octonion

Equations

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

@[instance_reducible]

instance Octonion.instModule : Module ℝ Octonion

Equations

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

@[simp]

theorem Octonion.conj_zero : conj 0 = 0

@[simp]

theorem Octonion.conj_add (x y : Octonion) : (x + y).conj = x.conj + y.conj

Conjugation is additive.

@[simp]

theorem Octonion.conj_smul (r : ℝ) (x : Octonion) : (r • x).conj = r • x.conj

Conjugation is ℝ-homogeneous; with conj_add, conj is ℝ-linear.

@[simp]

theorem Octonion.mul_zero' (x : Octonion) : x.mul 0 = 0

@[simp]

theorem Octonion.zero_mul' (x : Octonion) : mul 0 x = 0

The Euclidean inner product on 𝕆

octIp x y = ∑ᵢ xᵢ yᵢ is the standard positive-definite form. octIp_eq_re identifies it with the trace form re (x * conj y) of OctonionTrace.lean, which is how the cyclic identities there reach the trace form on hermitian octonionic matrices.

def Octonion.octIp (x y : Octonion) : ℝ

The Euclidean inner product on the octonions.

Equations

• x.octIp y = ∑ i : Fin 8, x.coords i * y.coords i

theorem Octonion.octIp_comm (x y : Octonion) : x.octIp y = y.octIp x

@[simp]

theorem Octonion.octIp_add_left (x y z : Octonion) : (x + y).octIp z = x.octIp z + y.octIp z

@[simp]

theorem Octonion.octIp_smul_left (r : ℝ) (x y : Octonion) : (r • x).octIp y = r * x.octIp y

@[simp]

theorem Octonion.octIp_add_right (x y z : Octonion) : x.octIp (y + z) = x.octIp y + x.octIp z

@[simp]

theorem Octonion.octIp_smul_right (r : ℝ) (x y : Octonion) : x.octIp (r • y) = r * x.octIp y

@[simp]

theorem Octonion.octIp_zero_left (x : Octonion) : octIp 0 x = 0

@[simp]

theorem Octonion.octIp_zero_right (x : Octonion) : x.octIp 0 = 0

theorem Octonion.octIp_self_nonneg (x : Octonion) : 0 ≤ x.octIp x

theorem Octonion.octIp_self_eq_zero {x : Octonion} (h : x.octIp x = 0) : x = 0

theorem Octonion.octIp_eq_re (x y : Octonion) : x.octIp y = (x.mul y.conj).re

The Euclidean inner product is the trace form: ⟨x, y⟩ = re (x * conj y). This is the bridge to OctonionTrace.lean.

theorem Octonion.re_three_cyc (x y z : Octonion) : ((x.mul y).mul z).re = ((y.mul z).mul x).re

Cyclic invariance of the real part of a triple product. re_mul_assoc moves the bracket, re_mul_comm rotates the factors.

theorem Octonion.octIp_conj_cyc (a b c : Octonion) : (a.conj.mul b.conj).octIp c = (b.conj.mul c.conj).octIp a

Cyclic rotation of a conjugated triple, in the octIp vocabulary the trace form on hermitian octonionic matrices is written in. This and octIp_conj_cyc' are the only octonionic input that form's Euclidean hypothesis needs.

theorem Octonion.octIp_conj_cyc' (a b c : Octonion) : (a.conj.mul b.conj).octIp c = (c.conj.mul a.conj).octIp b

Cyclic rotation the other way.

def Octonion.coordsEquiv : Octonion ≃ₗ[ℝ] Fin 8 → ℝ

Coordinates of an octonion, as a linear equivalence with Fin 8 → ℝ.

Equations

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

instance Octonion.instFiniteDimensional : FiniteDimensional ℝ Octonion

theorem Octonion.finrank_eq_eight : Module.finrank ℝ Octonion = 8

The octonions are 8-dimensional over ℝ.