Chevalley generators of type G₂ in the derivations of the split octonions

TauCeti/Algebra/Octonion/Derivation.lean identifies the derivation algebra of the split octonions, as a module, with 𝔰𝔩₃ × R³ × R³, through the special linear derivations TauCeti.Octonion.slDerivation and the two vector families TauCeti.Octonion.upperDerivation and TauCeti.Octonion.lowerDerivation. This file exhibits Chevalley generators of type G₂ in it: three families H, E, F indexed by the two simple roots that satisfy Serre's relations for Mathlib's Cartan matrix CartanMatrix.G₂. The universal property of the Serre presentation then gives a homomorphism of Lie algebras

TauCeti.Octonion.g₂ToDerivationLieAlgebra : LieAlgebra.g₂ →ₗ⁅R⁆ Der 𝕆

from the split Lie algebra of type G₂ presented by generators and relations. When 2 and 3 are invertible, the generators E and F generate Der 𝕆, so this homomorphism is surjective.

The trace-zero diagonal matrices act diagonally on all three families: a diagonal matrix diag(d₀, d₁, d₂) acts on the upper vector derivation of the i-th basis vector by dᵢ, on the lower one by -dᵢ, and on the special linear derivation of the matrix unit Eᵢⱼ by dᵢ - dⱼ. The weights ±εᵢ of the vector families are the six short roots of G₂, and the weights εᵢ - εⱼ of 𝔰𝔩₃ are the six long roots. The simple roots are the short root α₁ = ε₁ and the long root α₂ = ε₀ - ε₁ (indexing basis vectors from 0), in Bourbaki's numbering, with ⟨α₂, α₁∨⟩ = -3 and ⟨α₁, α₂∨⟩ = -1, the off-diagonal entries of CartanMatrix.G₂. Accordingly:

• E₁ is the upper vector derivation of e₁, and F₁ is minus the lower one, so that ⁅E₁, F₁⁆ = H₁ is the special linear derivation of diag(-1, 2, -1);
• E₂ and F₂ are the special linear derivations of the matrix units E₀₁ and E₁₀, and H₂ is the special linear derivation of diag(1, -1, 0).

Every relation is checked from the bracket formulas of the three families, over an arbitrary commutative ring. For generation, brackets of these root vectors give the upper and lower vector derivations of e₀, those of e₂ up to the factor 2 coming from the cross product, and then every matrix unit of 𝔰𝔩₃ up to the factor -3 from the bracket of an upper with a lower vector derivation; this is where 2 and 3 must be invertible.

Since Der 𝕆 has rank 14, the surjection shows that LieAlgebra.g₂ has rank at least 14 (TauCeti.Octonion.fourteen_le_rank_g₂). Its injectivity, which would identify Der 𝕆 with LieAlgebra.g₂, is not proved here.

Main definitions

• TauCeti.Octonion.cartanDerivation, TauCeti.Octonion.raisingDerivation and TauCeti.Octonion.loweringDerivation: the Chevalley generators Hᵢ, Eᵢ, Fᵢ in Der 𝕆.
• TauCeti.Octonion.g₂ToDerivationLieAlgebra: the homomorphism LieAlgebra.g₂ →ₗ⁅R⁆ Der 𝕆 they determine.

Main results

• TauCeti.Octonion.isSerreSystem: the generators satisfy Serre's relations for CartanMatrix.G₂.
• TauCeti.Octonion.lieSpan_range_raisingDerivation_union_range_loweringDerivation: if 2 and 3 are invertible, the raising and lowering generators generate Der 𝕆.
• TauCeti.Octonion.g₂ToDerivationLieAlgebra_surjective: hence Der 𝕆 is a quotient of LieAlgebra.g₂.
• TauCeti.Octonion.fourteen_le_rank_g₂: hence LieAlgebra.g₂ has rank at least 14.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 22, where 𝔤₂ is built as 𝔰𝔩₃ ⊕ W ⊕ W* and compared with the derivations of the octonions.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 4--6, Plate IX, for the numbering of the simple roots of G₂.

The generators

def TauCeti.Octonion.cartanDerivation {R : Type u_1} [CommRing R] : Fin 2 → ↥(derivationLieAlgebra R (Octonion R))

The Cartan generators of type G₂ in Der 𝕆: the special linear derivations of diag(-1, 2, -1), the coroot of the short simple root, and of diag(1, -1, 0), the coroot of the long simple root.

Equations

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

def TauCeti.Octonion.raisingDerivation {R : Type u_1} [CommRing R] : Fin 2 → ↥(derivationLieAlgebra R (Octonion R))

The raising generators of type G₂ in Der 𝕆: the upper vector derivation of the basis vector e₁, a root vector for the short simple root, and the special linear derivation of the matrix unit E₀₁, a root vector for the long simple root.

Equations

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

def TauCeti.Octonion.loweringDerivation {R : Type u_1} [CommRing R] : Fin 2 → ↥(derivationLieAlgebra R (Octonion R))

The lowering generators of type G₂ in Der 𝕆: minus the lower vector derivation of the basis vector e₁, and the special linear derivation of the matrix unit E₁₀.

Equations

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

@[simp]

theorem TauCeti.Octonion.cartanDerivation_zero {R : Type u_1} [CommRing R] : cartanDerivation 0 = slDerivation ((LieAlgebra.SpecialLinear.singleSubSingle 1 0) 1 + (LieAlgebra.SpecialLinear.singleSubSingle 1 2) 1)

