Chapter 7. Noetherian Rings (pp. 80–83)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 1 definition, 2 theorems, 7 propositions, 2 lemmas, 6 corollaries and 1 example.
Of the 19 statements checked against Lean, 19 are formalized somewhere and 0 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 19 | 100% | Mathlib states and proves it. |
| checked in total | 19 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first.LeanCategories/Algebra/AtiyahMacdonald/PrimaryDecomposition.leansupplies project notation for primary decompositions and their prime sets, but the existence and Noetherian theorems in this chapter are owned by pinned Mathlib. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, contains all 19 routes below. The boundary declarations, number-ring instances, Lasker–Noether interfaces, and associated-prime interfaces were compile-checked in the repository environment. - Current Mathlib: upstream
5aedf732b6987e8c26ab3c9ebc855314f82b045f(Apache-2.0), denotedH, was rechecked 2026-09-06 and introduces no contrary ownership boundary for these rows. No external route is needed in C07. - Source normalization: the printed irreducible-ideal definition omits a properness clause, although §7.1 scopes the primary-decomposition discussion to ideals
≠ (1)and Lemma 7.12 would be false for(1)otherwise. U012/U014 therefore use MathlibInfIrred, which makes the source’s necessary implicit properness explicit.
Proposition: Proposition 7.1
A surjective homomorphic image of a Noetherian ring is Noetherian.
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_quotient — A quotient of a Noetherian self-module is Noetherian, so a surjective ring image A/I is Noetherian exactly as in Proposition 7.1.
Proposition: Proposition 7.2
If A⊆B, A is Noetherian, and B is finitely generated as an A-module, then B is Noetherian as a ring.
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::IsNoetherianRing.of_finite — A module-finite algebra over a Noetherian ring is Noetherian as a ring, exactly Proposition 7.2.
Example: Gaussian integers and rings of integers
Z[i] is Noetherian; more generally, the ring of integers in any algebraic number field is Noetherian.
Formalized. Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean Noetherian instance for GaussianInt; Mathlib/NumberTheory/NumberField/Basic.lean::NumberField.extension_isNoetherian and ring-of-integers instances — The project environment synthesizes IsNoetherianRing GaussianInt and IsNoetherianRing (𝓞 K) for every number field K, realizing both source examples.
Proposition: Proposition 7.3
If A is Noetherian and S⊆A is multiplicatively closed, then S⁻¹A is Noetherian.
Formalized. Mathlib/RingTheory/Localization/Submodule.lean::IsLocalization.isNoetherianRing — Every localization of a Noetherian ring is Noetherian, exactly Proposition 7.3.
Corollary: Corollary 7.4
If A is Noetherian and p is prime, then the local ring A_p is Noetherian.
Formalized. IsLocalization.isNoetherianRing; Mathlib/RingTheory/Localization/AtPrime/Basic.lean::Localization.AtPrime — Specializing the localization theorem to the prime complement gives Noetherianity of A_𝔭.
Theorem: Theorem 7.5 (Hilbert basis theorem)
If A is Noetherian, then A[x] is Noetherian. Source remark: the same Noetherianity implication holds for the formal power-series ring Ax; this is proved later as 10.27.
Formalized. Mathlib/RingTheory/Polynomial/Basic.lean::Polynomial.isNoetherianRing; Mathlib/RingTheory/MvPowerSeries/Equiv.lean::MvPowerSeries.isNoetherianRing — The polynomial theorem is Hilbert basis. The finite-variable power-series instance includes the one-variable formal-power-series remark that the source defers to 10.27.
Corollary: Corollary 7.6
If A is Noetherian, then A[x₁,…,xₙ] is Noetherian.
Formalized. finite-variable MvPolynomial Noetherian instance in Mathlib/RingTheory/Polynomial/Basic.lean — Finite-variable multivariate polynomial rings over a Noetherian base are Noetherian, exactly Corollary 7.6.
Corollary: Corollary 7.7
Every finitely generated A-algebra B is Noetherian when A is Noetherian; in particular every finitely generated ring and every finitely generated algebra over a field is Noetherian.
Formalized. Mathlib/RingTheory/FiniteType.lean::Algebra.FiniteType.isNoetherianRing; isNoetherianRing_of_surjective — A finite-type algebra is a quotient of a finite polynomial algebra, hence Noetherian over a Noetherian base; the special cases over ℤ and fields follow directly.
Proposition: Proposition 7.8
For A⊆B⊆C with A Noetherian and C finitely generated as an A-algebra, if either (i) C is finitely generated as a B-module or (ii) C is integral over B, then B is finitely generated as an A-algebra.
Formalized. Mathlib/RingTheory/Adjoin/Tower.lean::fg_of_fg_of_fg; Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.finite — fg_of_fg_of_fg is explicitly documented as Atiyah–Macdonald Proposition 7.8 and handles the module-finite branch. In the integral branch, finite type plus integrality makes C module-finite over B, reducing to the same theorem.
Proposition: Proposition 7.9
If k is a field and E is a finitely generated k-algebra which is itself a field, then E is a finite algebraic extension of k.
Formalized. Mathlib/RingTheory/Jacobson/Ring.lean::finite_of_finite_type_of_isJacobsonRing; Mathlib/RingTheory/Algebraic/Integral.lean::Algebra.IsAlgebraic.of_finite — A field of finite type over the Jacobson field k is module-finite, hence algebraic, exactly Proposition 7.9.
Corollary: Corollary 7.10 (weak Hilbert Nullstellensatz)
If k is a field, A a finitely generated k-algebra, and m maximal in A, then A/m is finite algebraic over k; if k is algebraically closed, A/m≅k. The source identifies this as the weak Hilbert Nullstellensatz (the theorem of the zeros), with the proof attributed to Artin and Tate.
Formalized. finite_of_finite_type_of_isJacobsonRing; Algebra.IsAlgebraic.of_finite; Mathlib/FieldTheory/IsAlgClosed/Basic.lean::IntermediateField.eq_bot_of_isAlgClosed_of_isAlgebraic — Applied to the field A/𝔪, the first two declarations give a finite algebraic extension of k; when k is algebraically closed, every algebraic intermediate field is the base, yielding A/𝔪 ≃ₐ[k] k.
Definition: Irreducible ideal
An ideal a is irreducible when a=b∩c implies a=b or a=c.
Formalized. Mathlib/Order/Irreducible.lean::InfIrred — The printed definition gives the binary-intersection irreducibility condition but omits properness. Section 7.1 scopes primary decomposition to ideals ≠ (1), and Lemma 7.12 would otherwise fail for (1); InfIrred is exactly the coherent proper-ideal version, adding ¬ IsMax to the displayed condition.
Lemma: Lemma 7.11
Every ideal in a Noetherian ring is a finite intersection of irreducible ideals.
Formalized. Mathlib/Order/Irreducible.lean::exists_infIrred_decomposition — In the Noetherian ideal lattice (WellFoundedGT), every ideal is a finite infimum of InfIrred ideals, exactly Lemma 7.11, with the empty infimum covering the top ideal.
Lemma: Lemma 7.12
Every irreducible ideal in a Noetherian ring is primary.
Formalized. Mathlib/RingTheory/Lasker.lean::InfIrred.isPrimary — In a Noetherian module/ring, every inf-irreducible proper submodule/ideal is primary, exactly Lemma 7.12 with the source’s implicit properness normalized.
Theorem: Theorem 7.13
Every ideal in a Noetherian ring has a primary decomposition.
Formalized. Mathlib/RingTheory/Lasker.lean::Submodule.isLasker; IsLasker.exists_isMinimalPrimaryDecomposition — Mathlib explicitly names this the Lasker–Noether theorem: every submodule of a Noetherian module admits a finite primary decomposition. For ideals, this is Theorem 7.13; the project Ideal.IsPrimaryDecomposition wrapper is compatible notation but does not own the existence theorem.
Proposition: Proposition 7.14
In a Noetherian ring, every ideal a contains some power of its radical r(a).
Formalized. Mathlib/RingTheory/Finiteness/Ideal.lean::Ideal.exists_radical_pow_le_of_fg — In a Noetherian ring the radical of every ideal is finitely generated, so the theorem gives radical(a)^n ≤ a, exactly Proposition 7.14.
Corollary: Corollary 7.15
The nilradical of a Noetherian ring is nilpotent.
Formalized. Mathlib/RingTheory/Noetherian/Nilpotent.lean::IsNoetherianRing.isNilpotent_nilradical — The nilradical of a Noetherian ring is nilpotent, exactly Corollary 7.15.
Corollary: Corollary 7.16
For A Noetherian, m maximal, and q an ideal: q is m-primary ⇔ r(q)=m ⇔ mⁿ⊆q⊆m for some n>0.
Formalized. Mathlib/RingTheory/Ideal/IsPrimary.lean::Ideal.isPrimary_of_isMaximal_radical; Ideal.exists_radical_pow_le_of_fg; radical/power monotonicity lemmas — For maximal 𝔪, radical(q)=𝔪 makes q primary; Noetherian finite generation gives a power 𝔪^n≤q, while q≤radical(q)=𝔪. Conversely 𝔪^n≤q≤𝔪 forces radical(q)=𝔪; properness excludes n=0, giving the source n>0 formulation.
Proposition: Proposition 7.17
For a≠(1) in a Noetherian ring, the prime ideals belonging to a are exactly the prime ideals occurring among the colon ideals (a:x), x∈A.
Formalized. Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean::Submodule.isAssociatedPrime_iff; Mathlib/RingTheory/Lasker.lean::IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes — In a Noetherian ring, associated primes are exactly prime colons (a:x); the Lasker first-uniqueness theorem identifies these with the radicals occurring in a minimal primary decomposition, exactly the source “prime ideals belonging to a”.