English
If f is surjective and i is injective and there is m with f.iterateMapComap i m K = f.iterateMapComap i (m+1) K, then ker f ≤ K.
Русский
Если f сюръективен и i инъективен и существует m с f.iterateMapComap i m K = f.iterateMapComap i (m+1) K, то ker f ≤ K.
LaTeX
$$Eq (f.iterateMapComap i m K) (f.iterateMapComap i (m+1) K) → Surjective f → Injective i → LinearMap.ker f ≤ K$$
Lean4
/-- If `f` is surjective, `i` is injective, and there exists some `m` such that
`LinearMap.iterateMapComap f i m K = LinearMap.iterateMapComap f i (m + 1) K`,
then the kernel of `f` is contained in `K`.
This is a corollary of `LinearMap.iterateMapComap_eq_succ` and `LinearMap.ker_le_comap`.
As a special case, if one can take `K` to be zero,
then `f` is injective. This is the key result for establishing the strong rank condition
for Noetherian rings. -/
theorem ker_le_of_iterateMapComap_eq_succ (K : Submodule R N) (m : ℕ)
(heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K) (hf : Surjective f) (hi : Injective i) :
LinearMap.ker f ≤ K := by
rw [show K = _ from f.iterateMapComap_eq_succ i K m heq hf hi 0]
exact f.ker_le_comap
