Chapter 6. Chain Conditions (pp. 74–77)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 16 definitions, 1 theorem, 9 propositions, 2 corollaries and 2 other statements.
Of the 30 statements checked against Lean, 28 are formalized somewhere and 2 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 23 | 77% | Mathlib states and proves it. |
| in lean-categories | 5 | 17% | This repository states and proves it. |
| not formalized | 2 | 7% | A documented search found no Lean statement of it anywhere. |
| checked in total | 30 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first. Project HEAD351cba0287077eadfcd7c71a78ec4a509ce8c966explicitly reifies Noetherian modules, Artinian modules, simple modules, Noetherian rings, and Artinian rings as full subcategories; these definition rows areproject-existing, with the source equivalences supplied by the pinned Mathlib predicates. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, contains the chain-condition, finite-length, composition-series, Jordan–Hölder, and length APIs cited below. Critical declarations were compile-checked against the project environment. - Current/open Mathlib: upstream
5aedf732b6987e8c26ab3c9ebc855314f82b045f(Apache-2.0), denotedH, was checked 2026-09-06. The C06 positive declarations persist there. U010, U016, and U030 were separately searched in current/open work rather than inferred from nearby general results. - External negative search: targeted GitHub/indexed Lean searches found no strict owner for U010’s six-example module bundle or U016’s ring-example bundle; in particular the compact-Hausdorff function-ring and infinite-variable polynomial counterexamples remain absent. U030 is not negative: its source criterion compiles directly from pinned prime/product, Krull-dimension-zero, and Hopkins–Levitzki APIs.
Ndenotes dated 2026-09-06 negative evidence after project-first search, P/H, current/open work, installed packages, and targeted external search. Concrete comparison bundles are not credited piecemeal.
Definition: Partially ordered set
A relation ≤ on Σ is reflexive, transitive, and antisymmetric.
Formalized. Mathlib/Order/Defs/PartialOrder.lean::PartialOrder — The bundled order relation supplies reflexivity, transitivity, and antisymmetry exactly as in the source.
Definition: Stationary increasing sequence
x₁≤x₂≤⋯ is stationary if x_n=x_{n+1}=⋯ for some n.
Formalized. Mathlib/Order/Filter/EventuallyConst.lean::Filter.EventuallyConst; eventuallyConst_atTop; eventuallyConst_atTop_nat — For a monotone ℕ-sequence, eventual constancy at atTop is exactly existence of an index after which all terms are equal.
Proposition 6.1: Ascending-chain criterion for maximal elements
Every increasing sequence in Σ is stationary iff every nonempty subset of Σ has a maximal element.
Formalized. Mathlib/Order/OrderIsoNat.lean::wellFoundedGT_iff_monotone_chain_condition; Mathlib/Order/WellFounded.lean::wellFoundedGT_iff_exists_maximal — Both source conditions are equivalent to WellFoundedGT: every increasing sequence stabilizes iff every nonempty subset has a maximal element.
Definition: Ascending chain condition (a.c.c.)
For submodules ordered by inclusion, the stationary-chain condition of Proposition 6.1.
Formalized. Mathlib/RingTheory/Noetherian/Defs.lean::monotone_stabilizes_iff_noetherian — Specializing the abstract chain condition to the submodule lattice gives exactly the ascending chain condition.
Definition: Maximal condition
For submodules, every nonempty family has a maximal member; equivalent to a.c.c.
Formalized. Mathlib/RingTheory/Noetherian/Defs.lean::set_has_maximal_iff_noetherian — Every nonempty family of submodules has a maximal member iff the module is Noetherian, hence iff ACC holds.
Definition: Noetherian module
An A-module satisfying a.c.c., equivalently the maximal condition.
Formalized. LeanCategories/Modules/Mathlib.lean::LeanCategories.NoetherianModuleCat; P IsNoetherian; monotone_stabilizes_iff_noetherian; set_has_maximal_iff_noetherian — The project explicitly reifies Noetherian modules as a full subcategory; pinned Mathlib identifies its predicate with both source ACC and maximal-condition formulations.
Searched: repo HEAD + P
Definition: Descending chain condition (d.c.c.)
For submodules ordered by reverse inclusion, the stationary-chain condition.
Formalized. Mathlib/RingTheory/Artinian/Module.lean::monotone_stabilizes_iff_artinian — The theorem is the stationary-chain condition on the order-dual submodule lattice, exactly DCC.
Definition: Minimal condition
Every nonempty family of submodules has a minimal member; equivalent to d.c.c.
Formalized. Mathlib/RingTheory/Artinian/Module.lean::set_has_minimal_iff_artinian — Every nonempty family of submodules has a minimal member iff the module is Artinian/DCC.
Definition: Artinian module
An A-module satisfying d.c.c., equivalently the minimal condition.
Formalized. LeanCategories/Modules/Mathlib.lean::LeanCategories.ArtinianModuleCat; P IsArtinian; monotone_stabilizes_iff_artinian; set_has_minimal_iff_artinian — The project explicitly reifies Artinian modules as a full subcategory; pinned Mathlib supplies the exact DCC/minimal-condition equivalences.
Searched: repo HEAD + P
Reusable examples: Modules separating the two chain conditions
Finite abelian groups satisfy both; Z has a.c.c. but not d.c.c.; the p-primary subgroup of Q/Z has d.c.c. but not a.c.c.; Z[1/p] has neither; k[x] has a.c.c. but not d.c.c.; k[x₁,x₂,…] has neither.
Not formalized. partial: finite-module Noetherian/Artinian instances; PID and polynomial Noetherian APIs — P/H realize several individual examples, but no checked declaration or external Lean source realizes the full six-example bundle, in particular the Prüfer p-primary subgroup of ℚ/ℤ, ℤ[1/p], and the infinitely generated polynomial ring with the stated separating chain conditions.
Searched: N
Proposition 6.2: Noetherian iff all submodules are finitely generated
M is Noetherian exactly when every submodule of M is finitely generated.
Formalized. Mathlib/RingTheory/Noetherian/Defs.lean::isNoetherian_def — Exactly IsNoetherian R M ↔︎ ∀ N : Submodule R M, N.FG, Proposition 6.2.
Proposition 6.3: Chain conditions in a short exact sequence
For 0→M′→M→M″→0, M is Noetherian iff M′ and M″ are; similarly for Artinian.
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_iff_submodule_quotient; isNoetherian_of_range_eq_ker; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_iff_submodule_quotient; isArtinian_of_range_eq_ker — The submodule/quotient equivalences give the canonical short exact sequence iff; the range=kernel versions realize arbitrary exact maps after the standard identifications.
Corollary 6.4: Finite direct sums preserve Noetherian/Artinian
A finite direct sum of Noetherian modules is Noetherian; likewise for Artinian modules.
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_prod; isNoetherian_pi; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_prod; isArtinian_pi; isArtinian_finsupp — Finite products/direct sums of Noetherian modules are Noetherian and of Artinian modules are Artinian; finite Finsupp agrees with finite Pi.
Definition: Noetherian ring
A ring A that is Noetherian as an A-module, equivalently satisfies a.c.c. on ideals.
Formalized. LeanCategories/Algebra/Concrete/Rings.lean::LeanCategories.Algebra.NoetherianRingCat; P IsNoetherianRing; isNoetherianRing_iff_ideal_fg — The project explicitly reifies Noetherian commutative rings; the pinned predicate is Noetherianity of the self-module, equivalently ACC/finiteness on ideals.
Searched: repo HEAD + P
Definition: Artinian ring
A ring A that is Artinian as an A-module, equivalently satisfies d.c.c. on ideals.
Formalized. LeanCategories/Algebra/Concrete/Rings.lean::LeanCategories.Algebra.ArtinianRingCat; P IsArtinianRing and Artinian self-module characterization — The project explicitly reifies Artinian commutative rings; the pinned predicate is Artinianity of the self-module, equivalently DCC on ideals.
Searched: repo HEAD + P
Reusable comparisons: Basic Noetherian and Artinian ring examples
Fields and Z/(n), n≠0, are both; Z and every PID are Noetherian but Z is not Artinian; k[x₁,x₂,…] is not Noetherian, showing subrings of Noetherian rings need not be Noetherian; C(X) for compact infinite Hausdorff X is not Noetherian.
Not formalized. partial: field/finite/PID/Noetherian polynomial APIs; topological ring infrastructure — No checked project/P/H or external declaration realizes the complete source comparison bundle, especially non-Noetherianity of k[x₁,x₂,…] and of C(X) for compact infinite Hausdorff X, together with all stated positive examples.
Searched: N
Proposition 6.5: Finite modules over Noetherian/Artinian rings
If A is Noetherian (resp. Artinian) and M is finitely generated, then M is Noetherian (resp. Artinian).
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_of_isNoetherianRing_of_finite; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_of_fg_of_artinian' — A finitely generated module over a Noetherian ring is Noetherian and over an Artinian ring is Artinian, exactly Proposition 6.5.
Proposition 6.6: Quotients of Noetherian/Artinian rings
If A is Noetherian (resp. Artinian) and 𝔞 an ideal, then A/𝔞 is Noetherian (resp. Artinian).
Formalized. Mathlib/RingTheory/Noetherian/Basic.lean::isNoetherian_quotient; Mathlib/RingTheory/Artinian/Module.lean::isArtinian_of_quotient_of_artinian; quotient-ring instance — Quotients of Noetherian modules/rings and Artinian modules/rings retain the corresponding chain condition.
Definition: Chain of submodules
A finite strictly descending sequence M=M₀⊃M₁⊃⋯⊃M_n=0.
Formalized. Mathlib/Order/RelSeries.lean::LTSeries, applied to the submodule lattice/order dual — A finite strict series supplies precisely a finite strict chain; reversing order/orientation gives the source descending chain from M to 0.
Definition: Length of a chain
The number n of strict inclusions (“links”) in the chain.
Formalized. Mathlib/Order/RelSeries.lean::RelSeries.length; LTSeries.length — The series length is the number of strict links, exactly the source convention.
Definition: Composition series
A maximal chain of submodules, i.e. one into which no additional submodule can be inserted.
Formalized. Mathlib/Order/JordanHolder.lean::CompositionSeries — A composition series is a finite nonempty series whose adjacent terms are covers (IsMaximal), i.e. a chain admitting no insertion between successive terms; endpoint conditions recover the source whole-module series.
Definition: Simple module
A module with no submodules except 0 and itself; a chain is a composition series exactly when every successive quotient is simple.
Formalized. LeanCategories/Modules/Mathlib.lean::LeanCategories.SimpleModuleCat; P IsSimpleModule; covBy_iff_quot_is_simple — The project reifies simple modules; pinned Mathlib identifies a cover of submodules with simplicity of the successive quotient, exactly the source composition-series criterion.
Searched: repo HEAD + P
Proposition 6.7: Jordan–Hölder length precursor
If M has a composition series of length n, every composition series has length n and every chain extends to a composition series.
Formalized. Mathlib/Order/RelSeries.lean::LTSeries.exists_relSeries_covBy_and_head_eq_bot_and_last_eq_bot; Mathlib/RingTheory/FiniteLength.lean::isFiniteLength_of_exists_compositionSeries; Mathlib/RingTheory/Length.lean::Module.length_compositionSeries — Existence of one whole-module composition series gives finite length and both chain conditions; any strict chain then refines/embeds into a cover series from bottom to top, while every composition series has the common Module.length.
Proposition 6.8: Finite composition series iff both chain conditions
M has a composition series iff M satisfies both a.c.c. and d.c.c.
Formalized. Mathlib/RingTheory/FiniteLength.lean::isFiniteLength_iff_isNoetherian_isArtinian; isFiniteLength_iff_exists_compositionSeries — A module admits a composition series iff it is both Noetherian and Artinian, exactly Proposition 6.8.
Definition: Module of finite length
A module satisfying both a.c.c. and d.c.c.
Formalized. Mathlib/RingTheory/FiniteLength.lean::IsFiniteLength; isFiniteLength_iff_isNoetherian_isArtinian — Mathlib encodes finite length as finite iterated simple extensions and proves it equivalent to the source ACC+DCC definition.
Definition: Length of a module
For a finite-length module, the common length l(M) of all composition series.
Formalized. Mathlib/RingTheory/Length.lean::Module.length; Module.length_compositionSeries — For a finite-length module every composition series has length equal to Module.length, giving the source common integer length (viewed in ℕ∞).
Theorem (Jordan–Hölder): Composition factors are unique up to permutation and isomorphism
Any two composition series of a finite-length module have their successive quotient modules in bijection so that corresponding factors are isomorphic.
Formalized. Mathlib/Order/JordanHolder.lean::CompositionSeries.jordan_holder; Mathlib/RingTheory/SimpleModule/Basic.lean::JordanHolderLattice.Iso.linearEquiv — Jordan–Hölder equivalence matches the intervals of two composition series up to permutation, and Iso.linearEquiv turns corresponding intervals into linear equivalences of the successive quotient modules.
Proposition 6.9: Length is additive
For 0→M′→M→M″→0 of finite-length modules, l(M)=l(M′)+l(M″).
Formalized. Mathlib/RingTheory/Length.lean::Module.length_eq_add_of_exact — For an injective first map, surjective second map, and exact pair, module length is the sum of the endpoint lengths, exactly Proposition 6.9.
Proposition 6.10: Finite-dimensional vector spaces and chain conditions
For a k-vector space, finite dimension, finite length, a.c.c., and d.c.c. are equivalent; when finite, length equals dimension.
Formalized. Mathlib/RingTheory/FiniteLength.lean::IsSemisimpleModule.finite_tfae; Mathlib/RingTheory/Length.lean::Module.length_eq_finrank — Over a field/division ring, vector spaces are semisimple; the TFAE identifies finite generation/dimension, Noetherianity, Artinianity, and finite length, and length_eq_finrank identifies length with dimension.
Corollary 6.11: Noetherian iff Artinian under a maximal-ideal product filtration
If 0=𝔪₁⋯𝔪_n is a product of maximal ideals, then A is Noetherian iff A is Artinian.
Formalized. Mathlib/RingTheory/Ideal/Operations.lean::Ideal.IsPrime.prod_le; Mathlib/RingTheory/KrullDimension/Basic.lean::Ring.KrullDimLE.mk₀; Mathlib/RingTheory/HopkinsLevitzki.lean::isArtinianRing_iff_isNoetherianRing_krullDimLE_zero — If a finite product of maximal ideals is zero, every prime contains one factor by IsPrime.prod_le, hence equals that maximal ideal; KrullDimLE.mk₀ gives dimension at most zero, and Hopkins–Levitzki yields Noetherian ⇒ Artinian. The reverse Artinian ⇒ Noetherian is the same pinned equivalence. The assembled source theorem was compile-checked against P.