Root subgroup actions on base changes of Kostant-stable additive subgroups

Let L be a Lie algebra over ℚ, and let U_ℤ = kostantForm e h be the Kostant integral form in UniversalEnvelopingAlgebra ℚ L. When M ≤ V is stable under ρ(U_ℤ), every divided power of ρ(eᵢ) preserves M, since those divided powers lie in U_ℤ.

Combining this with the generic base-change exponential from TauCeti/RingTheory/Nilpotent/BaseChangeAction.lean, we obtain the additive one-parameter action of an arbitrary commutative ring R on R ⊗[ℤ] M attached to each root vector eᵢ whose image ρ(eᵢ) is nilpotent.

Main definitions and results

• TauCeti.UniversalEnvelopingAlgebra.baseChangeKostantExpHom: the root-vector one-parameter subgroup on an arbitrary base change of a Kostant-stable additive subgroup for each root vector whose image is nilpotent.
• TauCeti.UniversalEnvelopingAlgebra.baseChangeKostantExpHom_toLinearMap: its underlying linear map is the base-changed exponential.
• TauCeti.UniversalEnvelopingAlgebra.coe_baseChangeKostantExpHom: coercing the base-changed Kostant root subgroup to a function yields the base-changed exponential.

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.baseChangeKostantExpHom {V : Type u} [AddCommGroup V] [Module ℚ V] {R : Type v} [CommRing R] [Algebra ℤ R] {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_2} (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) : Multiplicative R →* TensorProduct ℤ R ↥M ≃ₗ[R] TensorProduct ℤ R ↥M

The root-vector one-parameter subgroup on an arbitrary base change of a Kostant-stable additive subgroup, for a root vector whose image is nilpotent.

For each commutative ring R, the parameter t : R acts on R ⊗[ℤ] M through the integral divided-power polynomial of ρ(eᵢ). This is the ring-valued action that underlies the root subgroup map attached to eᵢ in the Chevalley--Demazure construction.

Equations

• TauCeti.UniversalEnvelopingAlgebra.baseChangeKostantExpHom e h ρ M hM i hnil = TauCeti.baseChangeExpHom (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ hnil

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.baseChangeKostantExpHom_toLinearMap {V : Type u} [AddCommGroup V] [Module ℚ V] {R : Type v} [CommRing R] [Algebra ℤ R] {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_2} (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : Multiplicative R) : ↑((baseChangeKostantExpHom e h ρ M hM i hnil) t) = baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ (Multiplicative.toAdd t)

The underlying linear map of the base-changed Kostant root subgroup is the integral divided-power exponential.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.coe_baseChangeKostantExpHom {V : Type u} [AddCommGroup V] [Module ℚ V] {R : Type v} [CommRing R] [Algebra ℤ R] {L : Type u_1} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_2} (e : ι → L) (h : κ → L) (ρ : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] Module.End ℚ V) (M : AddSubgroup V) (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : Multiplicative R) : ⇑((baseChangeKostantExpHom e h ρ M hM i hnil) t) = ⇑(baseChangeExp (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) M ⋯ (Multiplicative.toAdd t))

Coercing the base-changed Kostant root subgroup to a function yields the base-changed exponential.