The ordered span of the rank-one Kostant form

Let H, E, and F satisfy the sl₂ commutator relations in an associative algebra over ℚ. The rank-one Kostant form is generated over ℤ by the divided powers of E and F and the generalized binomial coefficients in H. This file proves the spanning half of its integral PBW normal form: the subring generated by those elements is, as an additive group, spanned by

F⁽ᵃ⁾ (H choose b) E⁽ᶜ⁾.

The substantive step is closure of the ordered span under multiplication. In a product of two ordered monomials, TauCeti.Sl2.dividedPower_e_mul_dividedPower_f straightens the middle E⁽ᶜ⁾ F⁽ᵈ⁾; the divided-power commutation formulas move the remaining Cartan coefficients back to the middle; and integer translation preserves TauCeti.ringChooseSpan H. Thus every summand is again an integral combination of ordered monomials.

This is the rank-one spanning step toward the integral PBW theorem for the Kostant form used in the explicit Chevalley--Demazure construction of Layer 9 of the ReductiveGroups roadmap. Linear independence of these monomials is not asserted here.

In the universal enveloping algebra UniversalEnvelopingAlgebra ℚ L of a Lie algebra L with an sl₂ triple (h, e, f), the abstract rank-one generator set TauCeti.Sl2.kostantGenerators identifies with TauCeti.UniversalEnvelopingAlgebra.kostantGenerators ![e, f] ![h], and the subring closure identifies with TauCeti.UniversalEnvelopingAlgebra.kostantForm ![e, f] ![h].

Main definitions and results

• TauCeti.Sl2.orderedKostantMonomial is F⁽ᵃ⁾ (H choose b) E⁽ᶜ⁾.
• TauCeti.Sl2.orderedKostantSpan is their additive ℤ-span.
• TauCeti.Sl2.mul_mem_orderedKostantSpan proves that span is closed under multiplication.
• TauCeti.Sl2.kostantGenerators is the set of rank-one divided-power and Cartan-binomial generators in an abstract associative ℚ-algebra.
• TauCeti.Sl2.toAddSubgroup_subringClosure_kostantGenerators identifies the additive group of the generated subring with the ordered span.
• TauCeti.Sl2.kostantGenerators_eq_universalEnveloping bridges the abstract rank-one generators to TauCeti.UniversalEnvelopingAlgebra.kostantGenerators.
• TauCeti.Sl2.toAddSubgroup_kostantForm identifies the additive group of the enveloping-algebra Kostant form kostantForm ![e, f] ![h] with the ordered span.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §26.2.
• J. C. Jantzen, Representations of Algebraic Groups, 2nd ed., II.1.

noncomputable def TauCeti.Sl2.orderedKostantMonomial {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) (a b c : ℕ) : A

An ordered rank-one Kostant monomial F⁽ᵃ⁾ (H choose b) E⁽ᶜ⁾.

Equations

• TauCeti.Sl2.orderedKostantMonomial H E F a b c = TauCeti.Associative.dividedPower a F * Ring.choose H b * TauCeti.Associative.dividedPower c E

theorem TauCeti.Sl2.orderedKostantMonomial_zero_zero_zero {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) : orderedKostantMonomial H E F 0 0 0 = 1

@[simp]

theorem TauCeti.Sl2.orderedKostantMonomial_left {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) (n : ℕ) : orderedKostantMonomial H E F n 0 0 = Associative.dividedPower n F

@[simp]

theorem TauCeti.Sl2.orderedKostantMonomial_middle {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) (n : ℕ) : orderedKostantMonomial H E F 0 n 0 = Ring.choose H n

@[simp]

theorem TauCeti.Sl2.orderedKostantMonomial_right {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) (n : ℕ) : orderedKostantMonomial H E F 0 0 n = Associative.dividedPower n E

noncomputable def TauCeti.Sl2.orderedKostantMonomials {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) : Set A

The set of ordered rank-one Kostant monomials.

Equations

• TauCeti.Sl2.orderedKostantMonomials H E F = {x : A | ∃ (a : ℕ) (b : ℕ) (c : ℕ), TauCeti.Sl2.orderedKostantMonomial H E F a b c = x}

@[simp]

theorem TauCeti.Sl2.mem_orderedKostantMonomials_iff {A : Type u} [Ring A] [Algebra ℚ A] {H E F x : A} : x ∈ orderedKostantMonomials H E F ↔ ∃ (a : ℕ) (b : ℕ) (c : ℕ), orderedKostantMonomial H E F a b c = x

Membership in the set of ordered rank-one Kostant monomials.

noncomputable def TauCeti.Sl2.orderedKostantSpan {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) : AddSubgroup A

The additive ℤ-span of the ordered rank-one Kostant monomials.

Equations

• TauCeti.Sl2.orderedKostantSpan H E F = AddSubgroup.closure (TauCeti.Sl2.orderedKostantMonomials H E F)

@[simp]

theorem TauCeti.Sl2.orderedKostantMonomial_mem_orderedKostantSpan {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) (a b c : ℕ) : orderedKostantMonomial H E F a b c ∈ orderedKostantSpan H E F

Every ordered Kostant monomial belongs to its additive span.

@[simp]

theorem TauCeti.Sl2.orderedKostantSpan_le_iff {A : Type u} [Ring A] [Algebra ℚ A] {S : AddSubgroup A} {H E F : A} : orderedKostantSpan H E F ≤ S ↔ ∀ (a b c : ℕ), orderedKostantMonomial H E F a b c ∈ S

The ordered Kostant span lies in an additive subgroup exactly when that subgroup contains every ordered Kostant monomial.

@[simp]

theorem TauCeti.Sl2.one_mem_orderedKostantSpan {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) : 1 ∈ orderedKostantSpan H E F

The ordered Kostant span contains one.

theorem TauCeti.Sl2.dividedPower_mul_mul_dividedPower_mem_orderedKostantSpan {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) (a c : ℕ) {r : A} (hr : r ∈ ringChooseSpan H) : Associative.dividedPower a F * r * Associative.dividedPower c E ∈ orderedKostantSpan H E F

An ordered product with any integral combination of Cartan binomial coefficients in the middle belongs to the ordered Kostant span.

theorem TauCeti.Sl2.mul_mem_orderedKostantSpan {A : Type u} [Ring A] [Algebra ℚ A] {H E F x y : A} (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) (hhf : H * F - F * H = -(2 • F)) (hx : x ∈ orderedKostantSpan H E F) (hy : y ∈ orderedKostantSpan H E F) : x * y ∈ orderedKostantSpan H E F

The ordered rank-one Kostant span is closed under multiplication when H, E, and F satisfy the sl₂ commutator relations.

noncomputable def TauCeti.Sl2.kostantGenerators {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) : Set A

The three families of generators of the rank-one Kostant form in an abstract ℚ-algebra: lowering and raising divided powers and generalized binomial coefficients in the Cartan element.

This is the rank-one generator set attached to a single sl₂ triple (H, E, F) in an arbitrary ℚ-algebra, distinct from the indexed family TauCeti.UniversalEnvelopingAlgebra.kostantGenerators. In the universal enveloping algebra U(L), it identifies with TauCeti.UniversalEnvelopingAlgebra.kostantGenerators ![e, f] ![h].

Equations

• TauCeti.Sl2.kostantGenerators H E F = (Set.range fun (n : ℕ) => TauCeti.Associative.dividedPower n F) ∪ Set.range (Ring.choose H) ∪ Set.range fun (n : ℕ) => TauCeti.Associative.dividedPower n E

@[simp]

theorem TauCeti.Sl2.mem_kostantGenerators_iff {A : Type u} [Ring A] [Algebra ℚ A] {H E F x : A} : x ∈ kostantGenerators H E F ↔ (∃ (n : ℕ), Associative.dividedPower n F = x) ∨ (∃ (n : ℕ), Ring.choose H n = x) ∨ ∃ (n : ℕ), Associative.dividedPower n E = x

Membership in the rank-one Kostant generator set.

