# Noetherian rings have the Orzech property #

## Main results #

- `IsNoetherian.injective_of_surjective_of_injective`: if `M` and `N` are `R`-modules for a ring `R` (not necessarily commutative), `M` is Noetherian, `i : N →ₗ[R] M` is injective, `f : N →ₗ[R] M` is surjective, then `f` is also injective.
- `IsNoetherianRing.orzechProperty`: Any Noetherian ring satisfies the Orzech property.

source
theorem IsNoetherian.injective_of_surjective_of_injective {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (i f : N →ₗ[R] M) (hi : Function.Injective ⇑i) (hf : Function.Surjective ⇑f) :
Function.Injective ⇑f

Orzech's theorem for Noetherian modules: if `R` is a ring (not necessarily commutative), `M` and `N` are `R`-modules, `M` is Noetherian, `i : N →ₗ[R] M` is injective, `f : N →ₗ[R] M` is surjective, then `f` is also injective. The proof here is adapted from Djoković's paper Epimorphisms of modules which must be isomorphisms [djokovic1973], utilizing `LinearMap.iterateMapComap`. See also Orzech's original paper: Onto endomorphisms are isomorphisms [orzech1971].

source
theorem IsNoetherian.injective_of_surjective_of_submodule {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {N : Submodule R M} (f : ↥N →ₗ[R] M) (hf : Function.Surjective ⇑f) :
Function.Injective ⇑f

Orzech's theorem for Noetherian modules: if `R` is a ring (not necessarily commutative), `M` is a Noetherian `R`-module, `N` is a submodule, `f : N →ₗ[R] M` is surjective, then `f` is also injective.

source
theorem IsNoetherian.injective_of_surjective_endomorphism {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) (s : Function.Surjective ⇑f) :
Function.Injective ⇑f

Any surjective endomorphism of a Noetherian module is injective.

source
theorem IsNoetherian.bijective_of_surjective_endomorphism {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) (s : Function.Surjective ⇑f) :
Function.Bijective ⇑f

Any surjective endomorphism of a Noetherian module is bijective.

source
theorem IsNoetherian.subsingleton_of_prod_injective {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) :
Subsingleton N

If `M ⊕ N` embeds into `M`, for `M` Noetherian over `R`, then `N` is trivial.

source
def IsNoetherian.equivPUnitOfProdInjective {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) :
N ≃ₗ[R] PUnit.{w + 1}

If `M ⊕ N` embeds into `M`, for `M` Noetherian over `R`, then `N` is trivial.

Equations

- IsNoetherian.equivPUnitOfProdInjective f i = LinearEquiv.ofSubsingleton N PUnit.{?u.52 + 1}

Instances For

source
@[simp]
theorem IsNoetherian.equivPUnitOfProdInjective_symm_apply {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) (x✝ : PUnit.{w + 1}) :
(equivPUnitOfProdInjective f i).symm x✝ = 0
source
@[simp]
theorem IsNoetherian.equivPUnitOfProdInjective_apply {R : Type u_1} {M : Type u_2} {N : Type w} [Ring R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] [IsNoetherian R M] (f : M × N →ₗ[R] M) (i : Function.Injective ⇑f) (x✝ : N) :
(equivPUnitOfProdInjective f i) x✝ = PUnit.unit
source
@[instance 100]
instance IsNoetherianRing.orzechProperty (R : Type u_1) [Ring R] [IsNoetherianRing R] :
OrzechProperty R

Any Noetherian ring satisfies Orzech property. See also `IsNoetherian.injective_of_surjective_of_submodule` and `IsNoetherian.injective_of_surjective_of_injective`.