The Kostant integral form generated by root and Cartan vectors

Let L be a Lie algebra over ℚ. Given families e : ι → L of root vectors and h : κ → L of Cartan vectors, the associated Kostant integral form is the subring of UniversalEnvelopingAlgebra ℚ L generated by

eᵢ⁽ⁿ⁾ = eᵢⁿ / n!       and       (hⱼ choose n)

for all indices and all natural numbers n. When e ranges over the Chevalley root vectors x_α for every root α (positive and negative), and h ranges over the Cartan generators, this is the usual Kostant ℤ-form. The definition in this file deliberately takes the two distinguished families as data: the later Chevalley construction will supply them from a pinned root datum, while the integral-form construction and its functoriality do not use the Chevalley relations.

The divided powers are TauCeti.Associative.dividedPower. The Cartan generators are Mathlib's Ring.choose, which evaluates the descending Pochhammer polynomial and divides by n!; no second binomial-coefficient API is introduced here. The form is a Subring, rather than a ℚ-subalgebra, because multiplication by arbitrary rational scalars would destroy the integral lattice. A local ℚ≥0-module structure supplies the BinomialRing instance used to elaborate Ring.choose.

The Cartan--Cartan normal-ordering rule is TauCeti.ringChoose_mul_ringChoose: it expands a product of two binomial coefficients in one Cartan vector as an integral linear combination of binomial coefficients in that vector. Separately, because each coefficient in a designated Cartan vector is a generator of the Kostant form, the subring they generate lies in that form.

The main results are a spanning theorem and exact functoriality. When e and h generate L as a Lie algebra, the form spans the enveloping algebra over ℚ. A Lie homomorphism sends the form generated by (e, h) onto the form generated by their images, so a Lie equivalence restricts to a ring equivalence of the corresponding integral forms. These are respectively the fullness and transport results needed by the Chevalley construction.

Main definitions and results

• TauCeti.UniversalEnvelopingAlgebra.kostantForm: the generated integral form.
• TauCeti.UniversalEnvelopingAlgebra.kostantForm_le_iff: its universal property.
• TauCeti.UniversalEnvelopingAlgebra.subringClosure_range_ringChoose_le_kostantForm: the subring generated by the binomial coefficients in one Cartan vector lies in the Kostant form.
• TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_add_intCast_mem_kostantForm: integer translates of designated Cartan binomial coefficients belong to the Kostant form.
• TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_sub_intCast_mem_kostantForm: subtracting an integer from a designated Cartan argument also preserves membership in the Kostant form.
• TauCeti.UniversalEnvelopingAlgebra.span_kostantForm_eq_top: under a Lie-generation hypothesis, the form spans the enveloping algebra over ℚ.
• TauCeti.UniversalEnvelopingAlgebra.dividedPower_mem_map_kostantForm: divided powers of mapped root vectors lie in the mapped Kostant form.
• TauCeti.UniversalEnvelopingAlgebra.map_kostantForm: exact functoriality under Lie maps.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormMap: the restricted map of integral forms.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormEquiv: transport under a Lie equivalence.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormAut: transport under an invariant Lie automorphism.
• TauCeti.UniversalEnvelopingAlgebra.stabilizer: the subring stabilizing a given ℤ-submodule.
• TauCeti.UniversalEnvelopingAlgebra.kostantForm_le_stabilizer: generator criterion for the Kostant form to stabilize a ℤ-submodule.
• TauCeti.UniversalEnvelopingAlgebra.kostantFormRep: the restricted representation of the Kostant integral form on an invariant ℤ-submodule.
• TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormRep_apply: compatibility with the ambient algebra representation.

References

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

Generators and the integral form

def TauCeti.UniversalEnvelopingAlgebra.kostantRootGenerators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} (e : ι → L) : Set (UniversalEnvelopingAlgebra ℚ L)

The divided powers of a specified family of root vectors in the universal enveloping algebra.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootGenerators e = Set.range fun (p : ι × ℕ) => TauCeti.Associative.dividedPower p.2 ((UniversalEnvelopingAlgebra.ι ℚ) (e p.1))

def TauCeti.UniversalEnvelopingAlgebra.kostantCartanGenerators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} (h : κ → L) : Set (UniversalEnvelopingAlgebra ℚ L)

The binomial coefficients of a specified family of Cartan vectors in the universal enveloping algebra. Mathlib's Ring.choose x n is x * (x - 1) * ... * (x - n + 1) / n!.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantCartanGenerators h = Set.range fun (p : κ × ℕ) => Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h p.1)) p.2

def TauCeti.UniversalEnvelopingAlgebra.kostantGenerators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) : Set (UniversalEnvelopingAlgebra ℚ L)

