Geck's construction of a Lie algebra associated to a root system

This file contains an implementation of Geck's construction of a semisimple Lie algebra from a reduced crystallographic root system. It follows Geck quite closely.

Main definitions:

• RootPairing.GeckConstruction.lieAlgebra: the Geck construction of the Lie algebra associated to a root system with distinguished base.
• RootPairing.GeckConstruction.cartanSubalgebra: a distinguished subalgebra corresponding to a Cartan subalgebra of the Geck construction.
• RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra: the distinguished subalgebra is contained in the Geck construction.
• RootPairing.GeckConstruction.isSl2Triple: a distinguished family of sl₂ triples contained in the Geck construction.

Alternative approaches

The are at least three ways to construct a Lie algebra from a root system:

1. As a quotient of a free Lie algebra, using the Serre relations
2. Directly defining the Lie bracket on $H ⊕ K^∣Φ|$
3. The Geck construction

We comment on these as follows:

1. This construction takes just a matrix as input. It yields a semisimple Lie algebra iff the matrix is a Cartan matrix but it is quite a lot of work to prove this. On the other hand, it also allows construction of Kac-Moody Lie algebras. It has been implemented as Matrix.ToLieAlgebra but as of May 2025, almost nothing has been proved about it in Mathlib.
2. This construction takes a root system with base as input, together with sufficient additional data to determine a collection of extraspecial pairs of roots. The additional data for the extraspecial pairs is required to pin down certain signs when defining the Lie bracket. (These signs can be interpreted as a set-theoretic splitting of Tits's extension of the Weyl group by an elementary 2-group of order $2^l$ where $l$ is the rank.)
3. This construction takes a root system with base as input and is implemented here.

There seems to be no known construction of a Lie algebra from a root system without first choosing a base: https://mathoverflow.net/questions/495434/

TODO

• Lemma stating LinearIndependent R h (easy using RootPairing.Base.cartanMatrix_nondegenerate).
• Lemma stating ⁅e i, f j⁆ = 0 when i ≠ j (Lemma 3.5 from Geck).
• Instance stating LieModule.IsIrreducible R (lieAlgebra b) (b.support ⊕ ι → R) (Lemma 4.2 from Geck). This will immediately yield that the Geck construction is semisimple via LieAlgebra.hasTrivialRadical_of_isIrreducible_of_isFaithful.
• Instance stating ((cartanSubalgebra b).comap (lieAlgebra b).incl).IsCartanSubalgebra (included in Lemma 4.6 from Geck).

def RootPairing.GeckConstruction.e {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} (i : ↑b.support) : Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R

Part of an sl₂ triple used in Geck's construction of a Lie algebra from a root system.

Equations

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

def RootPairing.GeckConstruction.f {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} (i : ↑b.support) : Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R

Part of an sl₂ triple used in Geck's construction of a Lie algebra from a root system.

Equations

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

def RootPairing.GeckConstruction.h {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} (i : ↑b.support) : Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R

Part of an sl₂ triple used in Geck's construction of a Lie algebra from a root system.

Equations

• RootPairing.GeckConstruction.h i = Matrix.fromBlocks 0 0 0 (Matrix.diagonal fun (x : ι) => ↑(P.pairingIn ℤ x ↑i))

def RootPairing.GeckConstruction.ω {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} (b : P.Base) : Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R

An involutive matrix which can transfer results between RootPairing.GeckConstruction.e and RootPairing.GeckConstruction.f.

Equations

• RootPairing.GeckConstruction.ω b = Matrix.fromBlocks 1 0 0 (Matrix.of fun (i j : ι) => if i = -j then 1 else 0)

def RootPairing.GeckConstruction.lieAlgebra {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] (b : P.Base) [Fintype ↑b.support] [Fintype ι] [DecidableEq ι] : LieSubalgebra R (Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R)

Geck's construction of the Lie algebra associated to a root system with distinguished base.

Equations

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

def RootPairing.GeckConstruction.cartanSubalgebra {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] (b : P.Base) [Fintype ↑b.support] [Fintype ι] [DecidableEq ι] : LieSubalgebra R (Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R)

A distinguished subalgebra corresponding to a Cartan subalgebra of the Geck construction.

Equations

• RootPairing.GeckConstruction.cartanSubalgebra b = LieSubalgebra.lieSpan R (Matrix (↑b.support ⊕ ι) (↑b.support ⊕ ι) R) (Set.range RootPairing.GeckConstruction.h)

theorem RootPairing.GeckConstruction.ω_mul_ω {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} {b : P.Base} [DecidableEq ι] [Fintype ι] [Fintype ↑b.support] : ω b * ω b = 1

theorem RootPairing.GeckConstruction.ω_mul_h {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [DecidableEq ι] [Fintype ι] [Fintype ↑b.support] (i : ↑b.support) : ω b * h i = -h i * ω b

theorem RootPairing.GeckConstruction.ω_mul_e {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [DecidableEq ι] [Fintype ι] [Fintype ↑b.support] (i : ↑b.support) : ω b * e i = f i * ω b

theorem RootPairing.GeckConstruction.ω_mul_f {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [DecidableEq ι] [Fintype ι] [Fintype ↑b.support] (i : ↑b.support) : ω b * f i = e i * ω b

theorem RootPairing.GeckConstruction.lie_h_h {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ↑b.support] [Fintype ι] (i j : ↑b.support) : ⁅h i, h j⁆ = 0

theorem RootPairing.GeckConstruction.lie_h_e {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ↑b.support] [Fintype ι] (i j : ↑b.support) : ⁅h j, e i⁆ = b.cartanMatrix i j • e i

Lemma 3.3 (a) from Geck.

theorem RootPairing.GeckConstruction.lie_h_f {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [Fintype ↑b.support] [Fintype ι] (i j : ↑b.support) : ⁅h j, f i⁆ = -b.cartanMatrix i j • f i

Lemma 3.3 (b) from Geck.

theorem RootPairing.GeckConstruction.lie_e_f_same {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [P.IsReduced] [Fintype ↑b.support] [Fintype ι] (i : ↑b.support) : ⁅e i, f i⁆ = h i

Lemma 3.4 from Geck.

theorem RootPairing.GeckConstruction.isSl2Triple {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [P.IsReduced] [Fintype ↑b.support] [Fintype ι] [DecidableEq ι] (i : ↑b.support) : IsSl2Triple (h i) (e i) (f i)

theorem RootPairing.GeckConstruction.cartanSubalgebra_le_lieAlgebra {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [Finite ι] [CommRing R] [IsDomain R] [CharZero R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {P : RootSystem ι R M N} [P.IsCrystallographic] {b : P.Base} [P.IsReduced] [Fintype ↑b.support] [Fintype ι] [DecidableEq ι] : cartanSubalgebra b ≤ lieAlgebra b