The imaginary octonions are the fundamental representation of G₂ = Der 𝕆

TauCeti/Algebra/Octonion/Derivation.lean builds the derivation algebra Der 𝕆 of the split octonions, shows that it is 14-dimensional, and exhibits the imaginary octonions TauCeti.Octonion.imaginaryLieSubmodule as a 7-dimensional Lie submodule of 𝕆 on which it acts faithfully. That makes Im 𝕆 the candidate fundamental representation of G₂. This file proves that it really is one: over a field in which 2 is nonzero, Im 𝕆 is an irreducible representation of Der 𝕆 (TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule), of dimension 7 by TauCeti.Octonion.finrank_imaginary.

The whole argument runs on two of the three explicit families of derivations of TauCeti/Algebra/Octonion/Derivation.lean, the vector families TauCeti.Octonion.upperDerivation and TauCeti.Octonion.lowerDerivation, and never mentions the 𝔰𝔩₃ family. Write ε = ⟨1, -1, 0, 0⟩ for the imaginary part of the diagonal idempotent of 𝕆, the one imaginary direction on the scalar diagonal. The two computations that do the work are iterations of a single vector derivation:

• applying upperDerivation u twice kills every entry but the upper vector one, where it leaves -2 ⟨u, w⟩ · u, so one more lowerDerivation t lands on the line through ε (TauCeti.Octonion.lowerDerivation_upperDerivation_upperDerivation_apply), with coefficient 2 ⟨u, w⟩ ⟨t, u⟩;
• symmetrically for lowerDerivation twice followed by upperDerivation (TauCeti.Octonion.upperDerivation_lowerDerivation_lowerDerivation_apply), with coefficient 2 ⟨t, v⟩ ⟨u, t⟩.

Taking u = t a standard basis vector makes the coefficient 2 wᵢ, respectively 2 vᵢ. So a Lie submodule containing a nonzero imaginary octonion contains ε: if some lower coordinate wᵢ is nonzero the first computation produces a nonzero multiple of ε, if some upper coordinate vᵢ is nonzero the second does, and if all of them vanish the octonion is already a nonzero multiple of ε. Conversely ε generates: upperDerivation u and lowerDerivation t send ε to the upper vector 2 u and the lower vector 2 t, so with 2 invertible every imaginary octonion ⟨a, -a, v, w⟩ is a · ε plus the images of ε under the two derivations attached to 2⁻¹ v and 2⁻¹ w. Together these two directions say that Im 𝕆 is a minimal nonzero Lie submodule of 𝕆 (TauCeti.Octonion.eq_imaginaryLieSubmodule_of_le_of_ne_bot), which is irreducibility.

Some hypothesis on 2 is necessary for irreducibility: where 2 vanishes so does trace 1, so 1 is imaginary, and a derivation kills 1, so the line through 1 is a Lie submodule of Im 𝕆 different from 0 and from Im 𝕆. That is TauCeti.Octonion.not_isIrreducible_imaginaryLieSubmodule_of_two_eq_zero, proved below over every nontrivial base ring in which 2 vanishes, so the hypothesis is not an artefact of the argument. Faithfulness, however, holds over every commutative ring by TauCeti.Octonion.isFaithful_imaginaryLieSubmodule.

Main results

• TauCeti.Octonion.lowerDerivation_upperDerivation_upperDerivation_apply and TauCeti.Octonion.upperDerivation_lowerDerivation_lowerDerivation_apply: three vector derivations, applied to an arbitrary octonion, land on the line through ε = ⟨1, -1, 0, 0⟩, with the coefficients displayed above.
• TauCeti.Octonion.imaginaryLieSubmodule_le_of_mem: a Lie submodule of 𝕆 containing ε contains every imaginary octonion, as soon as 2 is invertible.
• TauCeti.Octonion.diagonal_mem_of_mem_of_trace_eq_zero: over a field in which 2 is nonzero, a Lie submodule of 𝕆 containing a nonzero imaginary octonion contains ε.
• TauCeti.Octonion.eq_imaginaryLieSubmodule_of_le_of_ne_bot: Im 𝕆 is a minimal nonzero Lie submodule of 𝕆.
• TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule: Im 𝕆 is an irreducible representation of Der 𝕆, with TauCeti.Octonion.instIsIrreducibleImaginaryLieSubmodule its instance form.
• TauCeti.Octonion.not_isIrreducible_imaginaryLieSubmodule_of_two_eq_zero: and it is reducible where 2 vanishes, so the hypothesis on 2 is necessary.

Implementation notes

The element ε is spelled out as the vector-matrix literal ⟨1, -1, 0, 0⟩ rather than given a name of its own: it occurs only as the right-hand side of the two computations and as the generator in the statements above, and TauCeti/Algebra/Octonion/Basic.lean names no other individual octonion either.

