Derivations of the split Albert algebra

F₄ is the derivation algebra of the split Albert algebra J = H₃(𝕆), and over a field its 26-dimensional fundamental representation is supposed to be the trace-zero subspace J₀. Neither statement can be made until one knows that a derivation of J lands in J₀; that is what this file proves.

Write Fⱼ(a) for the Hermitian matrix whose only nonzero entry is the octonion a in position (j + 1, j + 2) (TauCeti.AlbertAlgebra.offDiagSingle). Together with the diagonal frame E₀, E₁, E₂ of TauCeti/Algebra/AlbertAlgebra/Basic.lean the slots span J (TauCeti.AlbertAlgebra.eq_sum_smul_diagIdempotent_add_sum_offDiagSingle), and the trace of a derivation is killed on each kind of generator separately; on a diagonal idempotent more is true, D Eᵢ has no diagonal at all (TauCeti.AlbertAlgebra.derivation_apply_diagIdempotent_diag_eq_zero). Only the Peirce calculus of the frame enters, so no Jordan identity is needed — which is just as well, since J is not yet known here to satisfy one.

The trace-zero subspace is therefore a Lie submodule (TauCeti.AlbertAlgebra.traceZeroLieSubmodule), the candidate fundamental representation, of dimension 26 over a base satisfying StrongRankCondition (TauCeti.AlbertAlgebra.finrank_traceZeroLieSubmodule); Der J acts faithfully on it whenever scalar multiplication by 3 on J is regular (TauCeti.AlbertAlgebra.isFaithful_traceZeroLieSubmodule).

Main definitions

• TauCeti.AlbertAlgebra.traceZeroLieSubmodule: the trace-zero subspace J₀ as a Lie submodule of J over Der J, so that J₀ is a representation of Der J, with TauCeti.AlbertAlgebra.finrank_traceZeroLieSubmodule its dimension 26 over a base satisfying StrongRankCondition.

Main results

• TauCeti.AlbertAlgebra.derivation_apply_diagIdempotent_diag_eq_zero: the value of a derivation at a diagonal idempotent has vanishing diagonal.
• TauCeti.AlbertAlgebra.trace_derivation_apply_eq_zero: a derivation of J has values of trace 0, with TauCeti.AlbertAlgebra.derivation_apply_mem_traceZero its membership form.
• TauCeti.AlbertAlgebra.isFaithful_traceZeroLieSubmodule: when scalar multiplication by 3 on J is regular, Der J acts faithfully on J₀; TauCeti.AlbertAlgebra.instIsFaithfulTraceZeroLieSubmodule is the instance form of that, under [NoZeroSMulDivisors R (AlbertAlgebra R)] and [NeZero (3 : R)].

Implementation notes

Everything is stated over a commutative ring in which 2 is invertible, the hypothesis the symmetrized product already carries; the base is a field nowhere. Faithfulness is stated for the exact hypothesis it needs, IsSMulRegular (AlbertAlgebra R) (3 : R), which is not a class; the instance form asks instead for [NoZeroSMulDivisors R (AlbertAlgebra R)] and [NeZero (3 : R)], which imply it but are strictly stronger. Some hypothesis on 3 is unavoidable: in characteristic 3 the trace-zero element 3 • A - (tr A) • 1 degenerates to -(tr A) • 1, which retains no information about A.

Derivations are taken in the bundled form D : TauCeti.derivationLieAlgebra R (AlbertAlgebra R) of TauCeti/Algebra/Lie/Derivation/Basic.lean, and are applied through the coercion (D : Module.End R (AlbertAlgebra R)).

References

• TauCeti/Algebra/Octonion/Derivation.lean, the G₂ = Der(𝕆) counterpart of this file, from which the packaging of the invariant subspace is adapted: TauCeti.Octonion.imaginaryLieSubmodule, TauCeti.Octonion.isFaithful_imaginaryLieSubmodule and TauCeti.Octonion.instIsFaithfulImaginaryLieSubmodule — the imaginary octonions as a Lie submodule over Der 𝕆, faithful over every commutative ring — are the models for TauCeti.AlbertAlgebra.traceZeroLieSubmodule, TauCeti.AlbertAlgebra.isFaithful_traceZeroLieSubmodule and TauCeti.AlbertAlgebra.instIsFaithfulTraceZeroLieSubmodule here. The trace computation itself is not adapted from it: there the argument is the skewness of a derivation for the norm form, here it is the Peirce calculus of the diagonal frame.
• T. A. Springer and F. D. Veldkamp, Octonions, Jordan Algebras and Exceptional Groups, §5.
• N. Jacobson, Structure and Representations of Jordan Algebras, Ch. IX, where the Peirce calculus of a complete orthogonal frame of idempotents is developed.

A derivation has trace-zero values

theorem TauCeti.AlbertAlgebra.derivation_apply_diagIdempotent_diag_eq_zero {R : Type u_1} [CommRing R] [Invertible 2] (D : ↥(derivationLieAlgebra R (AlbertAlgebra R))) (i : Fin 3) : (↑D (diagIdempotent R i)).diag = 0

