Kostant-form stability of a coordinate lattice

A standard Chevalley carrier is built from a rational representation on a coordinate space ι → ℚ whose coordinate ℤ-lattice is preserved by the Kostant integral form. This file proves that stability once, from the two properties every such representation supplies: each designated root operator is square-zero and preserves the coordinate lattice, and each standard coordinate vector is a Cartan weight vector with integral weights. A root operator that cubes rather than squares to zero is covered by the second criterion below, where the divided square is the one further operator whose integrality has to be checked.

Main results

• TauCeti.UniversalEnvelopingAlgebra.ringChoose_apply_mem_coordinateLattice: the Cartan binomial operators preserve the coordinate lattice.
• TauCeti.UniversalEnvelopingAlgebra.kostantForm_apply_mem_coordinateLattice: the whole Kostant form preserves the coordinate lattice.

References

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

This is a shared prerequisite for the Chevalley--Demazure carriers in Layer 9 of TauCetiRoadmap/ReductiveGroups/README.md.

theorem TauCeti.UniversalEnvelopingAlgebra.ringChoose_apply_mem_coordinateLattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type v} {ι : Type u_1} [Finite ι] [DecidableEq ι] (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ (ι → ℚ)) {wt : ι → κ → ℤ} (hwt : ∀ (a : ι), IsCartanWeightVector h ρ (wt a) (Pi.single a 1)) (i : κ) (m : ℕ) {v : ι → ℚ} (hv : v ∈ coordinateLattice ι) : (ρ (Ring.choose ((UniversalEnvelopingAlgebra.ι ℚ) (h i)) m)) v ∈ coordinateLattice ι

Every Cartan binomial operator preserves the coordinate lattice, because the standard coordinate vectors are weight vectors with integral weights.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_apply_mem_coordinateLattice_of_pow_eq_zero {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type v} {ν : Type w} {ι : Type u_1} [Finite ι] [DecidableEq ι] (e : ν → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ (ι → ℚ)) {wt : ι → κ → ℤ} (d : ℕ) (hpow : ∀ (k : ν), ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)) ^ d = 0) (hstab : ∀ (k : ν), ∀ m < d, ∀ v ∈ coordinateLattice ι, (Associative.dividedPower m (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)))) v ∈ coordinateLattice ι) (hwt : ∀ (a : ι), IsCartanWeightVector h ρ (wt a) (Pi.single a 1)) {u : UniversalEnvelopingAlgebra ℚ L} (hu : u ∈ kostantForm e h) {v : ι → ℚ} (hv : v ∈ coordinateLattice ι) : (ρ u) v ∈ coordinateLattice ι

The coordinate lattice is Kostant-stable when each root operator is nilpotent with a common bound and all divided powers below that bound preserve the lattice.

theorem TauCeti.UniversalEnvelopingAlgebra.kostantForm_apply_mem_coordinateLattice {L : Type u} [LieRing L] [LieAlgebra ℚ L] {κ : Type v} {ν : Type w} {ι : Type u_1} [Finite ι] [DecidableEq ι] (e : ν → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ (ι → ℚ)) {wt : ι → κ → ℤ} (hsq : ∀ (k : ν), ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k)) ^ 2 = 0) (hstab : ∀ (k : ν), ∀ v ∈ coordinateLattice ι, (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e k))) v ∈ coordinateLattice ι) (hwt : ∀ (a : ι), IsCartanWeightVector h ρ (wt a) (Pi.single a 1)) {u : UniversalEnvelopingAlgebra ℚ L} (hu : u ∈ kostantForm e h) {v : ι → ℚ} (hv : v ∈ coordinateLattice ι) : (ρ u) v ∈ coordinateLattice ι

The coordinate lattice of a standard representation is an admissible lattice. The Kostant ℤ-form presented by square-zero root operators and Cartan operators with integral coordinate weights preserves the coordinate ℤ-lattice.