The computational lemmas are stated over a commutative ring and for an arbitrary octonion, not only an imaginary one; nothing in them needs the trace to vanish. Invertibility of 2 enters only in the generation lemma, and a field only where a nonzero coefficient has to be inverted, so the two halves of minimality carry different hypotheses. The minimality statement is made for Lie submodules of 𝕆 itself, which is where the derivations act; irreducibility of the subtype ↥(Im 𝕆) is read off it by pushing a Lie submodule of the subtype forward along LieSubmodule.incl, which is injective.

References

The identification of Der 𝕆 with the split LieAlgebra.g₂ and its type-G₂ Killing-simplicity are not proved here.

• T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, §2.
• J. C. Baez, The octonions, Bull. Amer. Math. Soc. 39 (2002), §4.1.

Iterating a vector derivation

theorem TauCeti.Octonion.upperDerivation_upperDerivation_apply {R : Type u_1} [CommRing R] (u : Fin 3 → R) (x : Octonion R) : ↑(upperDerivation u) (↑(upperDerivation u) x) = { a := 0, b := 0, v := -(2 * u ⬝ᵥ x.w) • u, w := 0 }

Applying TauCeti.Octonion.upperDerivation u twice kills every entry but the upper vector one, where it leaves -2 ⟨u, w⟩ · u: the two cross-product terms vanish because u ⨯₃ u = 0 and u ⬝ᵥ (u ⨯₃ v) = 0.

theorem TauCeti.Octonion.lowerDerivation_lowerDerivation_apply {R : Type u_1} [CommRing R] (t : Fin 3 → R) (x : Octonion R) : ↑(lowerDerivation t) (↑(lowerDerivation t) x) = { a := 0, b := 0, v := 0, w := -(2 * t ⬝ᵥ x.v) • t }

Applying TauCeti.Octonion.lowerDerivation t twice kills every entry but the lower vector one, where it leaves -2 ⟨t, v⟩ · t: the two cross-product terms vanish because t ⨯₃ t = 0 and t ⬝ᵥ (t ⨯₃ w) = 0. This statement is the mirror image of TauCeti.Octonion.upperDerivation_upperDerivation_apply.

theorem TauCeti.Octonion.lowerDerivation_upperDerivation_upperDerivation_apply {R : Type u_1} [CommRing R] (t u : Fin 3 → R) (x : Octonion R) : ↑(lowerDerivation t) (↑(upperDerivation u) (↑(upperDerivation u) x)) = (2 * u ⬝ᵥ x.w * t ⬝ᵥ u) • { a := 1, b := -1, v := 0, w := 0 }

Two upper vector derivations and one lower one land on the diagonal imaginary line. The double upper derivation of TauCeti.Octonion.upperDerivation_upperDerivation_apply leaves a pure upper vector, which a lower derivation turns into a multiple of ε = ⟨1, -1, 0, 0⟩.

theorem TauCeti.Octonion.upperDerivation_lowerDerivation_lowerDerivation_apply {R : Type u_1} [CommRing R] (u t : Fin 3 → R) (x : Octonion R) : ↑(upperDerivation u) (↑(lowerDerivation t) (↑(lowerDerivation t) x)) = (2 * t ⬝ᵥ x.v * u ⬝ᵥ t) • { a := 1, b := -1, v := 0, w := 0 }

Two lower vector derivations and one upper one land on the diagonal imaginary line. The double lower derivation of TauCeti.Octonion.lowerDerivation_lowerDerivation_apply leaves a pure lower vector, which an upper derivation turns into the multiple 2 ⟨t, v⟩ ⟨u, t⟩ of ε = ⟨1, -1, 0, 0⟩; these statements are the mirror images of TauCeti.Octonion.lowerDerivation_upperDerivation_upperDerivation_apply and its inputs.

theorem TauCeti.Octonion.upperDerivation_apply_diagonal {R : Type u_1} [CommRing R] (u : Fin 3 → R) : ↑(upperDerivation u) { a := 1, b := -1, v := 0, w := 0 } = { a := 0, b := 0, v := 2 • u, w := 0 }

An upper vector derivation moves ε = ⟨1, -1, 0, 0⟩ onto the upper vector 2 u: the diagonal entries of ε differ by 2, and its vector entries vanish.

theorem TauCeti.Octonion.lowerDerivation_apply_diagonal {R : Type u_1} [CommRing R] (t : Fin 3 → R) : ↑(lowerDerivation t) { a := 1, b := -1, v := 0, w := 0 } = { a := 0, b := 0, v := 0, w := 2 • t }

A lower vector derivation moves ε = ⟨1, -1, 0, 0⟩ onto the lower vector 2 t, the mirror image of the statement TauCeti.Octonion.upperDerivation_apply_diagonal.

ε generates the imaginary octonions

theorem TauCeti.Octonion.imaginaryLieSubmodule_le_of_mem {R : Type u_1} [CommRing R] [Invertible 2] {N : LieSubmodule R (↥(derivationLieAlgebra R (Octonion R))) (Octonion R)} (h : { a := 1, b := -1, v := 0, w := 0 } ∈ N) : imaginaryLieSubmodule R ≤ N

