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

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

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

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

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

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

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