The integral span of root vectors and coroots

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. This file defines the ℤ-span in L of the root vectors x α and the coroots α∨.

The only bracket coefficients not already known to be integers are those between two root vectors. If these coefficients are integral, IsSl2System.lie_mem_rootCorootSpan proves that the span is closed under the Lie bracket and IsSl2System.rootCorootLieSubalgebra packages it as a Lie subalgebra over ℤ. The other three generator pairs need no hypothesis:

• the bracket of opposite root vectors is a coroot by the normalization of x;
• a coroot acts on a root vector through the integral Cartan number TauCeti.rootCartanWeight;
• two coroots commute because a splitting Cartan subalgebra in a Killing-semisimple Lie algebra is abelian.

For a Chevalley-normalized system the remaining coefficients are ±(p + 1), so the resulting rootCorootLieSubalgebra is the integral Chevalley form of L. This is the Lie-algebra input to the Kostant ℤ-form used in the explicit Chevalley--Demazure construction of Layer 9 of the ReductiveGroups roadmap, which is in turn consumed by CFSGStatement milestone L0.

Main definitions and results

• TauCeti.rootCorootGenerators: the root vectors and coroots as a set in L.
• TauCeti.mem_rootCorootGenerators_iff: characteristic membership in the generator set.
• TauCeti.rootCorootSpan: their span over ℤ.
• TauCeti.corootFamily: the coroots as a family indexed by the weights of L.
• TauCeti.rootCartanWeight: the Cartan integers β α∨ as a ℤ-valued weight of β.
• TauCeti.coe_coroot_eq_zero_of_isZero and TauCeti.rootCartanWeight_eq_zero_of_isZero: both vanish at the zero weight, the one index that indexing by all weights adds to the roots.
• TauCeti.coweightPairing_toLinear_eq_rootCartanWeight: the Cartan integers are the coroot pairings of TauCeti.coweightPairing at a weight of L.
• TauCeti.lie_coroot_coroot_eq_zero and TauCeti.IsSl2System.lie_coroot_rootVector: the two bracket computations against a coroot, in their integral form.
• TauCeti.IsSl2System.lie_mem_rootCorootSpan: closure under the bracket when the root-vector coefficients are integral.
• TauCeti.IsSl2System.rootCorootLieSubalgebra: the resulting integral Lie subalgebra.
• TauCeti.IsSl2System.mem_rootCorootLieSubalgebra_iff: membership in the Lie subalgebra.
• TauCeti.IsSl2System.rootCorootLieSubalgebra_le_iff: the universal property of the Lie subalgebra.

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.

def TauCeti.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) : Set L

The set consisting of a weight-indexed family x and all coroots, regarded as elements of the ambient Lie algebra. When x is a normalized system (such as IsSl2System x), its zero-weight value vanishes alongside the zero coroot.

Equations

• TauCeti.rootCorootGenerators x = Set.range x ∪ Set.range fun (α : LieModule.Weight K (↥H) L) => ↑(LieAlgebra.IsKilling.coroot α)

@[simp]

theorem TauCeti.mem_rootCorootGenerators_iff {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} {v : L} : v ∈ rootCorootGenerators x ↔ (∃ (α : LieModule.Weight K (↥H) L), x α = v) ∨ ∃ (α : LieModule.Weight K (↥H) L), ↑(LieAlgebra.IsKilling.coroot α) = v

Membership in the set of root--coroot generators.

def TauCeti.rootCorootSpan {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) : Submodule ℤ L

The integral span of a weight-indexed family x and all coroots in the ambient Lie algebra.

Equations

• TauCeti.rootCorootSpan x = Submodule.span ℤ (TauCeti.rootCorootGenerators x)

@[simp]

theorem TauCeti.rootVector_mem_rootCorootSpan {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) (α : LieModule.Weight K (↥H) L) : x α ∈ rootCorootSpan x

A root vector belongs to its root--coroot span.

@[simp]

theorem TauCeti.coroot_mem_rootCorootSpan {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) (α : LieModule.Weight K (↥H) L) : ↑(LieAlgebra.IsKilling.coroot α) ∈ rootCorootSpan x

A coroot belongs to every root--coroot span.

@[simp]

theorem TauCeti.rootCorootSpan_le_iff {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} {P : Submodule ℤ L} : rootCorootSpan x ≤ P ↔ (∀ (α : LieModule.Weight K (↥H) L), x α ∈ P) ∧ ∀ (α : LieModule.Weight K (↥H) L), ↑(LieAlgebra.IsKilling.coroot α) ∈ P

The universal property of the integral root--coroot span.

The coroot family and its Cartan integers

noncomputable def TauCeti.corootFamily {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] : LieModule.Weight K (↥H) L → L

