The derivation algebra of the split octonions is simple

TauCeti/Algebra/Octonion/Derivation.lean writes the derivation algebra Der 𝕆 of the split octonions as 𝔰𝔩₃ × R³ × R³, through the special linear derivations and the upper and lower vector derivations, and TauCeti/Algebra/Octonion/Serre.lean exhibits Chevalley generators Hᵢ, Eᵢ, Fᵢ of type G₂ in it. This file shows that these generators form a LieAlgebra.Basis of Der 𝕆 with Cartan matrix CartanMatrix.G₂ᵀ, relative to the Cartan subalgebra TauCeti.Octonion.cartanSubalgebra spanned by the two Hᵢ (TauCeti.Octonion.lieBasis), and that over a field of characteristic zero Der 𝕆 is a simple Lie algebra, hence has a nondegenerate Killing form. Through LieAlgebra.Basis.cartanMatrix_base_eq, the root system of Der 𝕆 relative to cartanSubalgebra then has a base with Cartan matrix CartanMatrix.G₂ᵀ: the Lie algebra is Killing-simple of type G₂.

The identification of Der 𝕆 with the split Lie algebra LieAlgebra.g₂ presented by Serre's relations, that is the injectivity of TauCeti.Octonion.g₂ToDerivationLieAlgebra, is not proved here.

Main definitions

• TauCeti.Octonion.cartanSubalgebra: the Lie subalgebra of Der 𝕆 generated by the Cartan generators.
• TauCeti.Octonion.lieBasis: the Chevalley generators as a LieAlgebra.Basis of type G₂, when 2 and 3 are invertible.

Main results

• TauCeti.Octonion.mem_cartanSubalgebra_iff: the Cartan subalgebra consists of the special linear derivations of the diagonal trace-zero matrices.
• TauCeti.Octonion.linearIndependent_cartanDerivation: the two Cartan generators are linearly independent.
• TauCeti.Octonion.instIsCartanSubalgebraCartanSubalgebra and TauCeti.Octonion.instIsTriangularizableCartanSubalgebra: in characteristic zero, cartanSubalgebra is a splitting Cartan subalgebra of Der 𝕆.
• TauCeti.Octonion.isSimple_derivationLieAlgebra: Der 𝕆 is simple in characteristic zero.
• TauCeti.Octonion.instIsKillingDerivationLieAlgebra: hence its Killing form is nondegenerate.

Implementation notes

The proof of simplicity runs through the root-space decomposition, which the basis makes available: cartanSubalgebra is a Cartan subalgebra acting triangularizably. A nonzero ideal I then contains a nonzero generalized weight vector x, of weight χ say, and x is slDerivation M + upperDerivation u + lowerDerivation t for some trace-zero M and vectors u, t. The Cartan subalgebra consists of the special linear derivations of trace-zero diagonal matrices diag d, and the coordinates uᵢ, tᵢ and Mᵢⱼ of a derivation are read off by linear functionals on which diag d acts by dᵢ, -dᵢ and dᵢ - dⱼ. So a nonzero coordinate of x determines χ, and the bracket of x with the root vector of opposite weight — the lower vector derivation of eᵢ, the upper one, or the special linear derivation of Eⱼᵢ — has weight 0, so lies in the Cartan subalgebra. It is nonzero, since a diagonal entry of its 𝔰𝔩₃ parameter is -2 uᵢ, 2 tᵢ or Mᵢⱼ. When x has none of these coordinates it is already in the Cartan subalgebra. Finally a nonzero element diag d of the Cartan subalgebra scales the upper vector derivation of eᵢ by dᵢ, and bracketing that with the lower vector derivations produces all the vector derivations, which generate Der 𝕆.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 22, where 𝔤₂ is built as 𝔰𝔩₃ ⊕ W ⊕ W* and its root-space decomposition is read off that model.
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §19, where the simplicity of the classical algebras and of G₂ is read off a root-space decomposition.
• R. D. Schafer, An Introduction to Nonassociative Algebras, Ch. III, for the derivation algebra of a Cayley algebra as the simple Lie algebra of type G₂.

def TauCeti.Octonion.cartanSubalgebra (R : Type u_1) [CommRing R] : LieSubalgebra R ↥(derivationLieAlgebra R (Octonion R))

The Cartan subalgebra of Der 𝕆: the Lie subalgebra generated by the Cartan generators TauCeti.Octonion.cartanDerivation, the special linear derivations of diag(-1, 2, -1) and diag(1, -1, 0).

Equations

