Documentation

Mathlib.RingTheory.OrzechProperty

Orzech property of rings #

In this file we define the following property of rings:

It's proved in the above papers that

References #

Tags #

free module, rank, Orzech property, (strong) rank condition, invariant basis number, IBN

theorem orzechProperty_iff (R : Type u) [Semiring R] :
OrzechProperty R ∀ {M : Type u} [inst : AddCommMonoid M] [inst_1 : Module R M] [inst_2 : Module.Finite R M] {N : Submodule R M} (f : N →ₗ[R] M), Function.Surjective fFunction.Injective f
class OrzechProperty (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.

Instances
    theorem OrzechProperty.injective_of_surjective_of_submodule' {R : Type u} :
    ∀ {inst : Semiring R} [self : OrzechProperty R] {M : Type u} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : Module.Finite R M] {N : Submodule R M} (f : N →ₗ[R] M), Function.Surjective fFunction.Injective f