English
A restatement of the previous equivalence in a different form.
Русский
Повторное утверждение предыдущей эквивалентности в иной форме.
LaTeX
$$theorem format: (p.map e) ∈ (e.conj f).invtSubmodule ↔ p ∈ f.invtSubmodule$$
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 for any `n`,
`LinearMap.iterateMapComap f i n K = LinearMap.iterateMapComap f i (n + 1) K`.
In particular, by taking `n = 0`, the kernel of `f` is contained in `K`
(`LinearMap.ker_le_of_iterateMapComap_eq_succ`),
which is a consequence of `LinearMap.ker_le_comap`. -/
theorem 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) (n : ℕ) :
f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K := by
induction n with
| zero =>
contrapose! heq
induction m with
| zero => exact heq
| succ m ih =>
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ']
exact fun H ↦ ih (map_injective_of_injective hi (comap_injective_of_surjective hf H))
| succ n ih =>
rw [iterateMapComap, iterateMapComap, iterate_succ', iterate_succ', Function.comp_apply, Function.comp_apply, ←
iterateMapComap, ← iterateMapComap, ih]
