# 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

source
class OrzechProperty (R : Type u) [Semiring R] :
Prop

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`.

- 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) : Function.Surjective ⇑f → Function.Injective ⇑f

Instances

source
theorem orzechProperty_iff (R : Type u) [Semiring R] :
OrzechProperty R ↔ ∀ {M : Type u} [inst : AddCommMonoid M] [inst_1 : Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M), Function.Surjective ⇑f → Function.Injective ⇑f
source
theorem OrzechProperty.injective_of_surjective_of_injective {R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] {N : Type w} [AddCommMonoid N] [Module R N] (i f : N →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : Function.Surjective ⇑f) :
Function.Injective ⇑f
source
theorem OrzechProperty.injective_of_surjective_of_submodule {R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] {N : Submodule R M} (f : ↥N →ₗ[R] M) (hf : Function.Surjective ⇑f) :
Function.Injective ⇑f
source
theorem OrzechProperty.injective_of_surjective_endomorphism {R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] (f : M →ₗ[R] M) (hf : Function.Surjective ⇑f) :
Function.Injective ⇑f
source
theorem OrzechProperty.bijective_of_surjective_endomorphism {R : Type u} [Semiring R] [OrzechProperty R] {M : Type v} [AddCommMonoid M] [Module R M] [Module.Finite R M] (f : M →ₗ[R] M) (hf : Function.Surjective ⇑f) :
Function.Bijective ⇑f