Mathlib.RingTheory.OrzechProperty

Module docstring

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

OrzechProperty structure

Full source

/-- 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

Orzech Property of Rings

Informal description

A ring $R$ satisfies the *Orzech property* if for any finitely generated $R$-module $M$, any surjective homomorphism $f \colon N \to M$ from a submodule $N$ of $M$ to $M$ is injective. This property was introduced in works by Orzech, Djoković, and Ribenboim under the names $\Pi$-ring or $\Pi_1$-ring. It implies the strong rank condition for nontrivial rings (i.e., the existence of an injective linear map $(\text{Fin } n \to R) \hookrightarrow (\text{Fin } m \to R)$ implies $n \leq m$).

OrzechProperty.injective_of_surjective_of_injective theorem

{N : Type w} [AddCommMonoid N] [Module R N] (i f : N →ₗ[R] M) (hi : Injective i) (hf : Surjective f) : Injective f

Full source

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 : ShrinkShrink.{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

Injectivity of Surjective Linear Maps in Orzech Property Rings

Informal description

Let $R$ be a ring with the Orzech property, and let $M$ be a finitely generated $R$-module. For any $R$-module $N$ with an injective linear map $i \colon N \to M$ and a surjective linear map $f \colon N \to M$, the map $f$ is injective.

OrzechProperty.injective_of_surjective_of_submodule theorem

{N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f

Full source

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

Injectivity of Surjective Linear Maps from Submodules in Orzech Property Rings

Informal description

Let $R$ be a ring with the Orzech property and $M$ a finitely generated $R$-module. For any submodule $N$ of $M$ and any surjective $R$-linear map $f \colon N \to M$, the map $f$ is injective.

OrzechProperty.injective_of_surjective_endomorphism theorem

(f : M →ₗ[R] M) (hf : Surjective f) : Injective f

Full source

theorem injective_of_surjective_endomorphism
    (f : M →ₗ[R] M) (hf : Surjective f) : Injective f :=
  injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective hf

Injectivity of Surjective Endomorphisms in Orzech Property Rings

Informal description

Let $R$ be a ring with the Orzech property and $M$ a finitely generated $R$-module. For any surjective $R$-linear endomorphism $f \colon M \to M$, the map $f$ is injective.

OrzechProperty.bijective_of_surjective_endomorphism theorem

(f : M →ₗ[R] M) (hf : Surjective f) : Bijective f

Full source

theorem bijective_of_surjective_endomorphism
    (f : M →ₗ[R] M) (hf : Surjective f) : Bijective f :=
  ⟨injective_of_surjective_endomorphism f hf, hf⟩

Bijectivity of Surjective Endomorphisms in Orzech Property Rings

Informal description

Let $R$ be a ring with the Orzech property and $M$ a finitely generated $R$-module. For any surjective $R$-linear endomorphism $f \colon M \to M$, the map $f$ is bijective.