Kostant root subgroups as natural point representations

The divided-power exponential attached to a nilpotent root-vector action gives a homomorphism from 𝔾ₐ(A) to the automorphisms of A ⊗[ℤ] M for every commutative ℤ-algebra A. This file packages those homomorphisms and their value-ring naturality as a HopfAlgebra.PointRepresentation. The representation--comodule correspondence then recovers the coordinate-side polynomial coaction

m ↦ ∑ₙ D⁽ⁿ⁾(m) ⊗ Xⁿ.

Once integral PBW supplies a finite free admissible lattice, a basis turns this point representation into the natural matrix-valued map used to recover the root-subgroup scheme morphism 𝔾ₐ → GLₙ.

Main declarations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPointRepresentation: the natural point representation of 𝔾ₐ defined by the Kostant exponential.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupComodule: the polynomial comodule recovered from that natural action.
• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupComodule_coact: the explicit divided-power formula for its coaction.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, §§26--27.
• R. W. Carter, Simple Groups of Lie Type, §4.4.
• J. C. Jantzen, Representations of Algebraic Groups, II.1.

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPointRepresentation {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) : HopfAlgebra.PointRepresentation

The natural point representation of 𝔾ₐ on a Kostant-stable integral module attached to a nilpotent root-vector action.

Its component over a commutative ring A is the divided-power exponential homomorphism kostantRootSubgroupPoints; naturality is the compatibility of that polynomial action with maps of value rings.

Equations

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

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPointRepresentation_action {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (A : CommAlgCat ℤ) : (kostantRootSubgroupPointRepresentation e h ρ M hM i hnil).action A = GrpCat.ofHom (kostantRootSubgroupPoints e h ρ M hM i hnil)

At every categorical value ring, the concrete action is the Kostant root-subgroup point homomorphism.

@[irreducible]

noncomputable def TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupComodule {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) : Comodule ℤ (SymmetricAlgebra ℤ ℤ) ↥M

The right ℤ[X]-comodule on a Kostant-stable integral module encoded by the natural root-subgroup action. This is the coordinate-side form of the divided-power exponential.

Equations

• TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupComodule e h ρ M hM i hnil = (TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupPointRepresentation e h ρ M hM i hnil).toComodule

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.kostantRootSubgroupComodule_coact {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ m ∈ M, (ρ u) m ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (m : ↥M) : Comodule.coact m = ∑ n ∈ Finset.range (nilpotencyClass (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))), (integralDividedPower (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M n ⋯) m ⊗ₜ[ℤ] ((SymmetricAlgebra.ι ℤ ℤ) 1 ^ n)

The Kostant root-subgroup coaction is the finite divided-power polynomial m ↦ ∑ₙ D⁽ⁿ⁾(m) ⊗ Xⁿ.