doc-next-gen

Mathlib.Algebra.Module.Submodule.IterateMapComap

Module docstring

{"# 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].

"}

LinearMap.iterateMapComap definition
(n : ℕ)
Full source 
/-- The `LinearMap.iterateMapComap f i n K : Submodule R N` is
`f⁻¹(i(⋯(f⁻¹(i(K)))))` (`n` times). -/
def iterateMapComap (n : ℕ) := (fun K : Submodule R N ↦ (K.map i).comap f)^[n]
Iterated preimage-image composition of submodules
Informal description
Given a linear map \( f : N \to M \), an injective linear map \( i : N \to M \), a submodule \( K \subseteq N \), and a natural number \( n \), the \( n \)-th iterate of the map-comap operation is defined as \( f^{-1}(i(\cdots(f^{-1}(i(K))))) \) (applied \( n \) times), where: - \( f^{-1} \) denotes the preimage under \( f \) - \( i \) is applied to the submodule before taking the preimage More formally, \( \text{iterateMapComap}_f^i(n, K) \) is defined recursively by: - \( \text{iterateMapComap}_f^i(0, K) = K \) - \( \text{iterateMapComap}_f^i(n+1, K) = f^{-1}(i(\text{iterateMapComap}_f^i(n, K))) \)
LinearMap.iterateMapComap_le_succ theorem
(K : Submodule R N) (h : K.map f ≤ K.map i) (n : ℕ) : f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K
Full source 
/-- If `f(K) ≤ i(K)`, then `LinearMap.iterateMapComap` is not decreasing. -/
theorem iterateMapComap_le_succ (K : Submodule R N) (h : K.map f ≤ K.map i) (n : ℕ) :
    f.iterateMapComap i n K ≤ f.iterateMapComap i (n + 1) K := by
  nth_rw 2 [iterateMapComap]
  rw [iterate_succ', Function.comp_apply, ← iterateMapComap, ← map_le_iff_le_comap]
  induction n with
  | zero => exact h
  | succ n ih =>
    simp_rw [iterateMapComap, iterate_succ', Function.comp_apply]
    calc
      _ ≤ (f.iterateMapComap i n K).map i := map_comap_le _ _
      _ ≤ (((f.iterateMapComap i n K).map f).comap f).map i := map_mono (le_comap_map _ _)
      _ ≤ _ := map_mono (comap_mono ih)
Monotonicity of Iterated Map-Comap Operation under Submodule Inclusion
Informal description
Let $R$ be a semiring, $N$ and $M$ be $R$-modules, and $f : N \to M$ and $i : N \to M$ be $R$-linear maps. For any submodule $K \subseteq N$ such that $f(K) \subseteq i(K)$, and for any natural number $n$, the $n$-th iterate of the map-comap operation satisfies: \[ \text{iterateMapComap}_f^i(n, K) \subseteq \text{iterateMapComap}_f^i(n+1, K), \] where $\text{iterateMapComap}_f^i(n, K) = f^{-1}(i(\cdots(f^{-1}(i(K))))) $ (applied $n$ times).
LinearMap.iterateMapComap_eq_succ theorem
(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
Full source 
/-- 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]
Stabilization of Iterated Map-Comap Operation for Surjective and Injective Linear Maps
Informal description
Let $R$ be a semiring, $N$ and $M$ be $R$-modules, and $f \colon N \to M$ and $i \colon N \to M$ be $R$-linear maps. Suppose that: 1. $f$ is surjective, 2. $i$ is injective, 3. There exists a natural number $m$ such that $\text{iterateMapComap}_f^i(m, K) = \text{iterateMapComap}_f^i(m+1, K)$ for a submodule $K \subseteq N$. Then for any natural number $n$, we have: \[ \text{iterateMapComap}_f^i(n, K) = \text{iterateMapComap}_f^i(n+1, K), \] where $\text{iterateMapComap}_f^i(n, K) = f^{-1}(i(\cdots(f^{-1}(i(K))))) $ (applied $n$ times). In particular, taking $n = 0$ shows that the kernel of $f$ is contained in $K$.
LinearMap.ker_le_of_iterateMapComap_eq_succ theorem
(K : Submodule R N) (m : ℕ) (heq : f.iterateMapComap i m K = f.iterateMapComap i (m + 1) K) (hf : Surjective f) (hi : Injective i) : LinearMap.ker f ≤ K
Full source 
/-- 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. -/
theorem ker_le_of_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) : LinearMap.ker f ≤ K := by
  rw [show K = _ from f.iterateMapComap_eq_succ i K m heq hf hi 0]
  exact f.ker_le_comap
Kernel containment under stabilization of iterated map-comap operation
Informal description
Let $R$ be a semiring, $N$ and $M$ be $R$-modules, and $f \colon N \to M$ and $i \colon N \to M$ be $R$-linear maps. Suppose that: 1. $f$ is surjective, 2. $i$ is injective, 3. There exists a natural number $m$ such that $\text{iterateMapComap}_f^i(m, K) = \text{iterateMapComap}_f^i(m+1, K)$ for a submodule $K \subseteq N$. Then the kernel of $f$ is contained in $K$, i.e., $\ker f \subseteq K$.