Theorems · Theorem · commutative algebra

LinearMap.iterateMapComap_eq_succ

∀ {R : Type u_1} {N : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid N] [inst_2 : Module R N]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (m : ℕ),
  f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K →
    Function.Surjective ⇑f → Function.Injective ⇑i → ∀ (n : ℕ), f.iterateMapComap i n K = f.iterateMapComap i (n + 1) K

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.

Defined in

Mathlib.Algebra.Module.Submodule.IterateMapComap

Cited by

1 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule