Documentation

Mathlib.RingTheory.Noetherian.Orzech

Noetherian rings have the Orzech property #

Main results #

theorem LinearMap.eventually_disjoint_ker_pow_range_pow {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) :
∀ᶠ (n : ) in Filter.atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

For an endomorphism of a Noetherian module, any sufficiently large iterate has disjoint kernel and range.

theorem LinearMap.eventually_iSup_ker_pow_eq {R : Type u_1} {M : Type u_2} [Ring R] [AddCommGroup M] [Module R M] [IsNoetherian R M] (f : M →ₗ[R] M) :
∀ᶠ (n : ) in Filter.atTop, ⨆ (m : ), LinearMap.ker (f ^ m) = LinearMap.ker (f ^ n)
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) :

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 [Djo73], utilizing LinearMap.iterateMapComap. See also Orzech's original paper: Onto endomorphisms are isomorphisms [Orz71].

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) :

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.

Any surjective endomorphism of a Noetherian module is injective.

Any surjective endomorphism of a Noetherian module is bijective.

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) :

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

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) :

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

Equations
Instances For
    @[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) :
    @[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}) :