The integral exponential of a nilpotent element

Let A be an associative ℚ-algebra and x : A a nilpotent element. Mathlib's IsNilpotent.exp x is the finite sum ∑ i, xⁱ / i!. This file rewrites that sum in terms of the divided powers x⁽ⁱ⁾ = xⁱ / i! of TauCeti/RingTheory/DividedPowers/Associative.lean, so that

exp (t • x) = ∑ i, tⁱ • x⁽ⁱ⁾

has integer coefficients when t is an integer. Consequently exp (t • x) lies in any additive subgroup containing the divided powers of x, and it preserves any additive subgroup of a module that the divided powers of x preserve. The map t ↦ exp (t • x) is a homomorphism from the additive group of integers to Aˣ, whose values lie in such an additive subgroup.

This is the shape of a root subgroup map x_α : 𝔾ₐ → G of a Chevalley--Demazure group scheme: the divided powers of Chevalley root vectors are among the generators of the Kostant ℤ-form, so the exponentials above preserve an integral lattice. The application to the Kostant form is in TauCeti/Algebra/Lie/UniversalEnveloping/Kostant/Exponential.lean.

Main results

• TauCeti.nilpotencyClass_le_of_pow_eq_zero: a vanishing power bounds the nilpotency class.
• TauCeti.exp_smul_eq_sum_smul_dividedPower: the rescaled expansion exp (r • x) = ∑ rⁱ • x⁽ⁱ⁾.
• TauCeti.exp_zsmul_eq_sum_zsmul_dividedPower: the same expansion with integer coefficients.
• TauCeti.exp_zsmul_mem: exp (t • x) lies in an additive subgroup holding the divided powers of x.
• TauCeti.exp_zsmul_smul_mem: exp (t • x) preserves an additive subgroup that the divided powers of x preserve.
• TauCeti.nilpotentExpUnit: the exponential of a nilpotent element as a unit.
• TauCeti.expZSMulHom: the integer-parameter group of units t ↦ exp (t • x).
• TauCeti.expZSMulAddAut: the induced action by additive automorphisms on an additive subgroup preserved by the divided powers of x.

References

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

theorem TauCeti.nilpotencyClass_le_of_pow_eq_zero {R : Type u_1} [Zero R] [Pow R ℕ] {x : R} {n : ℕ} (h : x ^ n = 0) : nilpotencyClass x ≤ n

Any vanishing power gives an upper bound for the nilpotency class.

The divided-power expansion

theorem TauCeti.exp_smul_eq_sum_smul_dividedPower {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} {k : ℕ} (hk : x ^ k = 0) (r : ℚ) : IsNilpotent.exp (r • x) = ∑ i ∈ Finset.range k, r ^ i • Associative.dividedPower i x

The exponential of a rational multiple of a nilpotent element, expanded in divided powers.

The divided powers themselves do not depend on the scalar: rescaling x only rescales the coefficients.

theorem TauCeti.exp_zsmul_eq_sum_zsmul_dividedPower {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} {k : ℕ} (hk : x ^ k = 0) (t : ℤ) : IsNilpotent.exp (t • x) = ∑ i ∈ Finset.range k, t ^ i • Associative.dividedPower i x

The exponential of an integer multiple of a nilpotent element has integer coefficients on the divided powers. This is the integrality that lets a root subgroup map be defined over ℤ.

theorem TauCeti.exp_zsmul_mem {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} (hx : IsNilpotent x) {S : Type u_3} [SetLike S A] [AddSubgroupClass S A] {T : S} (hT : ∀ (i : ℕ), Associative.dividedPower i x ∈ T) (t : ℤ) : IsNilpotent.exp (t • x) ∈ T

An additive subgroup containing every divided power of a nilpotent element contains every integral exponential of it.