ε = ⟨1, -1, 0, 0⟩ generates the imaginary octonions. A Lie submodule of 𝕆 containing ε contains every imaginary octonion: writing x = ⟨a, -a, v, w⟩, the three summands of x = a · ε + D₊ ε + D₋ ε for the vector derivations D₊, D₋ attached to ⅟2 • v and ⅟2 • w are all in the submodule, by TauCeti.Octonion.upperDerivation_apply_diagonal and TauCeti.Octonion.lowerDerivation_apply_diagonal.

Minimality and irreducibility

theorem TauCeti.Octonion.diagonal_mem_of_mem_of_trace_eq_zero {K : Type u_1} [Field K] {N : LieSubmodule K (↥(derivationLieAlgebra K (Octonion K))) (Octonion K)} (h2 : 2 ≠ 0) {x : Octonion K} (hxN : x ∈ N) (hx : trace x = 0) (hx0 : x ≠ 0) : { a := 1, b := -1, v := 0, w := 0 } ∈ N

A Lie submodule of 𝕆 containing a nonzero imaginary octonion contains ε = ⟨1, -1, 0, 0⟩. If some lower coordinate of x is nonzero, TauCeti.Octonion.lowerDerivation_upperDerivation_upperDerivation_apply at the matching standard basis vector produces the nonzero multiple 2 x.w i · ε; if some upper coordinate is nonzero, TauCeti.Octonion.upperDerivation_lowerDerivation_lowerDerivation_apply does; and if both vector entries vanish then x is already x.a · ε with x.a ≠ 0.

theorem TauCeti.Octonion.eq_imaginaryLieSubmodule_of_le_of_ne_bot {K : Type u_1} [Field K] {N : LieSubmodule K (↥(derivationLieAlgebra K (Octonion K))) (Octonion K)} (h2 : 2 ≠ 0) (hle : N ≤ imaginaryLieSubmodule K) (hne : N ≠ ⊥) : N = imaginaryLieSubmodule K

The imaginary octonions are a minimal nonzero Lie submodule of 𝕆. A nonzero Lie submodule contained in Im 𝕆 contains ε = ⟨1, -1, 0, 0⟩ by TauCeti.Octonion.diagonal_mem_of_mem_of_trace_eq_zero, hence all of Im 𝕆 by TauCeti.Octonion.imaginaryLieSubmodule_le_of_mem.

theorem TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule {K : Type u_1} [Field K] (h2 : 2 ≠ 0) : LieModule.IsIrreducible K ↥(derivationLieAlgebra K (Octonion K)) ↥(imaginaryLieSubmodule K)

The imaginary octonions are an irreducible representation of Der 𝕆. Over a field in which 2 is nonzero the 7-dimensional Lie submodule Im 𝕆 of TauCeti/Algebra/Octonion/Derivation.lean is irreducible, so together with TauCeti.Octonion.finrank_imaginary and TauCeti.Octonion.isFaithful_imaginaryLieSubmodule it is the 7-dimensional fundamental representation of G₂ = Der 𝕆.

Where 2 vanishes the statement fails, by TauCeti.Octonion.not_isIrreducible_imaginaryLieSubmodule_of_two_eq_zero: there 1 is imaginary and is killed by every derivation, so it spans a Lie submodule of Im 𝕆 that is neither ⊥ nor ⊤.

instance TauCeti.Octonion.instIsIrreducibleImaginaryLieSubmodule {K : Type u_1} [Field K] [NeZero 2] : LieModule.IsIrreducible K ↥(derivationLieAlgebra K (Octonion K)) ↥(imaginaryLieSubmodule K)

The imaginary octonions are an irreducible representation of Der 𝕆, the instance form of TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule.

The hypothesis on 2 is necessary

theorem TauCeti.Octonion.not_isIrreducible_imaginaryLieSubmodule_of_two_eq_zero {R : Type u_1} [CommRing R] [Nontrivial R] (h2 : 2 = 0) : ¬LieModule.IsIrreducible R ↥(derivationLieAlgebra R (Octonion R)) ↥(imaginaryLieSubmodule R)

In characteristic 2 the imaginary octonions are reducible, so the hypothesis 2 ≠ 0 of TauCeti.Octonion.isIrreducible_imaginaryLieSubmodule cannot be dropped. Where 2 vanishes so does trace 1, making 1 imaginary; a derivation kills 1 (TauCeti.derivationLieAlgebra.apply_one_eq_zero), so 1 lies in the largest submodule LieModule.maxTrivSubmodule on which Der 𝕆 acts trivially, which therefore meets Im 𝕆 in more than 0. It does not contain all of Im 𝕆: a lower vector derivation moves the imaginary octonion ⟨0, 0, e₀, 0⟩ onto -ε, which is nonzero.