# Iterate maps and comaps of submodules #

Some preliminary work for establishing the strong rank condition for Noetherian rings.

Given two linear maps `f i : N →ₗ[R] M` and a submodule `K : Submodule R N`, we can define `LinearMap.iterateMapComap f i n K : Submodule R N` to be `f⁻¹(i(⋯(f⁻¹(i(K)))))` (`n` times). If `f(K) ≤ i(K)`, then this sequence is non-decreasing (`LinearMap.iterateMapComap_le_succ`). On the other hand, 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`. 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.

The construction here is adapted from the proof in Djoković's paper Epimorphisms of modules which must be isomorphisms [djokovic1973].

source
def LinearMap.iterateMapComap {R : Type u_1} {N : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid N] [Module R N] [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M) (n : ℕ) :
Submodule R N → Submodule R N

The `LinearMap.iterateMapComap f i n K : Submodule R N` is `f⁻¹(i(⋯(f⁻¹(i(K)))))` (`n` times).

Equations

- f.iterateMapComap i n = (fun (K : Submodule R N) => Submodule.comap f (Submodule.map i K))^[n]

Instances For

source
theorem LinearMap.iterateMapComap_le_succ {R : Type u_1} {N : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid N] [Module R N] [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (h : Submodule.map f K ≤ Submodule.map i K) (n : ℕ) :
f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K

If `f(K) ≤ i(K)`, then `LinearMap.iterateMapComap` is not decreasing.

source
theorem LinearMap.iterateMapComap_eq_succ {R : Type u_1} {N : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid N] [Module R N] [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (m : ℕ) (heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K) (hf : Function.Surjective ⇑f) (hi : 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`.

source
theorem LinearMap.ker_le_of_iterateMapComap_eq_succ {R : Type u_1} {N : Type u_2} {M : Type u_3} [Semiring R] [AddCommMonoid N] [Module R N] [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M) (K : Submodule R N) (m : ℕ) (heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K) (hf : Function.Surjective ⇑f) (hi : Function.Injective ⇑i) :
ker f ≤ 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.