feat: left-Noetherian rings and commutative rings satisfy OrzechProperty (#13425)

This is part 2 of #12076.

It states that if

- `R` is a ring (not necessarily commutative) and `M` is a Noetherian `R`-module (based on the proof in <https://math.stackexchange.com/a/1066128>), or
- `R` is a commutative ring and `M` is a finitely generated `R`-module (based on the proof in <https://math.stackexchange.com/a/1066110>),

if `N` is a submodule of `M`, `f : N -> M` is a surjective `R`-module homomorphism, then it is also injective.

These results generalize `(IsNoetherian|Module.Finite).injective_of_surjective_endomorphism`.

The proof for Noetherian case uses `LinearMap.iterateMapComap` which is put into `Mathlib/Algebra/Module/Submodule/IterateMapComap.lean`.

The changed proof makes `LinearMap.tunnel` and `LinearMap.tailing` not used in any other parts of mathlib. Remove them or not is leaved for future discussion.

Author: acmepjz

Mathlib.lean

@@ -413,6 +413,7 @@ import Mathlib.Algebra.Module.Prod
 import Mathlib.Algebra.Module.Projective
 import Mathlib.Algebra.Module.Submodule.Basic
 import Mathlib.Algebra.Module.Submodule.Bilinear
+import Mathlib.Algebra.Module.Submodule.IterateMapComap
 import Mathlib.Algebra.Module.Submodule.Ker
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.Algebra.Module.Submodule.LinearMap

Mathlib/Algebra/Module/Submodule/IterateMapComap.lean

@@ -0,0 +1,94 @@
+/-
+Copyright (c) 2024 Jz Pan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jz Pan
+-/
+import Mathlib.Algebra.Module.Submodule.Ker
+
+/-!
+
+# 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].
+
+-/
+
+open Function Submodule
+
+namespace LinearMap
+
+variable {R N M : Type*} [Semiring R] [AddCommMonoid N] [Module R N]
+  [AddCommMonoid M] [Module R M] (f i : N →ₗ[R] M)
+
+/-- 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]
+
+/-- 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)
+
+/-- 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]
+
+/-- 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
+
+end LinearMap

Mathlib/LinearAlgebra/InvariantBasisNumber.lean

@@ -38,6 +38,10 @@ It is also useful to consider the following stronger conditions:
 
 ## Instances
 
+- `IsNoetherianRing.orzechProperty` (defined in `Mathlib/RingTheory/Noetherian.lean`) :
+  any left-noetherian ring satisfies the Orzech property.
+  This applies in particular to division rings.
+
 - `strongRankCondition_of_orzechProperty` : the Orzech property implies the strong rank condition
   (for non trivial rings).
 
@@ -50,11 +54,11 @@ It is also useful to consider the following stronger conditions:
   invariant basis number property.
 
 - `invariantBasisNumber_of_nontrivial_of_commRing`: a nontrivial commutative ring satisfies
-  the invariant basis number property
+  the invariant basis number property.
 
-More generally, every commutative ring satisfies the strong rank condition. This is proved in
-`LinearAlgebra/FreeModule/StrongRankCondition`. We keep
-`invariantBasisNumber_of_nontrivial_of_commRing` here since it imports fewer files.
+More generally, every commutative ring satisfies the Orzech property,
+hence the strong rank condition, which is proved in `Mathlib/RingTheory/FiniteType.lean`.
+We keep `invariantBasisNumber_of_nontrivial_of_commRing` here since it imports fewer files.
 
 
 ## Counterexamples to converse results
@@ -263,30 +267,10 @@ section
 
 variable (R : Type u) [Ring R] [Nontrivial R] [IsNoetherianRing R]
 