@[simp]

theorem TauCeti.Octonion.cartanDerivation_one {R : Type u_1} [CommRing R] : cartanDerivation 1 = slDerivation ((LieAlgebra.SpecialLinear.singleSubSingle 0 1) 1)

@[simp]

theorem TauCeti.Octonion.raisingDerivation_zero {R : Type u_1} [CommRing R] : raisingDerivation 0 = upperDerivation (Pi.single 1 1)

@[simp]

theorem TauCeti.Octonion.raisingDerivation_one {R : Type u_1} [CommRing R] : raisingDerivation 1 = slDerivation ((LieAlgebra.SpecialLinear.single 0 1 raisingDerivation_one._proof_1) 1)

@[simp]

theorem TauCeti.Octonion.loweringDerivation_zero {R : Type u_1} [CommRing R] : loweringDerivation 0 = -lowerDerivation (Pi.single 1 1)

@[simp]

theorem TauCeti.Octonion.loweringDerivation_one {R : Type u_1} [CommRing R] : loweringDerivation 1 = slDerivation ((LieAlgebra.SpecialLinear.single 1 0 loweringDerivation_one._proof_1) 1)

Serre's relations

theorem TauCeti.Octonion.isSerreSystem {R : Type u_1} [CommRing R] : IsSerreSystem R CartanMatrix.G₂ cartanDerivation raisingDerivation loweringDerivation

The Chevalley generators of Der 𝕆 satisfy Serre's relations of type G₂, for Mathlib's Cartan matrix CartanMatrix.G₂, over every commutative ring.

The homomorphism from the Serre algebra

noncomputable def TauCeti.Octonion.g₂ToDerivationLieAlgebra {R : Type u_1} [CommRing R] : LieAlgebra.g₂ R →ₗ⁅R⁆ ↥(derivationLieAlgebra R (Octonion R))

The homomorphism from the split Lie algebra of type G₂ to Der 𝕆, determined by the Chevalley generators of TauCeti.Octonion.isSerreSystem through the universal property of the Serre presentation.

Equations

• TauCeti.Octonion.g₂ToDerivationLieAlgebra = TauCeti.serreLift ⋯

@[simp]

theorem TauCeti.Octonion.g₂ToDerivationLieAlgebra_serreH {R : Type u_1} [CommRing R] (i : Fin 2) : g₂ToDerivationLieAlgebra (serreH R CartanMatrix.G₂ i) = cartanDerivation i

@[simp]

theorem TauCeti.Octonion.g₂ToDerivationLieAlgebra_serreE {R : Type u_1} [CommRing R] (i : Fin 2) : g₂ToDerivationLieAlgebra (serreE R CartanMatrix.G₂ i) = raisingDerivation i

@[simp]

theorem TauCeti.Octonion.g₂ToDerivationLieAlgebra_serreF {R : Type u_1} [CommRing R] (i : Fin 2) : g₂ToDerivationLieAlgebra (serreF R CartanMatrix.G₂ i) = loweringDerivation i

Generation

theorem TauCeti.Octonion.eq_top_of_upperDerivation_mem_of_lowerDerivation_mem {R : Type u_1} [CommRing R] [Invertible 3] {S : LieSubalgebra R ↥(derivationLieAlgebra R (Octonion R))} (hu : ∀ (i : Fin 3), upperDerivation (Pi.single i 1) ∈ S) (hl : ∀ (i : Fin 3), lowerDerivation (Pi.single i 1) ∈ S) : S = ⊤

When 3 is invertible, a Lie subalgebra of Der 𝕆 containing the upper and lower vector derivations of the three basis vectors is everything: the bracket of the upper vector derivation of eᵢ with the lower one of eⱼ, for i ≠ j, is -3 times the special linear derivation of the matrix unit Eᵢⱼ, and every derivation is a sum of the three families (TauCeti.Octonion.derivationOfTriple_surjective).

theorem TauCeti.Octonion.lieSpan_range_raisingDerivation_union_range_loweringDerivation {R : Type u_1} [CommRing R] [Invertible 2] [Invertible 3] : LieSubalgebra.lieSpan R (↥(derivationLieAlgebra R (Octonion R))) (Set.range raisingDerivation ∪ Set.range loweringDerivation) = ⊤

The raising and lowering generators generate Der 𝕆 when 2 and 3 are invertible.

Brackets of the generators give the upper and lower vector derivations of e₀, and the bracket of two upper (lower) vector derivations gives twice the lower (upper) vector derivation of e₂. The vector derivations of all three basis vectors generate Der 𝕆 once 3 is invertible.

theorem TauCeti.Octonion.g₂ToDerivationLieAlgebra_surjective {R : Type u_1} [CommRing R] [Invertible 2] [Invertible 3] : Function.Surjective ⇑g₂ToDerivationLieAlgebra

Der 𝕆 is a quotient of the split Lie algebra of type G₂: when 2 and 3 are invertible, TauCeti.Octonion.g₂ToDerivationLieAlgebra is surjective.

theorem TauCeti.Octonion.fourteen_le_rank_g₂ (R : Type u_2) [CommRing R] [StrongRankCondition R] [Invertible 2] [Invertible 3] : 14 ≤ Module.rank R (LieAlgebra.g₂ R)

The split Lie algebra of type G₂ has rank at least 14 over a commutative ring with the strong rank condition in which 2 and 3 are invertible, since it surjects onto the 14-dimensional Der 𝕆.