diff --git a/Mathlib.lean b/Mathlib.lean index ca4b72887681b..24de57deea637 100644 --- 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 index 6fe7190ffe0d3..8fbe87b518af7 100644 --- 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 ): + +- 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 new file mode 100644 index 0000000000000..89dd344899873 --- /dev/null +++ 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 index 61cd82f7754b0..1beb5caf7a3ba 100644 --- 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},