The adjoint admissible lattice of a Chevalley system

The Kostant integral form U_ℤ ⊆ U(L) is the subring generated by the divided powers of the distinguished root vectors and the binomial coefficients of the distinguished Cartan vectors. Its downstream use — root subgroups, the elementary Chevalley group, the split torus — is always against a lattice: a ℤ-submodule of a representation which U_ℤ preserves and which is finite and free. Until now every such consumer took that lattice as a hypothesis.

This file supplies one, for the adjoint representation. Let x be a Chevalley system in L, take the root vectors themselves as the distinguished root vectors and the coroots as the distinguished Cartan vectors, and let L_ℤ = chevalleyLieLattice be the ℤ-span of both families. Then L_ℤ is a finite free full ℤ-form of L and is preserved by the whole of U_ℤ.

The two generating families are checked separately.

• The divided powers (ad (x α)) ^ n / n ! preserve L_ℤ by the root-string computation of TauCeti.Algebra.Lie.Weights.Root.KostantStability.
• The binomial coefficients (ad α∨) choose n preserve L_ℤ because ad α∨ acts on each root vector through the Cartan integer β α∨ and annihilates the coroots, so it is diagonal with integer eigenvalues in the generating family.

Because the Kostant form is generated as a ring by these two families, stability then holds for all of U_ℤ through TauCeti.UniversalEnvelopingAlgebra.kostantForm_le_stabilizer, and TauCeti.UniversalEnvelopingAlgebra.kostantFormRep packages the restricted action as a ℤ-algebra map into Module.End ℤ L_ℤ.

This advances Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md, "the Chevalley--Demazure construction ... via a Chevalley basis and the Kostant ℤ-form of the enveloping algebra", by supplying the adjoint admissible lattice that construction starts from; Layer 9 is consumed by milestone L0 of CFSGStatement.

Main definitions and results

• TauCeti.chevalleyKostantForm: the Kostant form of a system of root vectors, taken against TauCeti.corootFamily as its distinguished Cartan vectors.
• TauCeti.IsChevalleySystem.chevalleyKostantForm_le_stabilizer: it stabilizes the Chevalley lattice.
• TauCeti.IsChevalleySystem.chevalleyLatticeRep: the resulting integral representation.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §25.5, §27.
• R. W. Carter, Simple Groups of Lie Type, §4.4.

noncomputable def TauCeti.chevalleyKostantForm {L : Type v} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] (x : LieModule.Weight ℚ (↥H) L → L) : Subring (UniversalEnvelopingAlgebra ℚ L)

The Kostant integral form attached to a system of root vectors: the subring of U(L) generated by the divided powers of the root vectors and the binomial coefficients of the coroots.

Equations

• TauCeti.chevalleyKostantForm x = TauCeti.UniversalEnvelopingAlgebra.kostantForm x (TauCeti.corootFamily H)

theorem TauCeti.chevalleyKostantForm_def {L : Type v} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] (x : LieModule.Weight ℚ (↥H) L → L) : chevalleyKostantForm x = UniversalEnvelopingAlgebra.kostantForm x (corootFamily H)

TauCeti.chevalleyKostantForm is the generic Kostant form of the family of root vectors, together with TauCeti.corootFamily as the distinguished Cartan vectors.

theorem TauCeti.dividedPower_mem_chevalleyKostantForm {L : Type v} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] (x : LieModule.Weight ℚ (↥H) L → L) (α : LieModule.Weight ℚ (↥H) L) (n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (x α)) ∈ chevalleyKostantForm x

Every divided power of a root vector belongs to the Kostant form of a system of root vectors.

theorem TauCeti.ringChoose_coroot_mem_chevalleyKostantForm {L : Type v} [LieRing L] [LieAlgebra ℚ L] [LieAlgebra.IsKilling ℚ L] [FiniteDimensional ℚ L] {H : LieSubalgebra ℚ L} [H.IsCartanSubalgebra] (x : LieModule.Weight ℚ (↥H) L → L) (α : LieModule.Weight ℚ (↥H) L) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) ↑(LieAlgebra.IsKilling.coroot α)) n ∈ chevalleyKostantForm x

