Documentation

TauCeti.Algebra.Lie.Presentation.Serre.Basis

The Serre system carried by a Lie algebra basis #

A LieAlgebra.Basis ι H carries four of the six families of Serre relations as fields: the hᵢ commute, ⁅eᵢ, fᵢ⁆ = hᵢ, ⁅eᵢ, fⱼ⁆ = 0 for i ≠ j, and the two eigenvector equations for ad hᵢ. This file proves the remaining two, the higher relations

(ad eᵢ) ^ (1 - Aⱼᵢ) eⱼ = 0    and    (ad fᵢ) ^ (1 - Aⱼᵢ) fⱼ = 0,

so that the generators of a basis form a TauCeti.IsSerreSystem and the Lie algebra is a quotient of the Serre algebra of the transposed matrix of the basis.

The coefficient ring is a characteristic-zero integral domain, and the Lie algebra is torsion-free and Noetherian as a module over it, which is what makes the sl₂-strings finite. In particular no Killing form, splitting Cartan subalgebra or triangularizability is assumed, and the argument never mentions a root system.

The proof is sl₂ theory rather than root strings. For i ≠ j the vector eⱼ is primitive for the triple (-hᵢ, fᵢ, eᵢ) obtained from LieAlgebra.Basis.sl2 by exchanging the raising and lowering generators, because ⁅fᵢ, eⱼ⁆ = 0, and its eigenvalue for -hᵢ is -Aⱼᵢ. A primitive vector in a Noetherian module has a natural number as eigenvalue, so -Aⱼᵢ is one, and one further step along its string is zero. The f family follows by applying the result for e to the symmetric basis, which exchanges e and f and negates h.

Reading -Aⱼᵢ off LieAlgebra.IsSl2Triple.HasPrimitiveVectorWith.exists_nat rather than assuming it is why no sign condition on the off-diagonal entries of LieAlgebra.Basis.A is needed: that -Aⱼᵢ is a nonnegative integer is a consequence of the relations.

Main results #

References #

Roadmap #

Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md asks for the split reductive group scheme over ℤ to be constructed "via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra". RootPairing.GeckConstruction.basis produces a LieAlgebra.Basis for the explicit matrix Lie algebra of a root system over any field of characteristic zero, whereas that algebra is known to have a nondegenerate Killing form only over an algebraically closed one. So a form of these relations that does not assume LieAlgebra.IsKilling is what a pinned construction over ℚ can use, and TauCeti/LinearAlgebra/RootSystem/SimplyConnectedRootDatum/SerrePresentation.lean is the consumer. TauCeti/Algebra/Lie/Presentation/Serre/Killing.lean keeps the root-string form of the same relations, which applies to a split semisimple Lie algebra presented by a base rather than by a basis.

The higher Serre relations #

source
theorem TauCeti.ad_pow_lie_lieBasis_e_e {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Finite ι] [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] [IsNoetherian K L] {H : LieSubalgebra K L} (b : LieAlgebra.Basis ι H) (i j : ι) :
((LieAlgebra.ad K L) (b.e i) ^ (-b.A.transpose i j).toNat) ⁅b.e i, b.e j⁆ = 0

The higher Serre relation on the raising generators of a Lie algebra basis.

source
theorem TauCeti.ad_pow_lie_lieBasis_f_f {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Finite ι] [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] [IsNoetherian K L] {H : LieSubalgebra K L} (b : LieAlgebra.Basis ι H) (i j : ι) :
((LieAlgebra.ad K L) (b.f i) ^ (-b.A.transpose i j).toNat) ⁅b.f i, b.f j⁆ = 0

The higher Serre relation on the lowering generators of a Lie algebra basis.

The Serre system and the presentation #

source
theorem TauCeti.isSerreSystem_lieBasis {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Finite ι] [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] [IsNoetherian K L] {H : LieSubalgebra K L} (b : LieAlgebra.Basis ι H) :
IsSerreSystem K b.A.transpose b.h b.e b.f

The generators of a Lie algebra basis form a Serre system. The relevant Cartan matrix is the transpose of LieAlgebra.Basis.A, because TauCeti.IsSerreSystem follows Serre's convention ⁅Hᵢ, Eⱼ⁆ = CMᵢⱼ Eⱼ while LieAlgebra.Basis.lie_h_e reads ⁅hⱼ, eᵢ⁆ = Aᵢⱼ eᵢ.

source
theorem TauCeti.serreLift_lieBasis_surjective {ι : Type u_1} {K : Type u_2} {L : Type u_3} [Finite ι] [CommRing K] [IsDomain K] [CharZero K] [LieRing L] [LieAlgebra K L] [Module.IsTorsionFree K L] [IsNoetherian K L] {H : LieSubalgebra K L} (b : LieAlgebra.Basis ι H) :
Function.Surjective ⇑(serreLift ⋯)

The homomorphism induced by the generators of a Lie algebra basis is surjective.