Theorems · Theorem · commutative algebra

LinearMap.ker_le_of_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 → f.ker ≤ 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 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.

Defined in

Mathlib.Algebra.Module.Submodule.IterateMapComap

Cited by

1 results in Mathlib

Foundations

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

Assumes

SemiringAddCommMonoidModuleAddCommMonoidModule