theorem TauCeti.Sl2.subringClosure_kostantGenerators_eq_subringClosure_orderedKostantMonomials {A : Type u} [Ring A] [Algebra ℚ A] (H E F : A) : Subring.closure (kostantGenerators H E F) = Subring.closure (orderedKostantMonomials H E F)

The subring generated by the rank-one Kostant generators coincides with the subring generated by the ordered Kostant monomials.

@[simp]

theorem TauCeti.Sl2.toAddSubgroup_subringClosure_kostantGenerators {A : Type u} [Ring A] [Algebra ℚ A] {H E F : A} (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) (hhf : H * F - F * H = -(2 • F)) : (Subring.closure (kostantGenerators H E F)).toAddSubgroup = orderedKostantSpan H E F

The additive group of the subring generated by the rank-one Kostant generators is exactly the span of ordered F--H--E monomials.

@[simp]

theorem TauCeti.Sl2.mem_subringClosure_kostantGenerators_iff {A : Type u} [Ring A] [Algebra ℚ A] {H E F x : A} (hef : E * F - F * E = H) (hhe : H * E - E * H = 2 • E) (hhf : H * F - F * H = -(2 • F)) : x ∈ Subring.closure (kostantGenerators H E F) ↔ x ∈ orderedKostantSpan H E F

Membership in the subring generated by the rank-one Kostant generators is membership in the ordered Kostant span.

theorem TauCeti.Sl2.kostantGenerators_eq_universalEnveloping {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {h e f : L} : kostantGenerators ((UniversalEnvelopingAlgebra.ι ℚ) h) ((UniversalEnvelopingAlgebra.ι ℚ) e) ((UniversalEnvelopingAlgebra.ι ℚ) f) = UniversalEnvelopingAlgebra.kostantGenerators ![e, f] ![h]

The abstract rank-one Kostant generators coincide with the enveloping-algebra Kostant generators attached to the two-element root family ![e, f] and the one-element Cartan family ![h].

theorem TauCeti.Sl2.kostantForm_eq_subringClosure_kostantGenerators {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {h e f : L} : UniversalEnvelopingAlgebra.kostantForm ![e, f] ![h] = Subring.closure (kostantGenerators ((UniversalEnvelopingAlgebra.ι ℚ) h) ((UniversalEnvelopingAlgebra.ι ℚ) e) ((UniversalEnvelopingAlgebra.ι ℚ) f))

The enveloping-algebra Kostant form kostantForm ![e, f] ![h] is the subring closure of the rank-one Kostant generators.

@[simp]

theorem TauCeti.Sl2.toAddSubgroup_kostantForm {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {h e f : L} (hef : ⁅e, f⁆ = h) (hhe : ⁅h, e⁆ = 2 • e) (hhf : ⁅h, f⁆ = -(2 • f)) : (UniversalEnvelopingAlgebra.kostantForm ![e, f] ![h]).toAddSubgroup = orderedKostantSpan ((UniversalEnvelopingAlgebra.ι ℚ) h) ((UniversalEnvelopingAlgebra.ι ℚ) e) ((UniversalEnvelopingAlgebra.ι ℚ) f)

The additive group of the Kostant integral form kostantForm ![e, f] ![h] in the universal enveloping algebra is spanned by ordered F--H--E monomials.

@[simp]

theorem TauCeti.Sl2.mem_kostantForm_iff {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {h e f : L} (hef : ⁅e, f⁆ = h) (hhe : ⁅h, e⁆ = 2 • e) (hhf : ⁅h, f⁆ = -(2 • f)) {x : UniversalEnvelopingAlgebra ℚ L} : x ∈ UniversalEnvelopingAlgebra.kostantForm ![e, f] ![h] ↔ x ∈ orderedKostantSpan ((UniversalEnvelopingAlgebra.ι ℚ) h) ((UniversalEnvelopingAlgebra.ι ℚ) e) ((UniversalEnvelopingAlgebra.ι ℚ) f)

Membership in the Kostant integral form kostantForm ![e, f] ![h] is membership in the ordered Kostant span.