The generators of the Kostant integral form attached to root vectors e and Cartan vectors h: all divided powers of the former and all binomial coefficients of the latter.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantGenerators e h = TauCeti.UniversalEnvelopingAlgebra.kostantRootGenerators e ∪ TauCeti.UniversalEnvelopingAlgebra.kostantCartanGenerators h

def TauCeti.UniversalEnvelopingAlgebra.kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) : Subring (UniversalEnvelopingAlgebra ℚ L)

The Kostant integral form generated by specified root and Cartan vectors.

When e ranges over the Chevalley root vectors for every root, both positive and negative, and h ranges over the Cartan generators, this is the usual ℤ-form inside the universal enveloping algebra. It is represented as the smallest subring containing the divided powers of the supplied root vectors and the binomial coefficients of the supplied Cartan vectors.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantForm e h = Subring.closure (TauCeti.UniversalEnvelopingAlgebra.kostantGenerators e h)

theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_mem_kostantRootGenerators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} (e : ι → L) (i : ι) (n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) ∈ kostantRootGenerators e

A divided power of a designated root vector is one of the root-generator elements.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantRootGenerators_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {e : ι → L} {x : UniversalEnvelopingAlgebra ℚ L} : x ∈ kostantRootGenerators e ↔ ∃ (i : ι) (n : ℕ), Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) = x

Membership in the root generators: the elements are exactly the divided powers of the designated root vectors.

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_mem_kostantCartanGenerators {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} (h : κ → L) (i : κ) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n ∈ kostantCartanGenerators h

A binomial coefficient of a designated Cartan vector is one of the Cartan-generator elements.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantCartanGenerators_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type u_1} {h : κ → L} {x : UniversalEnvelopingAlgebra ℚ L} : x ∈ kostantCartanGenerators h ↔ ∃ (i : κ) (n : ℕ), Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n = x

Membership in the Cartan generators: the elements are exactly the binomial coefficients of the designated Cartan vectors.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_kostantGenerators_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {e : ι → L} {h : κ → L} {x : UniversalEnvelopingAlgebra ℚ L} : x ∈ kostantGenerators e h ↔ (∃ (i : ι) (n : ℕ), Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) = x) ∨ ∃ (i : κ) (n : ℕ), Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n = x

Membership in the full generator set: an element is a generator exactly when it is a divided power of a designated root vector or a binomial coefficient of a designated Cartan vector.

theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : ι) (n : ℕ) : Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) ∈ kostantForm e h

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

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : κ) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n ∈ kostantForm e h

Every binomial coefficient of a designated Cartan vector belongs to the Kostant form.

theorem TauCeti.UniversalEnvelopingAlgebra.subringClosure_range_ringChoose_le_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : κ) : Subring.closure (Set.range (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)))) ≤ kostantForm e h

The subring generated by the binomial coefficients in one designated Cartan vector is contained in the Kostant form.

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_add_intCast_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : κ) (z : ℤ) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i) + ↑z) n ∈ kostantForm e h

Every integer translate of a designated Cartan binomial coefficient belongs to the Kostant integral form. This is the integrality statement for the shifted coefficients produced by Cartan/root normal ordering.

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_ι_sub_intCast_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : κ) (z : ℤ) (n : ℕ) : Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i) - ↑z) n ∈ kostantForm e h

Subtracting an integer from the argument of a designated Cartan binomial coefficient keeps it in the Kostant integral form.

theorem TauCeti.UniversalEnvelopingAlgebra.rootVector_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : ι) : (UniversalEnvelopingAlgebra.ι ℚ) (e i) ∈ kostantForm e h

Each designated root vector itself belongs to the Kostant form.

theorem TauCeti.UniversalEnvelopingAlgebra.cartanVector_mem_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (i : κ) : (UniversalEnvelopingAlgebra.ι ℚ) (h i) ∈ kostantForm e h

Each designated Cartan vector itself belongs to the Kostant form.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_le_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (S : Subring (UniversalEnvelopingAlgebra ℚ L)) : kostantForm e h ≤ S ↔ (∀ (i : ι) (n : ℕ), Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)) ∈ S) ∧ ∀ (i : κ) (n : ℕ), Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n ∈ S

The universal property of the Kostant form: it lies in a subring exactly when that subring contains every root divided power and every Cartan binomial coefficient.

Spanning the enveloping algebra

