Inverting 1 + f for a locally nilpotent endomorphism

An endomorphism f of a module is locally nilpotent when every vector is annihilated by some power of f. Then 1 + f is invertible. No global nilpotence bound is needed, so the statement applies to operators which lower a filtration by direct summands without being nilpotent on the whole module, such as those of homological perturbation theory on bar constructions.

On a free module ι →₀ R, an endomorphism is locally nilpotent as soon as it strictly lowers a weight on the basis whose strict order is well-founded, for instance any weight on a finite basis.

Main results

• Module.End.isUnit_one_add_of_forall_exists_pow_apply_eq_zero: 1 + f is a unit when f is locally nilpotent.
• TauCeti.LinearMap.IsHomogeneous.ringInverse_one_add: the inverse of 1 + f has degree zero when f is locally nilpotent of degree zero.
• Module.End.exists_pow_apply_eq_zero_of_forall_mem_support_lt: an endomorphism of ι →₀ R that strictly lowers a well-founded weight on the basis is locally nilpotent.

theorem Module.End.isUnit_one_add_of_forall_exists_pow_apply_eq_zero {R : Type u_1} {M : Type u_2} [Semiring R] [AddCommGroup M] [Module R M] (f : End R M) (hf : ∀ (x : M), ∃ (n : ℕ), (f ^ n) x = 0) : IsUnit (1 + f)

If every vector is annihilated by some power of f, then 1 + f is invertible.

theorem TauCeti.LinearMap.IsHomogeneous.ringInverse_one_add {S : Type u_3} {N : Type u_4} [Ring S] [AddCommGroup N] [Module S N] {ι : Type u_5} [AddMonoid ι] {𝒜 : ι → Submodule S N} {f : Module.End S N} (hf : IsHomogeneous f 𝒜 𝒜 0) (hnil : ∀ (x : N), ∃ (n : ℕ), (f ^ n) x = 0) : IsHomogeneous (Ring.inverse (1 + f)) 𝒜 𝒜 0

If f is locally nilpotent and homogeneous of degree zero for a grading by submodules, then so is the inverse of 1 + f: on a homogeneous vector it is a finite geometric series in -f.

theorem Module.End.exists_pow_apply_eq_zero_of_forall_mem_support_lt {R : Type u_3} {ι : Type u_4} {α : Type u_5} [Semiring R] [LT α] (f : End R (ι →₀ R)) (w : ι → α) (hw : WellFounded (InvImage (fun (x1 x2 : α) => x1 < x2) w)) (hf : ∀ (i j : ι), j ∈ (f (Finsupp.single i 1)).support → w j < w i) (x : ι →₀ R) : ∃ (k : ℕ), (f ^ k) x = 0

Strictly lowering a well-founded weight on a basis is locally nilpotent. Let w be a weight on ι whose strict order w j < w i is well-founded, as is automatic when ι is finite and α is a preorder, or when < is well-founded on α. If an endomorphism f of ι →₀ R sends each basis vector single i 1 into the span of the basis vectors of strictly smaller weight, then every vector is killed by a power of f.