The value of a derivation at a diagonal idempotent has no diagonal: every scalar entry of D Eᵢ vanishes, so in particular D Eᵢ has trace 0.

theorem TauCeti.AlbertAlgebra.trace_derivation_apply_diagIdempotent {R : Type u_1} [CommRing R] [Invertible 2] (D : ↥(derivationLieAlgebra R (AlbertAlgebra R))) (i : Fin 3) : trace (↑D (diagIdempotent R i)) = 0

A derivation kills the trace of a diagonal idempotent.

theorem TauCeti.AlbertAlgebra.trace_derivation_apply_offDiagSingle {R : Type u_1} [CommRing R] [Invertible 2] (D : ↥(derivationLieAlgebra R (AlbertAlgebra R))) (j : Fin 3) (a : Octonion R) : trace (↑D (offDiagSingle j a)) = 0

A derivation kills the trace of an off-diagonal slot.

theorem TauCeti.AlbertAlgebra.trace_derivation_apply_eq_zero {R : Type u_1} [CommRing R] [Invertible 2] (D : ↥(derivationLieAlgebra R (AlbertAlgebra R))) (A : AlbertAlgebra R) : trace (↑D A) = 0

A derivation of the split Albert algebra has values of trace 0.

theorem TauCeti.AlbertAlgebra.derivation_apply_mem_traceZero {R : Type u_1} [CommRing R] [Invertible 2] (D : ↥(derivationLieAlgebra R (AlbertAlgebra R))) (A : AlbertAlgebra R) : ↑D A ∈ traceZero R

A derivation maps H₃(𝕆) into its trace-zero subspace, the membership form of TauCeti.AlbertAlgebra.trace_derivation_apply_eq_zero.

The trace-zero subspace as a representation of the derivation algebra

def TauCeti.AlbertAlgebra.traceZeroLieSubmodule (R : Type u_2) [CommRing R] [Invertible 2] : LieSubmodule R (↥(derivationLieAlgebra R (AlbertAlgebra R))) (AlbertAlgebra R)

The trace-zero subspace J₀ as a Lie submodule of H₃(𝕆) over Der H₃(𝕆), so that J₀ is a representation of the derivation algebra. This is the candidate fundamental representation of F₄; over a base satisfying StrongRankCondition its dimension is 26 (TauCeti.AlbertAlgebra.finrank_traceZeroLieSubmodule).

Equations

• TauCeti.AlbertAlgebra.traceZeroLieSubmodule R = { toSubmodule := TauCeti.AlbertAlgebra.traceZero R, lie_mem := ⋯ }

@[simp]

theorem TauCeti.AlbertAlgebra.toSubmodule_traceZeroLieSubmodule (R : Type u_2) [CommRing R] [Invertible 2] : ↑(traceZeroLieSubmodule R) = traceZero R

@[simp]

theorem TauCeti.AlbertAlgebra.mem_traceZeroLieSubmodule {R : Type u_1} [CommRing R] [Invertible 2] {A : AlbertAlgebra R} : A ∈ traceZeroLieSubmodule R ↔ trace A = 0

theorem TauCeti.AlbertAlgebra.finrank_traceZeroLieSubmodule (R : Type u_2) [CommRing R] [Invertible 2] [StrongRankCondition R] : Module.finrank R ↥(traceZeroLieSubmodule R) = 26

The trace-zero subspace is 26-dimensional, over a base satisfying StrongRankCondition.

theorem TauCeti.AlbertAlgebra.isFaithful_traceZeroLieSubmodule {R : Type u_1} [CommRing R] [Invertible 2] (h3 : IsSMulRegular (AlbertAlgebra R) 3) : LieModule.IsFaithful R ↥(derivationLieAlgebra R (AlbertAlgebra R)) ↥(traceZeroLieSubmodule R)

Der H₃(𝕆) acts faithfully on the trace-zero subspace as soon as scalar multiplication by 3 on H₃(𝕆) is regular, so no information is lost by restricting the derivation algebra to its candidate fundamental representation. Some hypothesis on 3 is needed; the instance TauCeti.AlbertAlgebra.instIsFaithfulTraceZeroLieSubmodule supplies this one from typeclasses.

instance TauCeti.AlbertAlgebra.instIsFaithfulTraceZeroLieSubmodule {R : Type u_1} [CommRing R] [Invertible 2] [NoZeroSMulDivisors R (AlbertAlgebra R)] [NeZero 3] : LieModule.IsFaithful R ↥(derivationLieAlgebra R (AlbertAlgebra R)) ↥(traceZeroLieSubmodule R)

Der H₃(𝕆) acts faithfully on the trace-zero subspace over a base for which 3 is a nonzero scalar acting without zero divisors, the typeclass form of TauCeti.AlbertAlgebra.isFaithful_traceZeroLieSubmodule.