The coroots of L, as a family indexed by the weights of L. The index runs over all weights and not only the roots: at the zero weight the value is 0 by TauCeti.coe_coroot_eq_zero_of_isZero, so that index contributes nothing to any span or product taken over this family.

This is the family of distinguished Cartan vectors of TauCeti.chevalleyKostantForm.

Equations

• TauCeti.corootFamily H α = ↑(LieAlgebra.IsKilling.coroot α)

@[simp]

theorem TauCeti.corootFamily_apply {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] (α : LieModule.Weight K (↥H) L) : corootFamily H α = ↑(LieAlgebra.IsKilling.coroot α)

The coroot family evaluates to the coroot of the weight indexing it.

noncomputable def TauCeti.rootCartanWeight {K : Type u} {L : Type v} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] {H : LieSubalgebra K L} [H.IsCartanSubalgebra] (β : LieModule.Weight K (↥H) L) : LieModule.Weight K (↥H) L → ℤ

The Cartan integers β α∨ collected as the integral weight of the root β against the family of all coroots, written through the root-chain coefficients that LieAlgebra.IsKilling.apply_coroot_eq_cast uses to exhibit that pairing as an integer.

Like TauCeti.corootFamily, this is indexed by all weights: at the zero weight the coroot is zero and so is the value, by TauCeti.rootCartanWeight_eq_zero_of_isZero.

Equations

• TauCeti.rootCartanWeight β α = ↑(LieModule.chainBotCoeff (⇑α) β) - ↑(LieModule.chainTopCoeff (⇑α) β)

theorem TauCeti.intCast_rootCartanWeight_apply {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] (α β : LieModule.Weight K (↥H) L) : ↑(rootCartanWeight β α) = β (LieAlgebra.IsKilling.coroot α)

The defining property of TauCeti.rootCartanWeight: it is the Cartan integer β α∨, read in K. Since K has characteristic zero this determines TauCeti.rootCartanWeight uniquely; it is deliberately not a simp lemma, as rewriting with it discards the integrality the definition exists to record.

@[simp]

theorem TauCeti.coe_coroot_eq_zero_of_isZero {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] {α : LieModule.Weight K (↥H) L} (hα : α.IsZero) : ↑(LieAlgebra.IsKilling.coroot α) = 0

A coroot at the zero weight vanishes in the ambient Lie algebra, which is why indexing the coroot family by all weights rather than by the roots costs nothing.

@[simp]

theorem TauCeti.rootCartanWeight_eq_zero_of_isZero {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] (β : LieModule.Weight K (↥H) L) {α : LieModule.Weight K (↥H) L} (hα : α.IsZero) : rootCartanWeight β α = 0

Every root has Cartan integer zero at the zero weight, the coroot there being zero.

@[simp]

theorem TauCeti.coweightPairing_toLinear_eq_rootCartanWeight {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] (β : LieModule.Weight K (↥H) L) (i : ↥LieSubalgebra.root) : coweightPairing (LieModule.Weight.toLinear K (↥H) L β) i = rootCartanWeight β ↑i

At a root the coroot pairing is the Cartan integer, in the Lie-theoretic spelling: for a weight β of L the root-chain description TauCeti.rootCartanWeight computes the same integer that TauCeti.coweightPairing extracts from the value of β on the coroot.

theorem TauCeti.lie_coroot_coroot_eq_zero {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] (α β : LieModule.Weight K (↥H) L) : ⁅↑(LieAlgebra.IsKilling.coroot α), ↑(LieAlgebra.IsKilling.coroot β)⁆ = 0

Two coroots commute, being elements of the abelian Cartan subalgebra.

theorem TauCeti.IsSl2System.lie_rootVector_rootVector_mem_rootCorootSpan {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] [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 γ) (α β : LieModule.Weight K (↥H) L) : ⁅x α, x β⁆ ∈ rootCorootSpan x

If every bracket of root vectors whose weights sum to a root has an integral coefficient, then the bracket of any two root-vector generators belongs to the integral root--coroot span.

The cases in which one weight is zero, the sum is zero, or the sum is not a root are discharged by the normalized-system API; only the genuine root-sum case uses hIntegral.

theorem TauCeti.IsSl2System.lie_coroot_rootVector {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) (α β : LieModule.Weight K (↥H) L) : ⁅↑(LieAlgebra.IsKilling.coroot α), x β⁆ = ↑(rootCartanWeight β α) • x β

A coroot acts on a root vector through a Cartan integer. This is the Cartan relation TauCeti.IsSl2System.lie_coroot with its coefficient in the integral form TauCeti.rootCartanWeight.