theorem TauCeti.UniversalEnvelopingAlgebra.span_kostantForm_eq_top {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (e : ι → L) (h : κ → L) (hgen : LieSubalgebra.lieSpan ℚ L (Set.range e ∪ Set.range h) = ⊤) : Submodule.span ℚ ↑(kostantForm e h) = ⊤

The Kostant integral form spans the enveloping algebra. If the supplied root and Cartan vectors generate L as a Lie algebra, every element of U(L) is a ℚ-linear combination of elements of kostantForm e h; equivalently, ℚ ⊗ℤ U_ℤ → U(L) is onto.

This is the half of "U_ℤ is a ℤ-form of U(L)" that does not need the integral Poincaré--Birkhoff--Witt theorem. The hypothesis is exactly what a Chevalley basis supplies, since the root vectors and the Cartan generators generate a semisimple Lie algebra.

Functoriality

theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_mem_map_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {A : Type u_2} [Ring A] [Algebra ℚ A] (e : ι → L) (h : κ → L) (f : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] A) (i : ι) (n : ℕ) : Associative.dividedPower n (f ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ∈ Subring.map (↑f) (kostantForm e h)

Every divided power of the image of a designated root vector lies in the image of the Kostant integral form: the root-vector generator eᵢ⁽ⁿ⁾ is carried there by any algebra map.

theorem TauCeti.UniversalEnvelopingAlgebra.image_kostantRootGenerators {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} (f : L →ₗ⁅ℚ⁆ M) (e : ι → L) : ⇑(map ℚ f) '' kostantRootGenerators e = kostantRootGenerators fun (i : ι) => f (e i)

A Lie homomorphism maps the root generators to the root generators of the image family.

theorem TauCeti.UniversalEnvelopingAlgebra.image_kostantCartanGenerators {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {κ : Type u_1} (f : L →ₗ⁅ℚ⁆ M) (h : κ → L) : ⇑(map ℚ f) '' kostantCartanGenerators h = kostantCartanGenerators fun (i : κ) => f (h i)

A Lie homomorphism maps the Cartan generators to the Cartan generators of the image family.

theorem TauCeti.UniversalEnvelopingAlgebra.image_kostantGenerators {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (f : L →ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) : ⇑(map ℚ f) '' kostantGenerators e h = kostantGenerators (fun (i : ι) => f (e i)) fun (i : κ) => f (h i)

A Lie homomorphism maps the full Kostant generator set onto the generator set of the image families.

theorem TauCeti.UniversalEnvelopingAlgebra.map_kostantForm {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (f : L →ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) : Subring.map (map ℚ f).toRingHom (kostantForm e h) = kostantForm (fun (i : ι) => f (e i)) fun (i : κ) => f (h i)

Exact functoriality of the Kostant form. The enveloping-algebra map induced by a Lie homomorphism sends the integral form generated by (e, h) onto the integral form generated by their pointwise images.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormMap {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (f : L →ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) : ↥(kostantForm e h) →+* ↥(kostantForm (fun (i : ι) => f (e i)) fun (i : κ) => f (h i))

The restriction of an enveloping-algebra map to the corresponding Kostant integral forms.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormMap_apply {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (f : L →ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) (x : ↥(kostantForm e h)) : ↑((kostantFormMap f e h) x) = (map ℚ f) ↑x

The restricted map agrees with the enveloping-algebra map on underlying elements.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantFormMap_surjective {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (f : L →ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) : Function.Surjective ⇑(kostantFormMap f e h)

The restricted map is onto the form generated by the image families. No surjectivity hypothesis on the ambient Lie homomorphism is needed, since the target families are its images.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormEquiv {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (g : L ≃ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) : ↥(kostantForm e h) ≃+* ↥(kostantForm (fun (i : ι) => g (e i)) fun (i : κ) => g (h i))

A Lie equivalence restricts to a ring equivalence between the Kostant forms generated by a family and by its pointwise image.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantFormEquiv g e h = (TauCeti.UniversalEnvelopingAlgebra.mapEquiv ℚ g).toRingEquiv.subringMap.trans (RingEquiv.subringCongr ⋯)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormEquiv_apply {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (g : L ≃ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) (x : ↥(kostantForm e h)) : ↑((kostantFormEquiv g e h) x) = (map ℚ g.toLieHom) ↑x

The restricted equivalence acts by the enveloping-algebra map induced by the original Lie equivalence.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormEquiv_symm_apply {L : Type u} {M : Type v} [LieRing L] [LieAlgebra ℚ L] [LieRing M] [LieAlgebra ℚ M] {ι : Type w} {κ : Type u_1} (g : L ≃ₗ⁅ℚ⁆ M) (e : ι → L) (h : κ → L) (y : ↥(kostantForm (fun (i : ι) => g (e i)) fun (i : κ) => g (h i))) : ↑((kostantFormEquiv g e h).symm y) = (map ℚ g.symm.toLieHom) ↑y

The inverse restricted equivalence acts by the enveloping-algebra map induced by the inverse Lie equivalence.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (g : L ≃ₗ⁅ℚ⁆ L) (e : ι → L) (h : κ → L) (heq : (kostantForm (fun (i : ι) => g (e i)) fun (i : κ) => g (h i)) = kostantForm e h) : ↥(kostantForm e h) ≃+* ↥(kostantForm e h)

A Lie self-equivalence that preserves a Kostant integral form restricts to a ring automorphism of that integral form.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantFormAut g e h heq = (TauCeti.UniversalEnvelopingAlgebra.kostantFormEquiv g e h).trans (RingEquiv.subringCongr heq)

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormAut_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (g : L ≃ₗ⁅ℚ⁆ L) (e : ι → L) (h : κ → L) (heq : (kostantForm (fun (i : ι) => g (e i)) fun (i : κ) => g (h i)) = kostantForm e h) (x : ↥(kostantForm e h)) : ↑((kostantFormAut g e h heq) x) = (map ℚ g.toLieHom) ↑x

The restricted automorphism acts by the enveloping-algebra map induced by the original Lie equivalence.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormAut_symm_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} (g : L ≃ₗ⁅ℚ⁆ L) (e : ι → L) (h : κ → L) (heq : (kostantForm (fun (i : ι) => g (e i)) fun (i : κ) => g (h i)) = kostantForm e h) (x : ↥(kostantForm e h)) : ↑((kostantFormAut g e h heq).symm x) = (map ℚ g.symm.toLieHom) ↑x

The inverse restricted automorphism acts by the enveloping-algebra map induced by the inverse Lie equivalence.

Module representations and stabilized lattices

def TauCeti.UniversalEnvelopingAlgebra.stabilizer {L : Type u} [LieRing L] [LieAlgebra ℚ L] {V : Type u_2} [AddCommGroup V] [Module ℚ V] (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (N : Submodule ℤ V) : Subring (UniversalEnvelopingAlgebra ℚ L)

The subring of elements in the universal enveloping algebra that stabilize a given ℤ-submodule under an algebra representation.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_stabilizer_iff {L : Type u} [LieRing L] [LieAlgebra ℚ L] {V : Type u_2} [AddCommGroup V] [Module ℚ V] (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (N : Submodule ℤ V) (u : UniversalEnvelopingAlgebra ℚ L) : u ∈ stabilizer ρ N ↔ ∀ v ∈ N, (ρ u) v ∈ N

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_le_stabilizer {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (N : Submodule ℤ V) (he : ∀ (i : ι) (n : ℕ), ∀ v ∈ N, (ρ (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) v ∈ N) (hh : ∀ (i : κ) (n : ℕ), ∀ v ∈ N, (ρ (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n)) v ∈ N) : kostantForm e h ≤ stabilizer ρ N

If every divided power of the designated root vectors and every binomial coefficient in the designated Cartan vectors preserves N, then the entire Kostant form stabilizes N.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_apply_mem {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (N : Submodule ℤ V) (he : ∀ (i : ι) (n : ℕ), ∀ v ∈ N, (ρ (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) v ∈ N) (hh : ∀ (i : κ) (n : ℕ), ∀ v ∈ N, (ρ (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n)) v ∈ N) (u : UniversalEnvelopingAlgebra ℚ L) (hu : u ∈ kostantForm e h) {v : V} (hv : v ∈ N) : (ρ u) v ∈ N

The action of an element of the Kostant form on an invariant ℤ-submodule.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantFormRep {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (N : Submodule ℤ V) (he : ∀ (i : ι) (n : ℕ), ∀ v ∈ N, (ρ (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) v ∈ N) (hh : ∀ (i : κ) (n : ℕ), ∀ v ∈ N, (ρ (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n)) v ∈ N) : ↥(kostantForm e h) →ₐ[ℤ] Module.End ℤ ↥N

The restricted representation of the Kostant integral form on an invariant ℤ-submodule N.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_kostantFormRep_apply {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type u_2} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (N : Submodule ℤ V) (he : ∀ (i : ι) (n : ℕ), ∀ v ∈ N, (ρ (Associative.dividedPower n ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) v ∈ N) (hh : ∀ (i : κ) (n : ℕ), ∀ v ∈ N, (ρ (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) n)) v ∈ N) (u : ↥(kostantForm e h)) (v : ↥N) : ↑(((kostantFormRep e h ρ N he hh) u) v) = (ρ ↑u) ↑v

The ambient action of the restricted Kostant representation agrees with the enveloping-algebra representation.