feat: add the definition of OrzechProperty (#13322)

This is part one of #12076. `OrzechProperty R` is a type class stating that `R` satisfies the following property: for any finitely generated `R`-module `M`, any surjective homomorphism `f : N → M` from a submodule `N` of `M` to `M` is injective. We stated some basic results about `OrzechProperty` and proved that it implies `StrongRankCondition`.
leanprover-community · May 31, 2024 · 86ab5d5 · 86ab5d5
1 parent 57716b0
commit 86ab5d5
Show file tree

Hide file tree

Showing 4 changed files with 215 additions and 19 deletions.
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -3572,6 +3572,7 @@ import Mathlib.RingTheory.NormTrace
 import Mathlib.RingTheory.Nullstellensatz
 import Mathlib.RingTheory.OreLocalization.Basic
 import Mathlib.RingTheory.OreLocalization.OreSet
+import Mathlib.RingTheory.OrzechProperty
 import Mathlib.RingTheory.Perfection
 import Mathlib.RingTheory.PiTensorProduct
 import Mathlib.RingTheory.Polynomial.Basic

diff --git a/Mathlib/LinearAlgebra/InvariantBasisNumber.lean b/Mathlib/LinearAlgebra/InvariantBasisNumber.lean
@@ -3,6 +3,7 @@ Copyright (c) 2020 Markus Himmel. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Markus Himmel, Scott Morrison
 -/
+import Mathlib.RingTheory.OrzechProperty
 import Mathlib.RingTheory.Ideal.Quotient
 import Mathlib.RingTheory.PrincipalIdealDomain
 
@@ -11,35 +12,63 @@ import Mathlib.RingTheory.PrincipalIdealDomain
 /-!
 # Invariant basis number property
 
-We say that a ring `R` satisfies the invariant basis number property if there is a well-defined
-notion of the rank of a finitely generated free (left) `R`-module. Since a finitely generated free
-module with a basis consisting of `n` elements is linearly equivalent to `Fin n → R`, it is
-sufficient that `(Fin n → R) ≃ₗ[R] (Fin m → R)` implies `n = m`.
+## Main definitions
 
-It is also useful to consider two stronger conditions, namely the rank condition,
-that a surjective linear map `(Fin n → R) →ₗ[R] (Fin m → R)` implies `m ≤ n` and
-the strong rank condition, that an injective linear map `(Fin n → R) →ₗ[R] (Fin m → R)`
-implies `n ≤ m`.
+Let `R` be a (not necessary commutative) ring.
 
-The strong rank condition implies the rank condition, and the rank condition implies
-the invariant basis number property.
+- `InvariantBasisNumber R` is a type class stating that `(Fin n → R) ≃ₗ[R] (Fin m → R)`
+  implies `n = m`, a property known as the *invariant basis number property.*
 
-## Main definitions
+  This assumption implies that there is a well-defined notion of the rank
+  of a finitely generated free (left) `R`-module.
+
+It is also useful to consider the following stronger conditions:
+
+- the *rank condition*, witnessed by the type class `RankCondition R`, states that
+  the existence of a surjective linear map `(Fin n → R) →ₗ[R] (Fin m → R)` implies `m ≤ n`
+
+- the *strong rank condition*, witnessed by the type class `StrongRankCondition R`, states
+  that the existence of an injective linear map `(Fin n → R) →ₗ[R] (Fin m → R)`
+  implies `n ≤ m`.
+
+- `OrzechProperty R`, defined in `Mathlib/RingTheory/OrzechProperty.lean`,
+  states that for any finitely generated `R`-module `M`, any surjective homomorphism `f : N → M`
+  from a submodule `N` of `M` to `M` is injective.
+
+
+## Instances
 
-`StrongRankCondition R` is a type class stating that `R` satisfies the strong rank condition.
-`RankCondition R` is a type class stating that `R` satisfies the rank condition.
-`InvariantBasisNumber R` is a type class stating that `R` has the invariant basis number property.
+- `strongRankCondition_of_orzechProperty` : the Orzech property implies the strong rank condition
+  (for non trivial rings).
 
-## Main results
+- `IsNoetherianRing.strongRankCondition` : every nontrivial left-noetherian ring satisfies the
+  strong rank condition (and so in particular every division ring or field).
 
-We show that every nontrivial left-noetherian ring satisfies the strong rank condition,
-(and so in particular every division ring or field),
-and then use this to show every nontrivial commutative ring has the invariant basis number property.
+- `rankCondition_of_strongRankCondition` : the strong rank condition implies the rank condition.
+
+- `invariantBasisNumber_of_rankCondition` : the rank condition implies the
+  invariant basis number property.
+
+- `invariantBasisNumber_of_nontrivial_of_commRing`: a nontrivial commutative ring satisfies
+  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.
 
+
+## Counterexamples to converse results
+
+The following examples can be found in the book of Lam [lam_1999]
+(see also <https://math.stackexchange.com/questions/4711904>):
+
+- Let `k` be a field, then the free (non-commutative) algebra `k⟨x, y⟩` satisfies
+  the rank condition but not the strong rank condition.
+- The free (non-commutative) algebra `ℚ⟨a, b, c, d⟩` quotient by the
+  two-sided ideal `(ac − 1, bd − 1, ab, cd)` satisfies the invariant basis number property
+  but not the rank condition.
+
+
 ## Future work
 
 So far, there is no API at all for the `InvariantBasisNumber` class. There are several natural
@@ -56,10 +85,15 @@ variants) should be formalized.
 
 * https://en.wikipedia.org/wiki/Invariant_basis_number
 * https://mathoverflow.net/a/2574/
+* [Lam, T. Y. *Lectures on Modules and Rings*][lam_1999]
+* [Orzech, Morris. *Onto endomorphisms are isomorphisms*][orzech1971]
+* [Djoković, D. Ž. *Epimorphisms of modules which must be isomorphisms*][djokovic1973]
+* [Ribenboim, Paulo.
+  *Épimorphismes de modules qui sont nécessairement des isomorphismes*][ribenboim1971]
 
 ## Tags
 
-free module, rank, invariant basis number, IBN
+free module, rank, Orzech property, (strong) rank condition, invariant basis number, IBN
 
 -/
 
@@ -101,6 +135,22 @@ theorem strongRankCondition_iff_succ :
         (hf.comp (Function.extend_injective (Fin.strictMono_castLE _).injective _))
 #align strong_rank_condition_iff_succ strongRankCondition_iff_succ
 
+/-- Any nontrivial ring satisfying Orzech property also satisfies strong rank condition. -/
+instance (priority := 100) strongRankCondition_of_orzechProperty
+    [Nontrivial R] [OrzechProperty R] : StrongRankCondition R := by
+  refine (strongRankCondition_iff_succ R).2 fun n i hi ↦ ?_
+  let f : (Fin (n + 1) → R) →ₗ[R] Fin n → R := {
+    toFun := fun x ↦ x ∘ Fin.castSucc
+    map_add' := fun _ _ ↦ rfl
+    map_smul' := fun _ _ ↦ rfl
+  }
+  have h : (0 : Fin (n + 1) → R) = update (0 : Fin (n + 1) → R) (Fin.last n) 1 := by
+    apply OrzechProperty.injective_of_surjective_of_injective i f hi
+      (Fin.castSucc_injective _).surjective_comp_right
+    ext m
+    simp [f, update_apply, (Fin.castSucc_lt_last m).ne]
+  simpa using congr_fun h (Fin.last n)
+
 theorem card_le_of_injective [StrongRankCondition R] {α β : Type*} [Fintype α] [Fintype β]
     (f : (α → R) →ₗ[R] β → R) (i : Injective f) : Fintype.card α ≤ Fintype.card β := by
   let P := LinearEquiv.funCongrLeft R R (Fintype.equivFin α)

diff --git a/Mathlib/RingTheory/OrzechProperty.lean b/Mathlib/RingTheory/OrzechProperty.lean
@@ -0,0 +1,96 @@
+/-
+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.RingTheory.Finiteness
+import Mathlib.Logic.Equiv.TransferInstance
+
+/-!
+
+# Orzech property of rings
+
+In this file we define the following property of rings:
+
+- `OrzechProperty R` is a type class stating that `R` satisfies the following property:
+  for any finitely generated `R`-module `M`, any surjective homomorphism `f : N → M`
+  from a submodule `N` of `M` to `M` is injective.
+  It was introduced in papers by Orzech [orzech1971], Djoković [djokovic1973] and
+  Ribenboim [ribenboim1971], under the names `Π`-ring or `Π₁`-ring.
+  It implies the strong rank condition (that is, the existence of an injective linear map
+  `(Fin n → R) →ₗ[R] (Fin m → R)` implies `n ≤ m`)
+  if the ring is nontrivial (see `Mathlib/LinearAlgebra/InvariantBasisNumber.lean`).
+
+It's proved in the above papers that
+
+- a left Noetherian ring (not necessarily commutative) satisfies the `OrzechProperty`,
+  which in particular includes the division ring case
+  (see `Mathlib/RingTheory/Noetherian.lean`);
+- a commutative ring satisfies the `OrzechProperty`
+  (see `Mathlib/RingTheory/FiniteType.lean`).
+
+## References
+
+* [Orzech, Morris. *Onto endomorphisms are isomorphisms*][orzech1971]
+* [Djoković, D. Ž. *Epimorphisms of modules which must be isomorphisms*][djokovic1973]
+* [Ribenboim, Paulo.
+  *Épimorphismes de modules qui sont nécessairement des isomorphismes*][ribenboim1971]
+
+## Tags
+
+free module, rank, Orzech property, (strong) rank condition, invariant basis number, IBN
+
+-/
+
+universe u v w
+
+open Function
+
+variable (R : Type u) [Semiring R]
+
+/-- A ring `R` satisfies the Orzech property, if for any finitely generated `R`-module `M`,
+any surjective homomorphism `f : N → M` from a submodule `N` of `M` to `M` is injective.
+
+NOTE: In the definition we need to assume that `M` has the same universe level as `R`, but it
+in fact implies the universe polymorphic versions
+`OrzechProperty.injective_of_surjective_of_injective`
+and `OrzechProperty.injective_of_surjective_of_submodule`. -/
+@[mk_iff]
+class OrzechProperty : Prop where
+  injective_of_surjective_of_submodule' : ∀ {M : Type u} [AddCommMonoid M] [Module R M]
+    [Module.Finite R M] {N : Submodule R M} (f : N →ₗ[R] M), Surjective f → Injective f
+
+namespace OrzechProperty
+
+variable {R}
+
+variable [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M]
+
+theorem injective_of_surjective_of_injective
+    {N : Type w} [AddCommMonoid N] [Module R N]
+    (i f : N →ₗ[R] M) (hi : Injective i) (hf : Surjective f) : Injective f := by
+  obtain ⟨n, g, hg⟩ := Module.Finite.exists_fin' R M
+  haveI := small_of_surjective hg
+  letI := Equiv.addCommMonoid (equivShrink M).symm
+  letI := Equiv.module R (equivShrink M).symm
+  let j : Shrink.{u} M ≃ₗ[R] M := Equiv.linearEquiv R (equivShrink M).symm
+  haveI := Module.Finite.equiv j.symm
+  let i' := j.symm.toLinearMap ∘ₗ i
+  replace hi : Injective i' := by simpa [i'] using hi
+  let f' := j.symm.toLinearMap ∘ₗ f ∘ₗ (LinearEquiv.ofInjective i' hi).symm.toLinearMap
+  replace hf : Surjective f' := by simpa [f'] using hf
+  simpa [f'] using injective_of_surjective_of_submodule' f' hf
+
+theorem injective_of_surjective_of_submodule
+    {N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f :=
+  injective_of_surjective_of_injective N.subtype f N.injective_subtype hf
+
+theorem injective_of_surjective_endomorphism
+    (f : M →ₗ[R] M) (hf : Surjective f) : Injective f :=
+  injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective hf
+
+theorem bijective_of_surjective_endomorphism
+    (f : M →ₗ[R] M) (hf : Surjective f) : Bijective f :=
+  ⟨injective_of_surjective_endomorphism f hf, hf⟩
+
+end OrzechProperty
diff --git a/docs/references.bib b/docs/references.bib
@@ -989,6 +989,23 @@ @Article{         dieudonne1953
   url           = {https://doi.org/10.2307/2031832}
 }
 
+@Article{         djokovic1973,
+  author        = {Djokovi\'{c}, D. \v{Z}.},
+  title         = {Epimorphisms of modules which must be isomorphisms},
+  journal       = {Canad. Math. Bull.},
+  fjournal      = {Canadian Mathematical Bulletin. Bulletin Canadien de
+                  Math\'{e}matiques},
+  volume        = {16},
+  year          = {1973},
+  pages         = {513--515},
+  issn          = {0008-4395,1496-4287},
+  mrclass       = {16A64},
+  mrnumber      = {346014},
+  mrreviewer    = {M.\ Teply},
+  doi           = {10.4153/CMB-1973-083-0},
+  url           = {https://doi.org/10.4153/CMB-1973-083-0}
+}
+
 @Article{         dolan1976,
   title         = {A {{Proof}} of {{Jacobson}}'s {{Theorem}}},
   author        = {Dolan, S. W.},
@@ -2527,6 +2544,22 @@ @Article{         orosi2018faulhaber
   zbl           = {1411.41023}
 }
 
+@Article{         orzech1971,
+  author        = {Orzech, Morris},
+  title         = {Onto endomorphisms are isomorphisms},
+  journal       = {Amer. Math. Monthly},
+  fjournal      = {American Mathematical Monthly},
+  volume        = {78},
+  year          = {1971},
+  pages         = {357--362},
+  issn          = {0002-9890,1930-0972},
+  mrclass       = {13.40},
+  mrnumber      = {280475},
+  mrreviewer    = {M.\ Teply},
+  doi           = {10.2307/2316897},
+  url           = {https://doi.org/10.2307/2316897}
+}
+
 @Book{            oxley2011,
   author        = {Oxley, James},
   title         = {Matroid Theory},
@@ -2599,6 +2632,22 @@ @Misc{            pöschel2017siegelsternberg
   primaryclass  = {math.DS}
 }
 
+@InCollection{    ribenboim1971,
+  author        = {Ribenboim, Paulo},
+  title         = {\'{E}pimorphismes de modules qui sont n\'{e}cessairement
+                  des isomorphismes},
+  booktitle     = {S\'{e}minaire {P}. {D}ubreil, {M}.-{L}.
+                  {D}ubreil-{J}acotin, {L}. {L}esieur et {C}. {P}isot
+                  (24\`eme ann\'{e}e: 1970/71), {A}lg\`ebre et th\'{e}orie
+                  des nombres, {F}asc. 2},
+  pages         = {Exp. No. 19, 5},
+  publisher     = {\'{E}d. Acad. RS Roumanie, Bucharest},
+  year          = {1971},
+  mrclass       = {16A52},
+  mrnumber      = {393128},
+  mrreviewer    = {Jonathan\ Golan}
+}
+
 @Book{            riehl2017,
   author        = {Riehl, Emily},
   title         = {Category theory in context},