Stabilising ranges of iterates #
Once the decreasing chain range f ⊇ range f² ⊇ ⋯ of an endomorphism f stops at stage n, the
kernel and the range of f ^ n together span the module. Unlike Mathlib's
LinearMap.eventually_codisjoint_ker_pow_range_pow, no Artinian hypothesis is needed: it only
serves to make the chain stop.
theorem
LinearMap.range_pow_add_eq_of_range_pow_succ_eq
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommMonoid M]
[Module R M]
{f : Module.End R M}
{n : ℕ}
(h : range (f ^ (n + 1)) = range (f ^ n))
(m : ℕ)
:
If the range of f ^ (n + 1) equals that of f ^ n, the ranges of all higher powers of f
equal it too.
theorem
LinearMap.codisjoint_ker_pow_range_pow_of_range_pow_succ_eq
{R : Type u_1}
{M : Type u_2}
[Semiring R]
[AddCommGroup M]
[Module R M]
{f : Module.End R M}
{n : ℕ}
(h : range (f ^ (n + 1)) = range (f ^ n))
:
Codisjoint (ker (f ^ n)) (range (f ^ n))
If the range of f ^ (n + 1) equals that of f ^ n, the kernel and the range of f ^ n
together span the module.