Rationalizing the Chevalley Lie lattice

A Chevalley system supplies the integral root--coroot Lie lattice IsChevalleySystem.chevalleyLieLattice. Its underlying integer module is finite and free, and its rational span is the whole ambient Lie algebra. This file packages those facts as a full lattice instance and applies the generic Lie-lattice rationalization theorem to obtain

ℚ ⊗[ℤ] hx.chevalleyLieLattice ≃ₗ⁅ℚ⁆ L.

No basis of the integral lattice is chosen here: the Fin-indexed basis that the matrix-coordinate and Kostant root-subgroup constructions read is the weight basis of the Kostant lane, which is a basis of weight vectors rather than an arbitrary one.

Main declarations

• TauCeti.IsChevalleySystem.instIsLatticeChevalleyLieLattice: the root--coroot Lie lattice is a full integral lattice.
• TauCeti.IsChevalleySystem.chevalleyLieLatticeRationalization: its scalar extension recovers the ambient rational Lie algebra as a Lie algebra.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§25--26.
• R. W. Carter, Simple Groups of Lie Type, §4.1.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

This advances the Chevalley-basis and generic-fibre part of the explicit pinned Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap. That construction is the declared input to milestone L0 of the CFSGStatement roadmap.

instance TauCeti.IsChevalleySystem.instIsLatticeChevalleyLieLattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable ℚ (↥H) L] {ω : L ≃ₗ⁅ℚ⁆ L} {x : LieModule.Weight ℚ (↥H) L → L} (hx : IsChevalleySystem ω x) : Submodule.IsLattice ℚ hx.chevalleyLieLattice.toSubmodule

The Chevalley root--coroot Lie lattice is a full integral lattice in the ambient rational Lie algebra.

noncomputable def TauCeti.IsChevalleySystem.chevalleyLieLatticeRationalization {L : Type u} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable ℚ (↥H) L] {ω : L ≃ₗ⁅ℚ⁆ L} {x : LieModule.Weight ℚ (↥H) L → L} (hx : IsChevalleySystem ω x) : TensorProduct ℤ ℚ ↥hx.chevalleyLieLattice ≃ₗ⁅ℚ⁆ L

The scalar extension of the Chevalley Lie lattice recovers the ambient rational Lie algebra, including its Lie bracket.

Equations

• hx.chevalleyLieLatticeRationalization = hx.chevalleyLieLattice.rationalizationEquiv

@[simp]

theorem TauCeti.IsChevalleySystem.chevalleyLieLatticeRationalization_tmul {L : Type u} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable ℚ (↥H) L] {ω : L ≃ₗ⁅ℚ⁆ L} {x : LieModule.Weight ℚ (↥H) L → L} (hx : IsChevalleySystem ω x) (q : ℚ) (z : ↥hx.chevalleyLieLattice) : hx.chevalleyLieLatticeRationalization (q ⊗ₜ[ℤ] z) = q • ↑z

On pure tensors, the Chevalley-lattice rationalization is the ambient scalar action.

@[simp]

theorem TauCeti.IsChevalleySystem.chevalleyLieLatticeRationalization_symm_coe {L : Type u} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable ℚ (↥H) L] {ω : L ≃ₗ⁅ℚ⁆ L} {x : LieModule.Weight ℚ (↥H) L → L} (hx : IsChevalleySystem ω x) (z : ↥hx.chevalleyLieLattice) : hx.chevalleyLieLatticeRationalization.symm ↑z = 1 ⊗ₜ[ℤ] z

The inverse Chevalley-lattice rationalization sends an integral vector to its unit pure tensor.