The integral root--coroot lattice

Let L be a finite-dimensional Lie algebra with nondegenerate Killing form, let H be a splitting Cartan subalgebra, and let x be a normalized system of root vectors. The integral root--coroot span from TauCeti.Algebra.Lie.Weights.Root.CorootSpan is generated by the vectors x α and the coroots α∨.

This file proves the module-theoretic properties that make that span a lattice. Its generating set is finite, hence the span is finite over ℤ; as a submodule of a vector space over a characteristic-zero field, it is torsion-free and therefore free. It is also full: its scalar span over the ground field is all of L. Fullness follows because the root vectors span L together with H, while the coroots span H.

For a Chevalley system, the integral structure-constant theorem canonically makes this lattice a Lie subalgebra. IsChevalleySystem.chevalleyLieLattice packages that specialization, so downstream Kostant constructions do not have to pass the integral-coefficient theorem as a separate argument. It is a finite free full ℤ-form of the characteristic-zero Lie algebra.

These are the lattice properties required by the Chevalley-basis input to the explicit Chevalley--Demazure construction in Layer 9 of the ReductiveGroups roadmap. That construction is consumed by milestone L0 of the CFSGStatement roadmap.

Main declarations

• TauCeti.finite_rootCorootGenerators: the root--coroot generating set is finite.
• TauCeti.IsSl2System.span_rootCorootSpan_eq_top: the integral span is full over the ground field.
• TauCeti.IsChevalleySystem.chevalleyLieLattice: the canonical integral Lie lattice attached to a Chevalley system.
• TauCeti.IsChevalleySystem.span_chevalleyLieLattice_eq_top: the Chevalley Lie lattice is full.

References

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

theorem TauCeti.finite_rootCorootGenerators {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (x : LieModule.Weight K (↥H) L → L) : (rootCorootGenerators x).Finite

The root vectors and coroots form a finite set.

theorem TauCeti.rootCorootSpan_eq_span_generators {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (x : LieModule.Weight K (↥H) L → L) : rootCorootSpan x = Submodule.span ℤ (rootCorootGenerators x)

The root--coroot span is the ℤ-span of its named generating set.

instance TauCeti.instModuleFiniteRootCorootSpan {K : Type u} {L : Type v} [Field K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (x : LieModule.Weight K (↥H) L → L) : Module.Finite ℤ ↥(rootCorootSpan x)

The integral root--coroot span is finitely generated as a ℤ-module.

theorem TauCeti.IsSl2System.span_rootCorootSpan_eq_top {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) : Submodule.span K ↑(rootCorootSpan x) = ⊤

The scalar span of the integral root--coroot span is the whole Lie algebra.

theorem TauCeti.IsSl2System.span_rootCorootLieSubalgebra_eq_top {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (hIntegral : ∀ (α β γ : LieModule.Weight K (↥H) L), α.IsNonZero → β.IsNonZero → γ.IsNonZero → ⇑γ = ⇑α + ⇑β → ∃ (z : ℤ), ⁅x α, x β⁆ = ↑z • x γ) : Submodule.span K ↑(hx.rootCorootLieSubalgebra hIntegral) = ⊤

Every integral root--coroot Lie subalgebra has full scalar span. The integral-coefficient hypothesis affects its Lie bracket structure, not its underlying lattice.

instance TauCeti.instModuleFreeRootCorootSpan {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (x : LieModule.Weight K (↥H) L → L) : Module.Free ℤ ↥(rootCorootSpan x)

The finite root--coroot span is a free ℤ-module.

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

The integral root--coroot Lie lattice canonically attached to a Chevalley system.

Equations

• hx.chevalleyLieLattice = ⋯.rootCorootLieSubalgebra ⋯

@[simp]

theorem TauCeti.IsChevalleySystem.chevalleyLieLattice_toSubmodule {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) : hx.chevalleyLieLattice.toSubmodule = rootCorootSpan x

The underlying integer submodule of the Chevalley Lie lattice is the root--coroot span.

@[simp]

theorem TauCeti.IsChevalleySystem.mem_chevalleyLieLattice_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) {y : L} : y ∈ hx.chevalleyLieLattice ↔ y ∈ rootCorootSpan x

Membership in the Chevalley Lie lattice is membership in the root--coroot span.

@[simp]

theorem TauCeti.IsChevalleySystem.chevalleyLieLattice_le_iff {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) {M : LieSubalgebra ℤ L} : hx.chevalleyLieLattice ≤ M ↔ (∀ (α : LieModule.Weight K (↥H) L), x α ∈ M) ∧ ∀ (α : LieModule.Weight K (↥H) L), ↑(LieAlgebra.IsKilling.coroot α) ∈ M

The Chevalley Lie lattice is the least integral Lie subalgebra containing all root vectors and coroots.

theorem TauCeti.IsChevalleySystem.rootVector_mem_chevalleyLieLattice {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α : LieModule.Weight K (↥H) L) : x α ∈ hx.chevalleyLieLattice

Every root vector belongs to the Chevalley Lie lattice.

theorem TauCeti.IsChevalleySystem.coroot_mem_chevalleyLieLattice {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) (α : LieModule.Weight K (↥H) L) : ↑(LieAlgebra.IsKilling.coroot α) ∈ hx.chevalleyLieLattice

Every coroot belongs to the Chevalley Lie lattice.

instance TauCeti.IsChevalleySystem.instModuleFiniteChevalleyLieLattice {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) : Module.Finite ℤ ↥hx.chevalleyLieLattice

A Chevalley Lie lattice is finitely generated as a ℤ-module.

theorem TauCeti.IsChevalleySystem.span_chevalleyLieLattice_eq_top {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) : Submodule.span K ↑hx.chevalleyLieLattice = ⊤

The scalar span of a Chevalley Lie lattice is the whole Lie algebra.

instance TauCeti.IsChevalleySystem.instModuleFreeChevalleyLieLattice {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [LieAlgebra.IsKilling K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {ω : L ≃ₗ⁅K⁆ L} {x : LieModule.Weight K (↥H) L → L} (hx : IsChevalleySystem ω x) : Module.Free ℤ ↥hx.chevalleyLieLattice

A Chevalley Lie lattice is a finite free ℤ-module.