Integral exponential actions on Kostant-stable additive subgroups

Let U_ℤ = kostantForm e h be a Kostant integral form in U(L), let ρ be a representation of U(L) on a rational vector space V, and let M ≤ V be an additive subgroup preserved by ρ(U_ℤ). If the endomorphism ρ(eᵢ) is nilpotent, the integral exponentials

x_i(t) = exp (t ρ(eᵢ)),   t ∈ ℤ,

preserve M. This file packages preservation into an action-level statement: the maps x_i(t) form a group homomorphism from the additive group of integers to the additive automorphisms of M.

The construction uses TauCeti.expZSMulAddAut, which packages the action of integral nilpotent exponentials on any additive subgroup stable under the corresponding divided powers. Stability under the whole Kostant form supplies that hypothesis because the divided powers of every designated root vector are Kostant generators.

Main results

• TauCeti.UniversalEnvelopingAlgebra.expZSMulKostantAddAut: integral exponentials attached to e i act by additive automorphisms on every Kostant-stable additive subgroup.
• TauCeti.UniversalEnvelopingAlgebra.expZSMulKostantOrbitAddAut: the canonical specialization to the integral orbit generated by a vector under the Kostant form.

This advances Layer 9, “Root subgroup maps,” of the ReductiveGroups roadmap. When specialized to distinguished root vectors and admissible lattices, these automorphisms supply the pointwise algebra assembled into the root subgroup morphisms x_α : 𝔾ₐ → G of the pinned Chevalley--Demazure group scheme.

References

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

noncomputable def TauCeti.UniversalEnvelopingAlgebra.expZSMulKostantAddAut {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) {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (M : S) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) : Multiplicative ℤ →* Multiplicative (AddAut ↥M)

Integral exponentials attached to e i act by additive automorphisms on an additive subgroup preserved by the Kostant form.

The target is the additive automorphism group of M, written multiplicatively so that the one-parameter group law is exposed as a MonoidHom. No freeness or finite-generation assumption on M is needed for this action-level statement.

Equations

• TauCeti.UniversalEnvelopingAlgebra.expZSMulKostantAddAut e h ρ M hM i hnil = TauCeti.expZSMulAddAut hnil M ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_expZSMulKostantAddAut {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) {S : Type u_2} [SetLike S V] [AddSubgroupClass S V] (M : S) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : Multiplicative ℤ) (v : ↥M) : ↑((Multiplicative.toAdd ((expZSMulKostantAddAut e h ρ M hM i hnil) t)) v) = (IsNilpotent.exp (Multiplicative.toAdd t • ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) ↑v

The integral exponential action on a Kostant-stable additive subgroup is the ambient nilpotent exponential.

The action on the canonical Kostant orbit

noncomputable def TauCeti.UniversalEnvelopingAlgebra.expZSMulKostantOrbitAddAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] [Module (UniversalEnvelopingAlgebra ℚ L) V] [IsScalarTower ℚ (UniversalEnvelopingAlgebra ℚ L) V] (e : ι → L) (h : κ → L) (v : V) (i : ι) (hnil : IsNilpotent ((Algebra.lsmul ℚ ℚ V) ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) : Multiplicative ℤ →* Multiplicative (AddAut ↥(kostantOrbit e h v))

Integral exponentials attached to e i act by additive automorphisms on the Kostant orbit generated by v.

Unlike expZSMulKostantAddAut, this specialization has no separate stability hypothesis: the Kostant orbit is stable under the whole Kostant form by construction. The only remaining hypothesis is the representation-theoretic condition that e i acts nilpotently on V.

Equations

• TauCeti.UniversalEnvelopingAlgebra.expZSMulKostantOrbitAddAut e h v i hnil = TauCeti.expZSMulAddAut hnil (TauCeti.UniversalEnvelopingAlgebra.kostantOrbit e h v) ⋯

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_expZSMulKostantOrbitAddAut {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {V : Type v} [AddCommGroup V] [Module ℚ V] [Module (UniversalEnvelopingAlgebra ℚ L) V] [IsScalarTower ℚ (UniversalEnvelopingAlgebra ℚ L) V] (e : ι → L) (h : κ → L) (v : V) (i : ι) (hnil : IsNilpotent ((Algebra.lsmul ℚ ℚ V) ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : Multiplicative ℤ) (x : ↥(kostantOrbit e h v)) : ↑((Multiplicative.toAdd ((expZSMulKostantOrbitAddAut e h v i hnil) t)) x) = (IsNilpotent.exp (Multiplicative.toAdd t • (Algebra.lsmul ℚ ℚ V) ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) ↑x

On the ambient rational representation, the integral exponential action on the Kostant orbit is the nilpotent exponential of the endomorphism attached to e i.