--- Note this includes fields,
--- and we use this below to show any commutative ring has invariant basis number.
-/-- Any nontrivial noetherian ring satisfies the strong rank condition.
-
-An injective map `((Fin n ⊕ Fin (1 + m)) → R) →ₗ[R] (Fin n → R)` for some left-noetherian `R`
-would force `Fin (1 + m) → R ≃ₗ PUnit` (via `IsNoetherian.equivPUnitOfProdInjective`),
-which is not the case!
--/
-instance (priority := 100) IsNoetherianRing.strongRankCondition : StrongRankCondition R := by
-  constructor
-  intro m n f i
-  by_contra h
-  rw [not_le, ← Nat.add_one_le_iff, le_iff_exists_add] at h
-  obtain ⟨m, rfl⟩ := h
-  let e : Fin (n + 1 + m) ≃ Sum (Fin n) (Fin (1 + m)) :=
-    (finCongr (add_assoc _ _ _)).trans finSumFinEquiv.symm
-  let f' :=
-    f.comp
-      ((LinearEquiv.sumArrowLequivProdArrow _ _ R R).symm.trans
-          (LinearEquiv.funCongrLeft R R e)).toLinearMap
-  have i' : Injective f' := i.comp (LinearEquiv.injective _)
-  apply @zero_ne_one (Fin (1 + m) → R) _ _
-  apply (IsNoetherian.equivPUnitOfProdInjective f' i').injective
-  ext
+/-- Any nontrivial noetherian ring satisfies the strong rank condition,
+    since it satisfies Orzech property. -/
+instance (priority := 100) IsNoetherianRing.strongRankCondition : StrongRankCondition R :=
+  inferInstance
 #align noetherian_ring_strong_rank_condition IsNoetherianRing.strongRankCondition
 
 end

Mathlib/RingTheory/FiniteType.lean

@@ -706,6 +706,96 @@ end MonoidAlgebra
 
 end MonoidAlgebra
 