Every binomial coefficient of a coroot belongs to the Kostant form of a system of root vectors.

theorem TauCeti.IsChevalleySystem.ringChoose_ad_coroot_mem_chevalleyLieLattice {L : Type v} [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) (α : LieModule.Weight ℚ (↥H) L) (n : ℕ) {y : L} (hy : y ∈ hx.chevalleyLieLattice) : (Ring.choose ((LieAlgebra.ad ℚ L) ↑(LieAlgebra.IsKilling.coroot α)) n) y ∈ hx.chevalleyLieLattice

The binomial coefficients of the coroots preserve the Chevalley lattice. The endomorphism ad α∨ is diagonal in the generating family of the lattice, with the Cartan integers β α∨ as eigenvalues on the root vectors and zero on the coroots.

theorem TauCeti.IsChevalleySystem.dividedPower_representation_mem {L : Type v} [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) (α : LieModule.Weight ℚ (↥H) L) (n : ℕ) {y : L} (hy : y ∈ hx.chevalleyLieLattice) : ((UniversalEnvelopingAlgebra.representation ℚ L L) (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (x α)))) y ∈ hx.chevalleyLieLattice

Every divided power of a root vector acts on the Chevalley lattice through the adjoint representation.

theorem TauCeti.IsChevalleySystem.ringChoose_representation_mem {L : Type v} [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) (α : LieModule.Weight ℚ (↥H) L) (n : ℕ) {y : L} (hy : y ∈ hx.chevalleyLieLattice) : ((UniversalEnvelopingAlgebra.representation ℚ L L) (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) ↑(LieAlgebra.IsKilling.coroot α)) n)) y ∈ hx.chevalleyLieLattice

Every binomial coefficient of a coroot acts on the Chevalley lattice through the adjoint representation.

theorem TauCeti.IsChevalleySystem.chevalleyKostantForm_le_stabilizer {L : Type v} [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) : chevalleyKostantForm x ≤ UniversalEnvelopingAlgebra.stabilizer (UniversalEnvelopingAlgebra.representation ℚ L L) hx.chevalleyLieLattice.toSubmodule

The Chevalley lattice is an admissible lattice for the adjoint representation. The Kostant integral form of a Chevalley system stabilizes the ℤ-span of its root vectors and coroots.

theorem TauCeti.IsChevalleySystem.chevalleyKostantForm_apply_mem {L : Type v} [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) {u : UniversalEnvelopingAlgebra ℚ L} (hu : u ∈ chevalleyKostantForm x) {y : L} (hy : y ∈ hx.chevalleyLieLattice) : ((UniversalEnvelopingAlgebra.representation ℚ L L) u) y ∈ hx.chevalleyLieLattice

The adjoint action of an element of the Kostant form of a Chevalley system preserves the Chevalley lattice.

noncomputable def TauCeti.IsChevalleySystem.chevalleyLatticeRep {L : Type v} [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) : ↥(chevalleyKostantForm x) →ₐ[ℤ] Module.End ℤ ↥hx.chevalleyLieLattice.toSubmodule

The integral adjoint representation of a Chevalley system. The Kostant form acts by ℤ-linear endomorphisms of the Chevalley lattice, which is a finite free full ℤ-form of L.

Equations

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

@[simp]

theorem TauCeti.IsChevalleySystem.coe_chevalleyLatticeRep_apply {L : Type v} [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) (u : ↥(chevalleyKostantForm x)) (y : ↥hx.chevalleyLieLattice.toSubmodule) : ↑((hx.chevalleyLatticeRep u) y) = ((UniversalEnvelopingAlgebra.representation ℚ L L) ↑u) ↑y