Mathlib.RingTheory.Noetherian.Orzech

Module docstring

{"# 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. "}

IsNoetherian.injective_of_surjective_of_injective theorem

(i f : N →ₗ[R] M) (hi : Injective i) (hf : Surjective f) : Injective f

Full source

/-- **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]. -/
theorem IsNoetherian.injective_of_surjective_of_injective (i f : N →ₗ[R] M)
    (hi : Injective i) (hf : Surjective f) : Injective f := by
  haveI := isNoetherian_of_injective i hi
  obtain ⟨n, H⟩ := monotone_stabilizes_iff_noetherian.2 ‹_›
    ⟨_, monotone_nat_of_le_succ <| f.iterateMapComap_le_succ i ⊥ (by simp)⟩
  exact LinearMap.ker_eq_bot.1 <| bot_unique <|
    f.ker_le_of_iterateMapComap_eq_succ i ⊥ n (H _ (Nat.le_succ _)) hf hi

Orzech's Theorem for Noetherian Modules: Surjective and Injective Linear Maps

Informal description

Let $R$ be a ring (not necessarily commutative), and let $M$ and $N$ be $R$-modules. Suppose that $M$ is Noetherian, and let $i \colon N \to M$ and $f \colon N \to M$ be $R$-linear maps. If $i$ is injective and $f$ is surjective, then $f$ is also injective.

IsNoetherian.injective_of_surjective_of_submodule theorem

{N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f

Full source

/-- **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. -/
theorem IsNoetherian.injective_of_surjective_of_submodule
    {N : Submodule R M} (f : N →ₗ[R] M) (hf : Surjective f) : Injective f :=
  IsNoetherian.injective_of_surjective_of_injective N.subtype f N.injective_subtype hf

Orzech's Theorem for Submodules of Noetherian Modules: Surjective Implies Injective

Informal description

Let $R$ be a ring (not necessarily commutative), $M$ a Noetherian $R$-module, and $N$ a submodule of $M$. If $f \colon N \to M$ is a surjective $R$-linear map, then $f$ is also injective.

IsNoetherian.injective_of_surjective_endomorphism theorem

(f : M →ₗ[R] M) (s : Surjective f) : Injective f

Full source

/-- Any surjective endomorphism of a Noetherian module is injective. -/
theorem IsNoetherian.injective_of_surjective_endomorphism (f : M →ₗ[R] M)
    (s : Surjective f) : Injective f :=
  IsNoetherian.injective_of_surjective_of_injective _ f (LinearEquiv.refl _ _).injective s

Noetherian Module Endomorphism Theorem: Surjective Implies Injective

Informal description

Let $R$ be a ring and $M$ be a Noetherian $R$-module. For any $R$-linear endomorphism $f \colon M \to M$, if $f$ is surjective, then it is also injective.

IsNoetherian.bijective_of_surjective_endomorphism theorem

(f : M →ₗ[R] M) (s : Surjective f) : Bijective f

Full source

/-- Any surjective endomorphism of a Noetherian module is bijective. -/
theorem IsNoetherian.bijective_of_surjective_endomorphism (f : M →ₗ[R] M)
    (s : Surjective f) : Bijective f :=
  ⟨IsNoetherian.injective_of_surjective_endomorphism f s, s⟩

Bijectivity of Surjective Endomorphisms on Noetherian Modules

Informal description

Let $R$ be a ring and $M$ a Noetherian $R$-module. For any $R$-linear endomorphism $f \colon M \to M$, if $f$ is surjective, then it is bijective.

IsNoetherian.subsingleton_of_prod_injective theorem

(f : M × N →ₗ[R] M) (i : Injective f) : Subsingleton N

Full source

/-- If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial. -/
theorem IsNoetherian.subsingleton_of_prod_injective (f : M × NM × N →ₗ[R] M)
    (i : Injective f) : Subsingleton N := .intro fun x y ↦ by
  have h := IsNoetherian.injective_of_surjective_of_injective f _ i LinearMap.fst_surjective
  simpa using h (show LinearMap.fst R M N (0, x) = LinearMap.fst R M N (0, y) from rfl)

Triviality of $N$ under injective linear map from $M \times N$ to Noetherian $M$

Informal description

Let $R$ be a ring, $M$ a Noetherian $R$-module, and $N$ an $R$-module. If there exists an injective $R$-linear map $f \colon M \times N \to M$, then $N$ is trivial (i.e., has at most one element).

IsNoetherian.equivPUnitOfProdInjective definition

(f : M × N →ₗ[R] M) (i : Injective f) : N ≃ₗ[R] PUnit.{w + 1}

Full source

/-- If `M ⊕ N` embeds into `M`, for `M` noetherian over `R`, then `N` is trivial. -/
@[simps!]
def IsNoetherian.equivPUnitOfProdInjective (f : M × NM × N →ₗ[R] M)
    (i : Injective f) : N ≃ₗ[R] PUnit.{w + 1} :=
  haveI := IsNoetherian.subsingleton_of_prod_injective f i
  .ofSubsingleton _ _

Isomorphism to trivial module under injective linear map from product to Noetherian module

Informal description

Given a Noetherian $R$-module $M$ and an $R$-module $N$, if there exists an injective $R$-linear map $f \colon M \times N \to M$, then $N$ is isomorphic to the trivial module $\text{PUnit}$ (a module with exactly one element).

IsNoetherianRing.orzechProperty instance

(R) [Ring R] [IsNoetherianRing R] : OrzechProperty R

Full source

/-- Any Noetherian ring satisfies Orzech property.
See also `IsNoetherian.injective_of_surjective_of_submodule` and
`IsNoetherian.injective_of_surjective_of_injective`. -/
instance (priority := 100) IsNoetherianRing.orzechProperty
    (R) [Ring R] [IsNoetherianRing R] : OrzechProperty R where
  injective_of_surjective_of_submodule' {M} :=
    letI := Module.addCommMonoidToAddCommGroup R (M := M)
    IsNoetherian.injective_of_surjective_of_submodule

Noetherian Rings Satisfy the Orzech Property

Informal description

Every Noetherian ring satisfies the Orzech property, meaning that for any finitely generated module $M$ over such a ring, any surjective linear map from a submodule $N$ of $M$ to $M$ is also injective.