Documentation

TauCeti.Algebra.Lie.UniversalEnveloping.Kostant.Exponential

Root subgroup elements of a Kostant integral form #

Let L be a Lie algebra over ℚ with distinguished root vectors e : ι → L and Cartan vectors h : κ → L, and let U_ℤ = kostantForm e h be the integral form they generate inside UniversalEnvelopingAlgebra ℚ L. A root vector eᵢ need not be nilpotent in the enveloping algebra itself — a nonzero Chevalley root vector never is, the enveloping algebra being a domain — but whenever its image under an algebra map f is nilpotent — an extra hypothesis throughout, satisfied by the finite-dimensional representations the construction is applied to —

x_i(t) = exp (t • f (ι ℚ (eᵢ))) = ∑ n, tⁿ • f (eᵢ⁽ⁿ⁾)

makes sense and has integer coefficients on the images of the root-vector generators of the Kostant form. What is built here is this integral-point family of units, indexed by t : ℤ; a later development is to exhibit it as the ℤ-points of a root subgroup map x_α : 𝔾ₐ → G of the Chevalley--Demazure construction. No scheme, and no morphism of schemes, appears below.

The results below record what integrality buys. First, x_i(t) lies in the image of the Kostant form. Second, and this is the form the construction of a Chevalley group actually uses, x_i(t) preserves any additive subgroup of a representation that the Kostant form preserves — an admissible lattice. Both statements are for an arbitrary integer t, which is exactly the range of scalars for which the rational coefficients tⁿ/n! of the ordinary exponential series recombine into integers.

The divided-power expansion, the one-parameter group law x_i(t) x_i(u) = x_i(t + u) and the general stability statements are TauCeti/RingTheory/Nilpotent/Exp.lean; nothing here re-proves them. Nothing here assumes the Chevalley relations either: the results hold for any families of distinguished vectors, and a pinned root datum will supply the specific ones.

Main results #

References #

Root subgroup elements inside the integral form #

source
theorem TauCeti.UniversalEnvelopingAlgebra.exp_zsmul_mem_map_kostantForm {L : Type u} [LieRing L] [LieAlgebra ℚ L] {ι : Type w} {κ : Type u_1} {A : Type v} [Ring A] [Algebra ℚ A] (e : ι → L) (h : κ → L) (f : UniversalEnvelopingAlgebra ℚ L →ₐ[ℚ] A) {i : ι} (hnil : IsNilpotent (f ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : ℤ) :
IsNilpotent.exp (t • f ((UniversalEnvelopingAlgebra.ι ℚ) (e i))) ∈ Subring.map (↑f) (kostantForm e h)

A root subgroup element exp (t • f (eᵢ)) lies in the image of the Kostant integral form.

The exponential is an a priori rational combination of powers of f (eᵢ); the content is that it is an integral combination of the images of the root-vector generators eᵢ⁽ⁿ⁾.

Root subgroup elements act on admissible lattices #

source
theorem TauCeti.UniversalEnvelopingAlgebra.dividedPower_apply_mem_of_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) {M : AddSubgroup V} (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) (i : ι) (n : ℕ) {v : V} (hv : v ∈ M) :
(Associative.dividedPower n (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) v ∈ M

Every designated root vector's divided powers preserve an additive subgroup stable under the whole Kostant form.

source
theorem TauCeti.UniversalEnvelopingAlgebra.exp_zsmul_apply_mem_of_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) {M : AddSubgroup V} (hM : ∀ u ∈ kostantForm e h, ∀ v ∈ M, (ρ u) v ∈ M) {i : ι} (hnil : IsNilpotent (ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) (t : ℤ) {v : V} (hv : v ∈ M) :
(IsNilpotent.exp (t • ρ ((UniversalEnvelopingAlgebra.ι ℚ) (e i)))) v ∈ M

A root subgroup element preserves an admissible lattice. If an additive subgroup M of a representation V of L is stable under the Kostant integral form, then it is stable under every root subgroup element exp (t • ρ (eᵢ)) with t an integer.

Only stability under the divided powers of the single root vector eᵢ is used; that weaker statement is TauCeti.exp_zsmul_smul_mem.

Stability of M under the whole group generated by these elements follows, since the inverse of exp (t • ρ (eᵢ)) is exp (-t • ρ (eᵢ)), of the same shape. This is how a Chevalley group is cut out as a group of automorphisms of a lattice.