Documentation

Mathlib.RingTheory.Noetherian.Orzech

Noetherian rings have the Orzech property #

Main results #

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

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

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
Instances For
    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) :
    (IsNoetherian.equivPUnitOfProdInjective f i) x✝ = 0
    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} ) :
    (IsNoetherian.equivPUnitOfProdInjective f i).symm x✝ = 0
    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.

    Equations
    • ⋯ = ⋯