• TauCeti.Octonion.cartanSubalgebra R = LieSubalgebra.lieSpan R (↥(TauCeti.derivationLieAlgebra R (TauCeti.Octonion R))) (Set.range TauCeti.Octonion.cartanDerivation)

theorem TauCeti.Octonion.cartanDerivation_mem_cartanSubalgebra {R : Type u_1} [CommRing R] (k : Fin 2) : cartanDerivation k ∈ cartanSubalgebra R

The Cartan generators lie in the Cartan subalgebra.

instance TauCeti.Octonion.instIsLieAbelianSubtypeEndMemLieSubalgebraDerivationLieAlgebraCartanSubalgebra {R : Type u_1} [CommRing R] : IsLieAbelian ↥(cartanSubalgebra R)

The Cartan subalgebra of Der 𝕆 is abelian, its two generators commuting.

theorem TauCeti.Octonion.mem_cartanSubalgebra_iff {R : Type u_1} [CommRing R] {D : ↥(derivationLieAlgebra R (Octonion R))} : D ∈ cartanSubalgebra R ↔ ∃ (N : ↥(LieAlgebra.SpecialLinear.sl (Fin 3) R)), (↑N).IsDiag ∧ slDerivation N = D

The Cartan subalgebra of Der 𝕆 consists of the special linear derivations of the diagonal trace-zero matrices.

theorem TauCeti.Octonion.linearIndependent_cartanDerivation {R : Type u_1} [CommRing R] : LinearIndependent R cartanDerivation

The two Cartan generators of Der 𝕆 are linearly independent over every commutative ring.

noncomputable def TauCeti.Octonion.lieBasis {R : Type u_1} [CommRing R] [Nontrivial R] [Invertible 2] [Invertible 3] : LieAlgebra.Basis (Fin 2) (cartanSubalgebra R)

The Chevalley generators of Der 𝕆 form a Lie algebra basis of type G₂, relative to TauCeti.Octonion.cartanSubalgebra, with Cartan matrix CartanMatrix.G₂ᵀ = !![2, -1; -3, 2], the short simple root first, over a nontrivial commutative ring in which 2 and 3 are invertible. The invertibility is what makes the raising and lowering generators generate Der 𝕆.

Equations

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

@[simp]

theorem TauCeti.Octonion.lieBasis_A {R : Type u_1} [CommRing R] [Nontrivial R] [Invertible 2] [Invertible 3] : lieBasis.A = CartanMatrix.G₂.transpose

@[simp]

theorem TauCeti.Octonion.lieBasis_h {R : Type u_1} [CommRing R] [Nontrivial R] [Invertible 2] [Invertible 3] : lieBasis.h = cartanDerivation

@[simp]

theorem TauCeti.Octonion.lieBasis_e {R : Type u_1} [CommRing R] [Nontrivial R] [Invertible 2] [Invertible 3] : lieBasis.e = raisingDerivation

@[simp]

theorem TauCeti.Octonion.lieBasis_f {R : Type u_1} [CommRing R] [Nontrivial R] [Invertible 2] [Invertible 3] : lieBasis.f = loweringDerivation

instance TauCeti.Octonion.instIsCartanSubalgebraCartanSubalgebra (K : Type u_1) [Field K] [CharZero K] : (cartanSubalgebra K).IsCartanSubalgebra

Over a field of characteristic zero, TauCeti.Octonion.cartanSubalgebra is a Cartan subalgebra of Der 𝕆, by the Lie algebra basis TauCeti.Octonion.lieBasis.

instance TauCeti.Octonion.instIsTriangularizableCartanSubalgebra (K : Type u_1) [Field K] [CharZero K] : LieModule.IsTriangularizable K ↥(cartanSubalgebra K) ↥(derivationLieAlgebra K (Octonion K))

Over a field of characteristic zero, the action of TauCeti.Octonion.cartanSubalgebra on Der 𝕆 is triangularizable, by the Lie algebra basis TauCeti.Octonion.lieBasis.

theorem TauCeti.Octonion.isSimple_derivationLieAlgebra {K : Type u_1} [Field K] [CharZero K] : LieAlgebra.IsSimple K ↥(derivationLieAlgebra K (Octonion K))

The derivation algebra of the split octonions is simple over a field of characteristic zero: its only ideals are ⊥ and ⊤, and it is not abelian.

instance TauCeti.Octonion.instIsKillingDerivationLieAlgebra {K : Type u_1} [Field K] [CharZero K] : LieAlgebra.IsKilling K ↥(derivationLieAlgebra K (Octonion K))

The Killing form of the derivation algebra of the split octonions is nondegenerate over a field of characteristic zero, since that Lie algebra is simple.