+section Orzech
+
+open Submodule Module Module.Finite in
+/-- Any commutative ring `R` satisfies the `OrzechProperty`, that is, for any finitely generated
+`R`-module `M`, any surjective homomorphism `f : N →ₗ[R] M` from a submodule `N` of `M` to `M`
+is injective.
+
+This is a consequence of Noetherian case
+(`IsNoetherian.injective_of_surjective_of_injective`), which requires that `M` is a
+Noetherian module, but allows `R` to be non-commutative. The reduction of this result to
+Noetherian case is adapted from <https://math.stackexchange.com/a/1066110>:
+suppose `{ m_j }` is a finite set of generator of `M`, for any `n : N` one can write
+`i n = ∑ j, b_j * m_j` for `{ b_j }` in `R`, here `i : N →ₗ[R] M` is the standard inclusion.
+We can choose `{ n_j }` which are preimages of `{ m_j }` under `f`, and can choose
+`{ c_jl }` in `R` such that `i n_j = ∑ l, c_jl * m_l` for each `j`.
+Now let `A` be the subring of `R` generated by `{ b_j }` and `{ c_jl }`, then it is
+Noetherian. Let `N'` be the `A`-submodule of `N` generated by `n` and `{ n_j }`,
+`M'` be the `A`-submodule of `M` generated by `{ m_j }`,
+then it's easy to see that `i` and `f` restrict to `N' →ₗ[A] M'`,
+and the restricted version of `f` is surjective, hence by Noetherian case,
+it is also injective, in particular, if `f n = 0`, then `n = 0`.
+
+See also Orzech's original paper: *Onto endomorphisms are isomorphisms* [orzech1971]. -/
+instance (priority := 100) CommRing.orzechProperty
+    (R : Type*) [CommRing R] : OrzechProperty R := by
+  refine ⟨fun {M} _ _ _ {N} f hf ↦ ?_⟩
+  letI := addCommMonoidToAddCommGroup R (M := M)
+  letI := addCommMonoidToAddCommGroup R (M := N)
+  let i := N.subtype
+  let hi : Function.Injective i := N.injective_subtype
+  refine LinearMap.ker_eq_bot.1 <| LinearMap.ker_eq_bot'.2 fun n hn ↦ ?_
+  obtain ⟨k, mj, hmj⟩ := exists_fin (R := R) (M := M)
+  rw [← surjective_piEquiv_apply_iff] at hmj
+  obtain ⟨b, hb⟩ := hmj (i n)
+  choose nj hnj using fun j ↦ hf (mj j)
+  choose c hc using fun j ↦ hmj (i (nj j))
+  let A := Subring.closure (Set.range b ∪ Set.range c.uncurry)
+  let N' := span A ({n} ∪ Set.range nj)
+  let M' := span A (Set.range mj)
+  haveI : IsNoetherianRing A := is_noetherian_subring_closure _
+    (.union (Set.finite_range _) (Set.finite_range _))
+  haveI : Module.Finite A M' := span_of_finite A (Set.finite_range _)
+  refine congr($((LinearMap.ker_eq_bot'.1 <| LinearMap.ker_eq_bot.2 <|
+    IsNoetherian.injective_of_surjective_of_injective
+      ((i.restrictScalars A).restrict fun x hx ↦ ?_ : N' →ₗ[A] M')
+      ((f.restrictScalars A).restrict fun x hx ↦ ?_ : N' →ₗ[A] M')
+      (fun _ _ h ↦ injective_subtype _ (hi congr(($h).1)))
+      fun ⟨x, hx⟩ ↦ ?_) ⟨n, (subset_span (by simp))⟩ (Subtype.val_injective hn)).1)
+  · induction hx using span_induction' with
+    | mem x hx =>
+      change i x ∈ M'
+      simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
+      rcases hx with hx | ⟨j, rfl⟩
+      · rw [hx, ← hb, piEquiv_apply_apply]
+        refine Submodule.sum_mem _ fun j _ ↦ ?_
+        let b' : A := ⟨b j, Subring.subset_closure (by simp)⟩
+        rw [show b j • mj j = b' • mj j from rfl]
+        exact smul_mem _ _ (subset_span (by simp))
+      · rw [← hc, piEquiv_apply_apply]
+        refine Submodule.sum_mem _ fun j' _ ↦ ?_
+        let c' : A := ⟨c j j', Subring.subset_closure
+          (by simp [show ∃ a b, c a b = c j j' from ⟨j, j', rfl⟩])⟩
+        rw [show c j j' • mj j' = c' • mj j' from rfl]
+        exact smul_mem _ _ (subset_span (by simp))
+    | zero => simp
+    | add x _ y _ hx hy => rw [map_add]; exact add_mem hx hy
+    | smul a x _ hx => rw [map_smul]; exact smul_mem _ _ hx
+  · induction hx using span_induction' with
+    | mem x hx =>
+      change f x ∈ M'
+      simp only [Set.singleton_union, Set.mem_insert_iff, Set.mem_range] at hx
+      rcases hx with hx | ⟨j, rfl⟩
+      · rw [hx, hn]; exact zero_mem _
+      · exact subset_span (by simp [hnj])
+    | zero => simp
+    | add x _ y _ hx hy => rw [map_add]; exact add_mem hx hy
+    | smul a x _ hx => rw [map_smul]; exact smul_mem _ _ hx
+  suffices x ∈ LinearMap.range ((f.restrictScalars A).domRestrict N') by
+    obtain ⟨a, ha⟩ := this
+    exact ⟨a, Subtype.val_injective ha⟩
+  induction hx using span_induction' with
+  | mem x hx =>
+    obtain ⟨j, rfl⟩ := hx
+    exact ⟨⟨nj j, subset_span (by simp)⟩, hnj j⟩
+  | zero => exact zero_mem _
+  | add x _ y _ hx hy => exact add_mem hx hy
+  | smul a x _ hx => exact smul_mem _ a hx
+
+end Orzech
+
 section Vasconcelos
 
 /-- A theorem/proof by Vasconcelos, given a finite module `M` over a commutative ring, any

Mathlib/RingTheory/Noetherian.lean

@@ -4,7 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro, Kevin Buzzard
 -/
 import Mathlib.Order.Filter.EventuallyConst
-import Mathlib.RingTheory.Finiteness
+import Mathlib.Order.PartialSups
+import Mathlib.Algebra.Module.Submodule.IterateMapComap
+import Mathlib.RingTheory.OrzechProperty
 import Mathlib.RingTheory.Nilpotent.Lemmas
 
 #align_import ring_theory.noetherian from "leanprover-community/mathlib"@"210657c4ea4a4a7b234392f70a3a2a83346dfa90"
@@ -456,14 +458,31 @@ lemma LinearMap.eventually_iSup_ker_pow_eq (f : M →ₗ[R] M) :
   · rw [← hn _ (hm.trans h), hn _ hm]
   · exact f.iterateKer.monotone h.le
 
+/-- **Orzech's theorem** for Noetherian module: if `R` is a ring (not necessarily commutative),
+`M` and `N` are `R`-modules, `M` is Noetherian, `i : N →ₗ[R] M` is injective,
+`f : N →ₗ[R] M` is surjective, then `f` is also injective. The proof here is adapted from
+Djoković's paper *Epimorphisms of modules which must be isomorphisms* [djokovic1973],
+utilizing `LinearMap.iterateMapComap`.
+See also Orzech's original paper: *Onto endomorphisms are isomorphisms* [orzech1971]. -/
+theorem IsNoetherian.injective_of_surjective_of_injective (i f : N →ₗ[R] M)
+    (hi : Injective i) (hf : Surjective f) : Injective f := by
+  haveI := isNoetherian_of_injective i hi
+  obtain ⟨n, H⟩ := monotone_stabilizes_iff_noetherian.2 ‹_›
+    ⟨_, monotone_nat_of_le_succ <| f.iterateMapComap_le_succ i ⊥ (by simp)⟩
+  exact LinearMap.ker_eq_bot.1 <| bot_unique <|
+    f.ker_le_of_iterateMapComap_eq_succ i ⊥ n (H _ (Nat.le_succ _)) hf hi
+
+/-- **Orzech's theorem** for Noetherian module: if `R` is a ring (not necessarily commutative),
+`M` is a Noetherian `R`-module, `N` is a submodule, `f : N →ₗ[R] M` is surjective, then `f` is also
+injective. -/
+theorem IsNoetherian.injective_of_surjective_of_submodule
+    {N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f :=
+  IsNoetherian.injective_of_surjective_of_injective N.subtype f N.injective_subtype hf
+
 /-- Any surjective endomorphism of a Noetherian module is injective. -/
 theorem IsNoetherian.injective_of_surjective_endomorphism (f : M →ₗ[R] M)
-    (s : Surjective f) : Injective f := by
-  obtain ⟨n, hn⟩ := eventually_atTop.mp f.eventually_disjoint_ker_pow_range_pow
-  specialize hn (n + 1) (n.le_add_right 1)
-  rw [disjoint_iff, LinearMap.range_eq_top.mpr (LinearMap.iterate_surjective s _), inf_top_eq,
-    LinearMap.ker_eq_bot] at hn
-  exact LinearMap.injective_of_iterate_injective n.succ_ne_zero hn
+    (s : Surjective f) : Injective f :=
+  IsNoetherian.injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective s
 #align is_noetherian.injective_of_surjective_endomorphism IsNoetherian.injective_of_surjective_endomorphism
 
 /-- Any surjective endomorphism of a Noetherian module is bijective. -/
@@ -494,16 +513,17 @@ theorem IsNoetherian.disjoint_partialSups_eventually_bot
 #align is_noetherian.disjoint_partial_sups_eventually_bot IsNoetherian.disjoint_partialSups_eventually_bot
 
 /-- If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial. -/
-noncomputable def IsNoetherian.equivPUnitOfProdInjective (f : M × N →ₗ[R] M)
-    (i : Injective f) : N ≃ₗ[R] PUnit.{w + 1} := by
-  apply Nonempty.some
-  obtain ⟨n, w⟩ :=
-    IsNoetherian.disjoint_partialSups_eventually_bot (f.tailing i) (f.tailings_disjoint_tailing i)
-  specialize w n (le_refl n)
-  apply Nonempty.intro
-  refine (LinearMap.tailingLinearEquiv f i n).symm ≪≫ₗ ?_
-  rw [w]
-  apply Submodule.botEquivPUnit
+theorem IsNoetherian.subsingleton_of_prod_injective (f : M × N →ₗ[R] M)
+    (i : Injective f) : Subsingleton N := .intro fun x y ↦ by
+  have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective
+  simpa using h (show LinearMap.fst R M N (0, x) = LinearMap.fst R M N (0, y) from rfl)
+
+/-- If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial. -/
+@[simps!]
+def IsNoetherian.equivPUnitOfProdInjective (f : M × N →ₗ[R] M)
+    (i : Injective f) : N ≃ₗ[R] PUnit.{w + 1} :=
+  haveI := IsNoetherian.subsingleton_of_prod_injective f i
+  .ofSubsingleton _ _
 #align is_noetherian.equiv_punit_of_prod_injective IsNoetherian.equivPUnitOfProdInjective
 
 end
@@ -624,3 +644,12 @@ theorem IsNoetherianRing.isNilpotent_nilradical (R : Type*) [CommRing R] [IsNoet
   obtain ⟨n, hn⟩ := Ideal.exists_radical_pow_le_of_fg (⊥ : Ideal R) (IsNoetherian.noetherian _)
   exact ⟨n, eq_bot_iff.mpr hn⟩
 #align is_noetherian_ring.is_nilpotent_nilradical IsNoetherianRing.isNilpotent_nilradical
+
+/-- Any Noetherian ring satisfies Orzech property.
+See also `IsNoetherian.injective_of_surjective_of_submodule` and
+`IsNoetherian.injective_of_surjective_of_injective`. -/
+instance (priority := 100) IsNoetherianRing.orzechProperty
+    (R) [Ring R] [IsNoetherianRing R] : OrzechProperty R where
+  injective_of_surjective_of_submodule' {M} :=
+    letI := Module.addCommMonoidToAddCommGroup R (M := M)
+    IsNoetherian.injective_of_surjective_of_submodule