HepLean Documentation

Mathlib.Algebra.Module.Submodule.IterateMapComap

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 : N →ₗ[R] M) (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
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 : N →ₗ[R] M) (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 : N →ₗ[R] M) (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 : N →ₗ[R] M) (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) :
    LinearMap.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.