theorem TauCeti.IsSl2System.lie_coroot_rootVector_mem_rootCorootSpan {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) (α β : LieModule.Weight K (↥H) L) : ⁅↑(LieAlgebra.IsKilling.coroot α), x β⁆ ∈ rootCorootSpan x

The bracket of a coroot with a root vector belongs to the integral root--coroot span. Its coefficient is the corresponding integral Cartan number.

theorem TauCeti.IsSl2System.lie_rootVector_coroot_mem_rootCorootSpan {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) (α β : LieModule.Weight K (↥H) L) : ⁅x α, ↑(LieAlgebra.IsKilling.coroot β)⁆ ∈ rootCorootSpan x

The bracket of a root vector with a coroot belongs to the integral root--coroot span.

theorem TauCeti.IsSl2System.lie_coroot_coroot_mem_rootCorootSpan {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} (α β : LieModule.Weight K (↥H) L) : ⁅↑(LieAlgebra.IsKilling.coroot α), ↑(LieAlgebra.IsKilling.coroot β)⁆ ∈ rootCorootSpan x

Two coroots have zero bracket, hence their bracket belongs to the integral root--coroot span.

theorem TauCeti.IsSl2System.lie_mem_rootCorootSpan {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 γ) {a b : L} (ha : a ∈ rootCorootSpan x) (hb : b ∈ rootCorootSpan x) : ⁅a, b⁆ ∈ rootCorootSpan x

The integral root--coroot span is closed under the Lie bracket when all root-vector structure constants are integers.

noncomputable def TauCeti.IsSl2System.rootCorootLieSubalgebra {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 γ) : LieSubalgebra ℤ L

The integral Lie subalgebra spanned by a normalized root-vector system and the coroots, under the hypothesis that every root-vector structure constant is integral. For a Chevalley-normalized system this is the Chevalley ℤ-form of the ambient Lie algebra.

Equations

• hx.rootCorootLieSubalgebra hIntegral = { toSubmodule := TauCeti.rootCorootSpan x, lie_mem' := ⋯ }

@[simp]

theorem TauCeti.IsSl2System.rootCorootLieSubalgebra_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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (hIntegral : ∀ (α β γ : LieModule.Weight K (↥H) L), α.IsNonZero → β.IsNonZero → γ.IsNonZero → ⇑γ = ⇑α + ⇑β → ∃ (z : ℤ), ⁅x α, x β⁆ = ↑z • x γ) : (hx.rootCorootLieSubalgebra hIntegral).toSubmodule = rootCorootSpan x

The underlying integer submodule of rootCorootLieSubalgebra is the root--coroot span.

@[simp]

theorem TauCeti.IsSl2System.mem_rootCorootLieSubalgebra_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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (hIntegral : ∀ (α β γ : LieModule.Weight K (↥H) L), α.IsNonZero → β.IsNonZero → γ.IsNonZero → ⇑γ = ⇑α + ⇑β → ∃ (z : ℤ), ⁅x α, x β⁆ = ↑z • x γ) {v : L} : v ∈ hx.rootCorootLieSubalgebra hIntegral ↔ v ∈ rootCorootSpan x

Membership in rootCorootLieSubalgebra coincides with membership in rootCorootSpan.

@[simp]

theorem TauCeti.IsSl2System.rootCorootLieSubalgebra_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] {x : LieModule.Weight K (↥H) L → L} (hx : IsSl2System x) (hIntegral : ∀ (α β γ : LieModule.Weight K (↥H) L), α.IsNonZero → β.IsNonZero → γ.IsNonZero → ⇑γ = ⇑α + ⇑β → ∃ (z : ℤ), ⁅x α, x β⁆ = ↑z • x γ) {M : LieSubalgebra ℤ L} : hx.rootCorootLieSubalgebra hIntegral ≤ M ↔ (∀ (α : LieModule.Weight K (↥H) L), x α ∈ M) ∧ ∀ (α : LieModule.Weight K (↥H) L), ↑(LieAlgebra.IsKilling.coroot α) ∈ M

The universal property of rootCorootLieSubalgebra: it is the least Lie subalgebra containing the root vectors and coroots.

theorem TauCeti.IsSl2System.rootVector_mem_rootCorootLieSubalgebra {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 γ) (α : LieModule.Weight K (↥H) L) : x α ∈ hx.rootCorootLieSubalgebra hIntegral

A root vector belongs to the integral root--coroot Lie subalgebra.

theorem TauCeti.IsSl2System.coroot_mem_rootCorootLieSubalgebra {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 γ) (α : LieModule.Weight K (↥H) L) : ↑(LieAlgebra.IsKilling.coroot α) ∈ hx.rootCorootLieSubalgebra hIntegral

A coroot belongs to the integral root--coroot Lie subalgebra.