funlean.
Step 55 / 64

Master’s level

Rings that cannot grow forever

Every ascending chain of ideals stabilizes: no endless tower inside the ring.

Start with a concrete example

The multiples of 16 are among the multiples of 8, then 4, then 2. These collections grow. The Noetherian condition says an increasing chain of ideals eventually stops growing; the special word “ideal” also imposes arithmetic closure rules.

A small check: try the idea

Think with the concrete example above. You can try again.

Which inclusion is correct for integer multiples?

Read the answer and reasoning

Multiples of 16 are among multiples of 8. 16k=8×(2k). But 8 is itself a multiple of 8 and not of 16. Watch the direction in the growing chain.

Build the idea in three steps

  1. An ideal of a ring is a bundle of multiples: closed under the ring addition, and swallowing products with anything — the multiples of 8 in ℤ, say. A ring is Noetherian when no endless strictly growing tower of ideals exists: every ascending chain stops.
  2. IsNoetherianRing R is deliberately an abbreviation: IsNoetherian R R — the ring, viewed as a module over itself, is Noetherian. The second displayed theorem translates the phrase into everyday currency: every ideal is finitely generated.
  3. The top of the proof insists on it: the summit excerpts carry [IsNoetherianRing A] next to [CommRing A] and [IsLocalRing A]. Finite data controls everything inside A — without that harness, the two workshops could sprawl without limit.

A small example

The tower (16) ⊂ (8) ⊂ (4) ⊂ (2) in ℤ — 16 sits inside the multiples of 8 because 8 divides 16 — must stop, and it does: every ideal of ℤ is generated by a single number, so every ascending chain ends after finitely many steps.

Lean definition · original excerpt

Mathlib · db584cd · Defs.lean

/-- A (semi)ring is Noetherian if it is Noetherian as a module over itself,i.e. all its ideals are finitely generated. -/@[wikidata Q582271]abbrev IsNoetherianRing (R) [Semiring R] :=  IsNoetherian R R theorem isNoetherianRing_iff {R} [Semiring R] : IsNoetherianRing R ↔ IsNoetherian R R :=  Iff.rfl /-- A ring is Noetherian if and only if all its ideals are finitely-generated. -/theorem isNoetherianRing_iff_ideal_fg (R : Type*) [Semiring R] :    IsNoetherianRing R ↔ ∀ I : Ideal R, I.FG :=

How to read this Lean

The abbreviation design is typical Mathlib craft: name the readable concept, realize it through the module-side predicate, then prove the equivalence with the generator-counting phrase people carry in their heads (isNoetherianRing_iff_ideal_fg). Chain stabilization and basis theorems fill the remainder of this file. In the endgame hypothesis rows the word appears by abbreviation — compact to state, heavy to earn.

Original source ↗ · L193–204Open the complete saved source

Where this idea is used

12. The workshops agree13. Pip’s impossible quilt
I’m lost · Help

Mika’s help desk

Rings that cannot grow forever

One thing at a time

Read the three explanation steps first. The Lean source is there for a closer look afterwards; you do not have to read it first.

In simpler words

Every ascending chain of ideals stabilizes: no endless tower inside the ring.

Earlier ideas are listed under “Start with these ideas” on this page.

A small clue

The tower (16) ⊂ (8) ⊂ (4) ⊂ (2) in ℤ — 16 sits inside the multiples of 8 because 8 divides 16 — must stop, and it does: every ideal of ℤ is generated by a single number, so every ascending chain ends after finitely many steps.

Close this panel to return to the exact place you were reading. These are prepared hints for this page.

Start with the first small story →