The exponential of a locally nilpotent endomorphism

Let f be an endomorphism of a module M over a semiring R, where M is also a ℚ-vector space. Call f locally nilpotent when every vector is killed by some power of f, the power depending on the vector. Then the exponential series

exp f x = ∑ i, (fⁱ x) / i!

is a finite sum at every vector, and Module.End.locallyNilpotentExp f hf is the resulting R-linear automorphism of M. Its inverse is the exponential of -f.

Mathlib's IsNilpotent.exp exponentiates an element of a ℚ-algebra that is nilpotent, so for an endomorphism it needs a power of f killing every vector at once. For nilpotent f the two exponentials agree (Module.End.locallyNilpotentExp_eq_exp). Local nilpotence without a uniform bound is the situation of the adjoint action of a Chevalley generator on a Lie algebra presented by generators and relations, such as Mathlib's Serre construction Matrix.ToLieAlgebra, which is not known to be finite-dimensional in advance.

Main definitions

• Module.End.locallyNilpotentExp: the exponential of a locally nilpotent endomorphism, as a linear automorphism.

Main results

• Module.End.locallyNilpotentExp_apply_eq_sum: at a vector killed by f ^ k, the exponential is the exponential series truncated at length k.
• Module.End.locallyNilpotentExp_apply_eq_exp_restrict: on an f-stable subspace where f is nilpotent, the exponential is Mathlib's IsNilpotent.exp of the restriction.
• Module.End.locallyNilpotentExp_symm_apply_eq_sum: the inverse is the exponential series of -f.
• Module.End.locallyNilpotentExp_symm: the inverse is the exponential of -f.
• Module.End.map_locallyNilpotentExp: an additive map intertwining two locally nilpotent endomorphisms intertwines their exponentials.
• Module.End.locallyNilpotentExp_eq_exp: for nilpotent f the exponential is IsNilpotent.exp f.

noncomputable def Module.End.locallyNilpotentExp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) : M ≃ₗ[R] M

The exponential of a locally nilpotent endomorphism. If every vector of M is killed by some power of f, the exponential series ∑ (fⁱ x) / i! is a finite sum at every vector x, and it defines an R-linear automorphism of M whose inverse is the exponential series of -f.

theorem Module.End.locallyNilpotentExp_apply_eq_sum {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) {x : M} {k : ℕ} (hk : (f ^ k) x = 0) : (f.locallyNilpotentExp hf) x = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • (f ^ i) x

The exponential as a truncated series. At a vector killed by f ^ k, the exponential of f is its exponential series truncated at length k.

theorem Module.End.locallyNilpotentExp_apply_eq_exp_restrict {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) {V : Submodule ℚ M} (hV : ∀ v ∈ V, (LinearMap.toAddMonoidHom f).toRatLinearMap v ∈ V) {n : ℕ} (hn : (LinearMap.toAddMonoidHom f).toRatLinearMap.restrict hV ^ n = 0) (v : ↥V) : (f.locallyNilpotentExp hf) ↑v = ↑((IsNilpotent.exp ((LinearMap.toAddMonoidHom f).toRatLinearMap.restrict hV)) v)

The exponential on a nilpotent piece. On an f-stable ℚ-subspace V on which f is nilpotent, the exponential of f at a vector of V is Mathlib's IsNilpotent.exp of the restriction of f to V.

theorem Module.End.locallyNilpotentExp_symm_apply_eq_sum {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) {x : M} {k : ℕ} (hk : (f ^ k) x = 0) : (f.locallyNilpotentExp hf).symm x = ∑ i ∈ Finset.range k, (↑i.factorial)⁻¹ • ((-f) ^ i) x

The inverse of the exponential. At a vector killed by f ^ k, the inverse of the exponential of f is the exponential series of -f truncated at length k.

@[simp]

theorem Module.End.locallyNilpotentExp_symm {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) : (f.locallyNilpotentExp hf).symm = (-f).locallyNilpotentExp ⋯

The inverse of the exponential is the exponential of -f.

theorem Module.End.map_locallyNilpotentExp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) {S : Type u_3} {N : Type u_4} {F : Type u_5} [Semiring S] [AddCommGroup N] [Module S N] [Module ℚ N] [FunLike F M N] [AddMonoidHomClass F M N] {f' : End S N} (hf' : ∀ (y : N), ∃ (n : ℕ), (f' ^ n) y = 0) (g : F) (hg : Function.Semiconj ⇑g ⇑f ⇑f') (x : M) : g ((f.locallyNilpotentExp hf) x) = (f'.locallyNilpotentExp hf') (g x)

Naturality of the exponential. An additive map g with g ∘ f = f' ∘ g carries the exponential of f to that of f'. The two endomorphisms may be linear over different semirings.

theorem Module.End.locallyNilpotentExp_eq_exp {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] [Module ℚ M] (f : End R M) (hnil : IsNilpotent f) : ↑(f.locallyNilpotentExp ⋯) = IsNilpotent.exp f

For a nilpotent endomorphism, the exponential is Mathlib's IsNilpotent.exp.