theorem TauCeti.exp_zsmul_smul_mem {A : Type u_2} [Ring A] [Algebra ℚ A] {V : Type u_3} [AddCommGroup V] [Module A V] {x : A} (hx : IsNilpotent x) {S : Type u_4} [SetLike S V] [AddSubgroupClass S V] {M : S} (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (t : ℤ) {v : V} (hv : v ∈ M) : IsNilpotent.exp (t • x) • v ∈ M

An additive subgroup of a module that is stable under the action of every divided power of a nilpotent element is stable under the action of every integral exponential of it.

For the divided powers of a Chevalley root vector this says that a root subgroup element preserves an admissible lattice.

The one-parameter group of units

noncomputable def TauCeti.nilpotentExpUnit {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} (hx : IsNilpotent x) : Aˣ

The unit exp x attached to a nilpotent element x, with inverse exp (-x).

For a Chevalley root vector this is the root subgroup element x_α (1).

Equations

• TauCeti.nilpotentExpUnit hx = { val := IsNilpotent.exp x, inv := IsNilpotent.exp (-x), val_inv := ⋯, inv_val := ⋯ }

@[simp]

theorem TauCeti.coe_nilpotentExpUnit {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} (hx : IsNilpotent x) : ↑(nilpotentExpUnit hx) = IsNilpotent.exp x

Coercing nilpotentExpUnit hx to A yields exp x.

@[simp]

theorem TauCeti.coe_inv_nilpotentExpUnit {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} (hx : IsNilpotent x) : ↑(nilpotentExpUnit hx)⁻¹ = IsNilpotent.exp (-x)

Coercing the inverse of nilpotentExpUnit hx to A yields exp (-x).

noncomputable def TauCeti.expZSMulHom {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} (hx : IsNilpotent x) : Multiplicative ℤ →* Aˣ

The one-parameter group of units t ↦ exp (t • x) attached to a nilpotent element x.

For a Chevalley root vector this is the root subgroup map x_α evaluated on the integral points of the additive group.

Equations

• TauCeti.expZSMulHom hx = { toFun := fun (t : Multiplicative ℤ) => TauCeti.nilpotentExpUnit ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.coe_expZSMulHom {A : Type u_2} [Ring A] [Algebra ℚ A] {x : A} (hx : IsNilpotent x) (t : Multiplicative ℤ) : ↑((expZSMulHom hx) t) = IsNilpotent.exp (Multiplicative.toAdd t • x)

Coercing the integer-parameter-group value expZSMulHom hx t to A yields exp (Multiplicative.toAdd t • x).

The action on an invariant additive subgroup

noncomputable def TauCeti.expZSMulAddAut {A : Type u_2} [Ring A] [Algebra ℚ A] {V : Type u_3} [AddCommGroup V] [Module A V] {x : A} (hx : IsNilpotent x) {S : Type u_4} [SetLike S V] [AddSubgroupClass S V] (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) : Multiplicative ℤ →* Multiplicative (AddAut ↥M)

Integral exponentials act on a divided-power-stable additive subgroup by additive automorphisms. This is the restriction of expZSMulHom hx from units of the ambient algebra to automorphisms of the invariant subgroup.

Equations

• TauCeti.expZSMulAddAut hx M hM = { toFun := fun (t : Multiplicative ℤ) => Multiplicative.ofAdd (TauCeti.expZSMulAddEquiv✝ hx M hM t), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem TauCeti.coe_expZSMulAddAut {A : Type u_2} [Ring A] [Algebra ℚ A] {V : Type u_3} [AddCommGroup V] [Module A V] {x : A} (hx : IsNilpotent x) {S : Type u_4} [SetLike S V] [AddSubgroupClass S V] (M : S) (hM : ∀ (n : ℕ), ∀ v ∈ M, Associative.dividedPower n x • v ∈ M) (t : Multiplicative ℤ) (v : ↥M) : ↑((Multiplicative.toAdd ((expZSMulAddAut hx M hM) t)) v) = IsNilpotent.exp (Multiplicative.toAdd t • x) • ↑v

The action of expZSMulAddAut on the invariant subgroup is the ambient nilpotent exponential.