Mathlib.RingTheory.Noetherian.Defs

Module docstring

{"# Noetherian rings and modules

The following are equivalent for a module M over a ring R: 1. Every increasing chain of submodules M₁ ⊆ M₂ ⊆ M₃ ⊆ ⋯ eventually stabilises. 2. Every submodule is finitely generated.

A module satisfying these equivalent conditions is said to be a Noetherian R-module. A ring is a Noetherian ring if it is Noetherian as a module over itself.

(Note that we do not assume yet that our rings are commutative, so perhaps this should be called \"left Noetherian\". To avoid cumbersome names once we specialize to the commutative case, we don't make this explicit in the declaration names.)

Main definitions

Let R be a ring and let M and P be R-modules. Let N be an R-submodule of M.

IsNoetherian R M is the proposition that M is a Noetherian R-module. It is a class, implemented as the predicate that all R-submodules of M are finitely generated.

Main statements

isNoetherian_iff is the theorem that an R-module M is Noetherian iff > is well-founded on Submodule R M.

Note that the Hilbert basis theorem, that if a commutative ring R is Noetherian then so is R[X], is proved in RingTheory.Polynomial.

References

[M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra][atiyah-macdonald]
[P. Samuel, Algebraic Theory of Numbers][samuel1967]

Tags

Noetherian, noetherian, Noetherian ring, Noetherian module, noetherian ring, noetherian module

IsNoetherian structure

(R M) [Semiring R] [AddCommMonoid M] [Module R M]

Full source

/-- `IsNoetherian R M` is the proposition that `M` is a Noetherian `R`-module,
implemented as the predicate that all `R`-submodules of `M` are finitely generated.
-/
-- Porting note: should this be renamed to `Noetherian`?
class IsNoetherian (R M) [Semiring R] [AddCommMonoid M] [Module R M] : Prop where
  noetherian : ∀ s : Submodule R M, s.FG

Noetherian Module

Informal description

The structure `IsNoetherian R M` represents the property that an `R`-module `M` is Noetherian, meaning every submodule of `M` is finitely generated.

isNoetherian_def theorem

: IsNoetherian R M ↔ ∀ s : Submodule R M, s.FG

Full source

/-- An R-module is Noetherian iff all its submodules are finitely-generated. -/
theorem isNoetherian_def : IsNoetherianIsNoetherian R M ↔ ∀ s : Submodule R M, s.FG :=
  ⟨fun h => h.noetherian, IsNoetherian.mk⟩

Characterization of Noetherian Modules via Finitely Generated Submodules

Informal description

An $R$-module $M$ is Noetherian if and only if every submodule of $M$ is finitely generated.

isNoetherian_submodule theorem

{N : Submodule R M} : IsNoetherian R N ↔ ∀ s : Submodule R M, s ≤ N → s.FG

Full source

theorem isNoetherian_submodule {N : Submodule R M} :
    IsNoetherianIsNoetherian R N ↔ ∀ s : Submodule R M, s ≤ N → s.FG := by
  refine ⟨fun ⟨hn⟩ => fun s hs =>
    have : s ≤ LinearMap.range N.subtype := N.range_subtype.symm ▸ hs
    Submodule.map_comap_eq_self this ▸ (hn _).map _,
    fun h => ⟨fun s => ?_⟩⟩
  have f := (Submodule.equivMapOfInjective N.subtype Subtype.val_injective s).symm
  have h₁ := h (s.map N.subtype) (Submodule.map_subtype_le N s)
  have h₂ : (⊤ : Submodule R (s.map N.subtype)).map f = ⊤ := by simp
  have h₃ := ((Submodule.fg_top _).2 h₁).map (↑f : _ →ₗ[R] s)
  exact (Submodule.fg_top _).1 (h₂ ▸ h₃)

Noetherian Submodule Characterization via Finitely Generated Submodules

Informal description

Let $M$ be a module over a ring $R$ and $N$ be a submodule of $M$. Then $N$ is Noetherian as an $R$-module if and only if every submodule $s$ of $M$ contained in $N$ is finitely generated.

isNoetherian_submodule_left theorem

{N : Submodule R M} : IsNoetherian R N ↔ ∀ s : Submodule R M, (N ⊓ s).FG

Full source

theorem isNoetherian_submodule_left {N : Submodule R M} :
    IsNoetherianIsNoetherian R N ↔ ∀ s : Submodule R M, (N ⊓ s).FG :=
  isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_left, fun H _ hs => inf_of_le_right hs ▸ H _⟩

Noetherian Submodule Criterion via Intersection with Finitely Generated Submodules

Informal description

Let $M$ be a module over a ring $R$ and $N$ be a submodule of $M$. Then $N$ is a Noetherian $R$-module if and only if for every submodule $s$ of $M$, the intersection $N \cap s$ is finitely generated.

isNoetherian_submodule_right theorem

{N : Submodule R M} : IsNoetherian R N ↔ ∀ s : Submodule R M, (s ⊓ N).FG

Full source

theorem isNoetherian_submodule_right {N : Submodule R M} :
    IsNoetherianIsNoetherian R N ↔ ∀ s : Submodule R M, (s ⊓ N).FG :=
  isNoetherian_submodule.trans ⟨fun H _ => H _ inf_le_right, fun H _ hs => inf_of_le_left hs ▸ H _⟩

Noetherian Submodule Criterion via Intersection with Finitely Generated Submodules

Informal description

Let $M$ be a module over a ring $R$ and $N$ be a submodule of $M$. Then $N$ is Noetherian as an $R$-module if and only if for every submodule $s$ of $M$, the intersection $s \sqcap N$ is finitely generated.

isNoetherian_submodule' instance

[IsNoetherian R M] (N : Submodule R M) : IsNoetherian R N

Full source

instance isNoetherian_submodule' [IsNoetherian R M] (N : Submodule R M) : IsNoetherian R N :=
  isNoetherian_submodule.2 fun _ _ => IsNoetherian.noetherian _

Submodules of Noetherian Modules are Noetherian

Informal description

For any Noetherian $R$-module $M$, every submodule $N$ of $M$ is also a Noetherian $R$-module.

isNoetherian_of_le theorem

{s t : Submodule R M} [ht : IsNoetherian R t] (h : s ≤ t) : IsNoetherian R s

Full source

theorem isNoetherian_of_le {s t : Submodule R M} [ht : IsNoetherian R t] (h : s ≤ t) :
    IsNoetherian R s :=
  isNoetherian_submodule.mpr fun _ hs' => isNoetherian_submodule.mp ht _ (le_trans hs' h)

Noetherian Property is Inherited by Submodules

Informal description

Let $M$ be a module over a ring $R$, and let $s$ and $t$ be submodules of $M$ such that $s \subseteq t$. If $t$ is a Noetherian $R$-module, then $s$ is also a Noetherian $R$-module.

isNoetherian_iff' theorem

: IsNoetherian R M ↔ WellFoundedGT (Submodule R M)

Full source

theorem isNoetherian_iff' : IsNoetherianIsNoetherian R M ↔ WellFoundedGT (Submodule R M) := by
  have := (CompleteLattice.wellFoundedGT_characterisations <| Submodule R M).out 0 3
  -- Porting note: inlining this makes rw complain about it being a metavariable
  rw [this]
  exact
    ⟨fun ⟨h⟩ => fun k => (fg_iff_compact k).mp (h k), fun h =>
      ⟨fun k => (fg_iff_compact k).mpr (h k)⟩⟩

Noetherian Module Characterization via Well-foundedness of Submodule Order

Informal description

An $R$-module $M$ is Noetherian if and only if the "greater than" relation $>$ is well-founded on the lattice of submodules of $M$.

isNoetherian_iff theorem

: IsNoetherian R M ↔ WellFounded ((· > ·) : Submodule R M → Submodule R M → Prop)

Full source

theorem isNoetherian_iff :
    IsNoetherianIsNoetherian R M ↔ WellFounded ((· > ·) : Submodule R M → Submodule R M → Prop) := by
  rw [isNoetherian_iff', ← isWellFounded_iff]

Noetherian Module Characterization via Well-foundedness of Submodule Order

Informal description

An $R$-module $M$ is Noetherian if and only if the strict greater-than relation $>$ on the lattice of submodules of $M$ is well-founded. That is, every strictly decreasing chain of submodules eventually stabilizes.

wellFoundedGT instance

[h : IsNoetherian R M] : WellFoundedGT (Submodule R M)

Full source

instance wellFoundedGT [h : IsNoetherian R M] : WellFoundedGT (Submodule R M) :=
  h.wellFoundedGT

Well-foundedness of Submodule Order in Noetherian Modules

Informal description

For any Noetherian $R$-module $M$, the "greater than" relation on the lattice of submodules of $M$ is well-founded.

isNoetherian_iff_fg_wellFounded theorem

: IsNoetherian R M ↔ WellFoundedGT { N : Submodule R M // N.FG }

Full source

theorem isNoetherian_iff_fg_wellFounded :
    IsNoetherianIsNoetherian R M ↔ WellFoundedGT { N : Submodule R M // N.FG } := by
  let α := { N : Submodule R M // N.FG }
  constructor
  · intro H
    let f : α ↪o Submodule R M := OrderEmbedding.subtype _
    exact OrderEmbedding.wellFoundedLT f.dual
  · intro H
    constructor
    intro N
    obtain ⟨⟨N₀, h₁⟩, e : N₀ ≤ N, h₂⟩ :=
      WellFounded.has_min H.wf { N' : α | N'.1 ≤ N } ⟨⟨⊥, Submodule.fg_bot⟩, @bot_le _ _ _ N⟩
    convert h₁
    refine (e.antisymm ?_).symm
    by_contra h₃
    obtain ⟨x, hx₁ : x ∈ N, hx₂ : x ∉ N₀⟩ := Set.not_subset.mp h₃
    apply hx₂
    rw [eq_of_le_of_not_lt (le_sup_right : N₀ ≤ _) (h₂
      ⟨_, Submodule.FG.sup ⟨{x}, by rw [Finset.coe_singleton]⟩ h₁⟩ <|
      sup_le ((Submodule.span_singleton_le_iff_mem _ _).mpr hx₁) e)]
    exact (le_sup_left : (R ∙ x) ≤ _) (Submodule.mem_span_singleton_self _)

Noetherian Module Characterization via Well-foundedness on Finitely Generated Submodules

Informal description

An $R$-module $M$ is Noetherian if and only if the "greater than" relation $>$ is well-founded on the set of finitely generated submodules of $M$.

set_has_maximal_iff_noetherian theorem

: (∀ a : Set <| Submodule R M, a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M

Full source

/-- A module is Noetherian iff every nonempty set of submodules has a maximal submodule among them.
-/
theorem set_has_maximal_iff_noetherian :
    (∀ a : Set <| Submodule R M, a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬M' < I) ↔ IsNoetherian R M := by
  rw [isNoetherian_iff, WellFounded.wellFounded_iff_has_min]

Noetherian Module Characterization via Maximal Submodules in Nonempty Sets

Informal description

An $R$-module $M$ is Noetherian if and only if every nonempty set of submodules of $M$ contains a maximal element with respect to the strict inclusion relation $<$. That is, for any nonempty set $\mathcal{A}$ of submodules of $M$, there exists a submodule $M' \in \mathcal{A}$ such that no submodule $I \in \mathcal{A}$ strictly contains $M'$.

monotone_stabilizes_iff_noetherian theorem

: (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M

Full source

/-- A module is Noetherian iff every increasing chain of submodules stabilizes. -/
theorem monotone_stabilizes_iff_noetherian :
    (∀ f : ℕ →o Submodule R M, ∃ n, ∀ m, n ≤ m → f n = f m) ↔ IsNoetherian R M := by
  rw [isNoetherian_iff', wellFoundedGT_iff_monotone_chain_condition]

Noetherian Module Characterization via Stabilizing Chains of Submodules

Informal description

An $R$-module $M$ is Noetherian if and only if every increasing chain of submodules $f \colon \mathbb{N} \to \text{Submodule}(R, M)$ stabilizes, meaning there exists an index $n$ such that for all $m \geq n$, we have $f(n) = f(m)$.

Module.End.eventually_disjoint_ker_pow_range_pow theorem

(f : End R M) : ∀ᶠ n in atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n))

Full source

/-- For an endomorphism of a Noetherian module, any sufficiently large iterate has disjoint kernel
and range. -/
theorem Module.End.eventually_disjoint_ker_pow_range_pow (f : End R M) :
    ∀ᶠ n in atTop, Disjoint (LinearMap.ker (f ^ n)) (LinearMap.range (f ^ n)) := by
  obtain ⟨n, hn : ∀ m, n ≤ m → LinearMap.ker (f ^ n) = LinearMap.ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
  refine eventually_atTop.mpr ⟨n, fun m hm ↦ disjoint_iff.mpr ?_⟩
  rw [← hn _ hm, Submodule.eq_bot_iff]
  rintro - ⟨hx, ⟨x, rfl⟩⟩
  apply pow_map_zero_of_le hm
  replace hx : x ∈ LinearMap.ker (f ^ (n + m)) := by
    simpa [f.pow_apply n, f.pow_apply m, ← f.pow_apply (n + m), ← iterate_add_apply] using hx
  rwa [← hn _ (n.le_add_right m)] at hx

Disjointness of Kernel and Range for Iterates of an Endomorphism on a Noetherian Module

Informal description

For any endomorphism $f$ of a Noetherian $R$-module $M$, there exists a natural number $N$ such that for all $n \geq N$, the kernel and range of the $n$-th iterate $f^n$ are disjoint, i.e., $\ker(f^n) \cap \mathrm{range}(f^n) = \{0\}$.

LinearMap.eventually_iSup_ker_pow_eq theorem

(f : M →ₗ[R] M) : ∀ᶠ n in atTop, ⨆ m, LinearMap.ker (f ^ m) = LinearMap.ker (f ^ n)

Full source

lemma LinearMap.eventually_iSup_ker_pow_eq (f : M →ₗ[R] M) :
    ∀ᶠ n in atTop, ⨆ m, LinearMap.ker (f ^ m) = LinearMap.ker (f ^ n) := by
  obtain ⟨n, hn : ∀ m, n ≤ m → ker (f ^ n) = ker (f ^ m)⟩ :=
    monotone_stabilizes_iff_noetherian.mpr inferInstance f.iterateKer
  refine eventually_atTop.mpr ⟨n, fun m hm ↦ ?_⟩
  refine le_antisymm (iSup_le fun l ↦ ?_) (le_iSup (fun i ↦ LinearMap.ker (f ^ i)) m)
  rcases le_or_lt m l with h | h
  · rw [← hn _ (hm.trans h), hn _ hm]
  · exact f.iterateKer.monotone h.le

Stabilization of Kernel Supremum for Powers of a Linear Endomorphism on a Noetherian Module

Informal description

For any linear endomorphism $f \colon M \to M$ of a Noetherian $R$-module $M$, there exists a natural number $N$ such that for all $n \geq N$, the supremum of the kernels of the powers $f^m$ for $m \in \mathbb{N}$ equals the kernel of $f^n$, i.e., \[ \bigsqcup_{m \in \mathbb{N}} \ker(f^m) = \ker(f^n). \]

IsNoetherianRing abbrev

(R) [Semiring R]

Full source

/-- A (semi)ring is Noetherian if it is Noetherian as a module over itself,
i.e. all its ideals are finitely generated. -/
abbrev IsNoetherianRing (R) [Semiring R] :=
  IsNoetherian R R

Noetherian Ring

Informal description

A (semi)ring $R$ is Noetherian if it is Noetherian as a module over itself, meaning all its ideals are finitely generated.

isNoetherianRing_iff theorem

{R} [Semiring R] : IsNoetherianRing R ↔ IsNoetherian R R

Full source

theorem isNoetherianRing_iff {R} [Semiring R] : IsNoetherianRingIsNoetherianRing R ↔ IsNoetherian R R :=
  Iff.rfl

Equivalence of Noetherian Ring and Noetherian Module over Itself

Informal description

A semiring $R$ is a Noetherian ring if and only if it is Noetherian as a module over itself.

isNoetherianRing_iff_ideal_fg theorem

(R : Type*) [Semiring R] : IsNoetherianRing R ↔ ∀ I : Ideal R, I.FG

Full source

/-- A ring is Noetherian if and only if all its ideals are finitely-generated. -/
theorem isNoetherianRing_iff_ideal_fg (R : Type*) [Semiring R] :
    IsNoetherianRingIsNoetherianRing R ↔ ∀ I : Ideal R, I.FG :=
  isNoetherianRing_iff.trans isNoetherian_def

Characterization of Noetherian Rings via Finitely Generated Ideals

Informal description

A semiring $R$ is Noetherian if and only if every ideal $I$ of $R$ is finitely generated.