Chapter 8. Artin Rings (pp. 89–90)

FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.

This chapter contains 1 definition, 2 theorems, 5 propositions, 1 corollary, 1 example, 1 counterexample, 1 construction and 1 other statements.

Of the 13 statements checked against Lean, 10 are formalized somewhere and 3 are not.

Status	Statements	Share	What it means
in Mathlib	10	77%	Mathlib states and proves it.
not formalized	3	23%	A documented search found no Lean statement of it anywhere.
checked in total	13

Which versions of Lean and Mathlib were searched

• Project search: LeanCategories/** outside .lake/.agents/.git was searched first. The project reifies Artinian rings as LeanCategories.Algebra.ArtinianRingCat, but the theorem-level structure in this chapter is owned by pinned Mathlib.
• Pinned Mathlib: project pin db584cd6d46c92f209a44c0f1c829460d327499d (Apache-2.0, Lean v4.33.0), denoted P, contains the Artinian spectrum, nilpotence, Krull-dimension, localization/product, Nakayama, and cotangent-space interfaces cited below. The assembled U007 and U008 bundles were compile-checked against P; ZMod (p^n) synthesizes both Artinian and local structures for prime p.
• Current/open Mathlib: upstream 5aedf732b6987e8c26ab3c9ebc855314f82b045f (Apache-2.0), denoted H, was refreshed 2026-09-06 and retains the checked positive interfaces. The strict negative boundaries U010, U012, and U013 were searched in current/open work and broad indexed GitHub Lean code; no complete owner was found.
• N denotes dated 2026-09-06 negative evidence after project-first search, P/H, open/current work, installed packages, and targeted external Lean search. Partial positive examples or a two-clause subtheorem do not satisfy a bundled source row.

Proposition: Proposition 8.1

FC04-C08-U001 · § Artin Rings; pp. 89–90; L3277 · after FC04-C06-U015, FC04-C01-U020, FC04-C01-U021, FC04-C01-U022 · in Mathlib

Every prime ideal in an Artin ring is maximal.

Formalized. Mathlib/RingTheory/Artinian/Module.lean::IsArtinianRing.isMaximal_of_isPrime; isPrime_iff_isMaximal — Every prime ideal of a commutative Artinian ring is maximal, exactly Proposition 8.1.

Corollary: Corollary 8.2

FC04-C08-U002 · § Artin Rings; pp. 89–90; L3281 · after FC04-C08-U001, FC04-C01-U035, FC04-C01-U037 · in Mathlib

In an Artin ring, the nilradical equals the Jacobson radical.

Formalized. Mathlib/RingTheory/Artinian/Ring.lean::IsArtinianRing.jacobson_eq_radical; Ideal.jacobson_bot; nilradical — Specializing jacobson_eq_radical to the zero ideal identifies the Jacobson radical of the ring with its nilradical, exactly Corollary 8.2.

Proposition: Proposition 8.3

FC04-C08-U003 · § Artin Rings; pp. 89–90; L3283 · after FC04-C06-U015, FC04-C01-U021, FC04-C01-U040, FC04-C01-U047 · in Mathlib

An Artin ring has only finitely many maximal ideals.

Formalized. Mathlib/RingTheory/Artinian/Module.lean::IsArtinianRing.setOfPred_isMaximal_finite; Finite (MaximalSpectrum R) instance — An Artinian ring has finitely many maximal ideals, exactly Proposition 8.3.

Proposition: Proposition 8.4

FC04-C08-U004 · § Artin Rings; pp. 89–90; L3285 · after FC04-C06-U015, FC04-C01-U035, FC04-C01-U041 · in Mathlib

The nilradical of an Artin ring is nilpotent.

Formalized. Mathlib/RingTheory/Artinian/Ring.lean::IsArtinianRing.isNilpotent_nilradical — The nilradical of a commutative Artinian ring is nilpotent, exactly Proposition 8.4.

Definition: Chains of primes, length, and dimension of a ring

FC04-C08-U005 · § Artin Rings; pp. 89–90; L3289 · after FC04-C01-U020, FC04-C06-U020 · in Mathlib

A chain of prime ideals is a finite strict chain p₀⊂⋯⊂pₙ; its length is n. For A≠0, dim A is the supremum of these lengths (an integer ≥0 or +∞). A field has dimension 0 and Z has dimension 1.

Formalized. Mathlib/RingTheory/KrullDimension/Basic.lean::ringKrullDim; Mathlib/Order/KrullDimension.lean::Order.krullDim; Mathlib/RingTheory/KrullDimension/Field.lean::ringKrullDim_eq_zero_of_field; Mathlib/RingTheory/KrullDimension/PID.lean::IsPrincipalIdealRing.ringKrullDim_eq_one — ringKrullDim is the supremum of strict prime-chain lengths (with bottom for the zero ring and top for infinity). Fields have dimension 0; applying the PID theorem with Int.not_isField gives dim ℤ=1.

Theorem: Theorem 8.5

FC04-C08-U006 · § Artin Rings; pp. 89–90; L3291 · after FC04-C06-U015, FC04-C08-U001, FC04-C08-U003, FC04-C08-U004, FC04-C08-U005, FC04-C06-U014, FC04-C07-U015, FC04-C07-U017, FC04-C06-U030 · in Mathlib

A ring A is Artin if and only if A is Noetherian and dim A=0.

Formalized. Mathlib/RingTheory/HopkinsLevitzki.lean::isArtinianRing_iff_isNoetherianRing_krullDimLE_zero; Mathlib/RingTheory/KrullDimension/Zero.lean::ringKrullDimZero_iff_ringKrullDim_eq_zero — For a nonzero commutative ring, Artinianity is equivalent to Noetherianity plus Krull dimension zero, exactly Theorem 8.5.

Comparison / example: Structure of an Artin local ring

FC04-C08-U007 · § Artin Rings; pp. 89–90; L3295 · after FC04-C08-U001, FC04-C08-U004, FC04-C01-U028, FC04-C01-U015, FC04-C01-U035 · in Mathlib

For an Artin local ring (A,m), m is the unique prime and the nilradical, hence is nilpotent; every element is either a unit or nilpotent. Z/(pⁿ) is the standard example.

Formalized. Mathlib/RingTheory/KrullDimension/Zero.lean::Ring.KrullDimLE.existsUnique_isPrime; Ring.KrullDimLE.nilradical_eq_maximalIdeal; Ring.KrullDimLE.isNilpotent_iff_mem_nonunits; P Artinian/nilpotence and ZMod instances — An Artinian local ring has a unique prime, its maximal ideal equals the nilradical and is nilpotent, and every element is a unit or nilpotent. For prime p, the environment synthesizes IsArtinianRing (ZMod (p^n)) and IsLocalRing (ZMod (p^n)), realizing the standard ℤ/(p^n) example. The complete bundle was compile-checked.

Proposition: Proposition 8.6

FC04-C08-U008 · § Artin Rings; pp. 89–90; L3298 · after FC04-C06-U014, FC04-C01-U028, FC04-C02-U031, FC04-C08-U006 · in Mathlib

For a Noetherian local ring (A,m), exactly one holds: mⁿ≠mⁿ⁺¹ for every n, or mⁿ=0 for some n, in which case A is an Artin local ring.

Formalized. Mathlib/RingTheory/Nakayama.lean::Submodule.eq_bot_of_le_smul_of_le_jacobson_bot; Mathlib/RingTheory/HopkinsLevitzki.lean::isArtinianRing_iff_isNilpotent_maximalIdeal; IsLocalRing.jacobson_eq_maximalIdeal — If two consecutive powers of the maximal ideal of a Noetherian local ring coincide, Nakayama forces that power to be zero; conversely nilpotence produces a stationary zero power. Thus exactly the source dichotomy holds, and the nilpotent branch is equivalent to being Artinian. This assembly was compile-checked against P.

Theorem: Theorem 8.7 (structure theorem for Artin rings)

FC04-C08-U009 · § Artin Rings; pp. 89–90; L3304 · after FC04-C08-U001, FC04-C08-U003, FC04-C08-U004, FC04-C01-U043, FC04-C01-U046, FC04-C04-U028 · in Mathlib

Every Artin ring is, uniquely up to isomorphism, a finite direct product of Artin local rings.

Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::MaximalSpectrum.toPiLocalizationEquiv; finite MaximalSpectrum instance; Mathlib/RingTheory/Artinian/Ring.lean::IsArtinianRing.localization_artinian; Localization.AtPrime local-ring instance — The Artinian spectrum is finite and discrete, and toPiLocalizationEquiv canonically identifies the ring with the product of its localizations at all maximal ideals; each factor is an Artinian local ring. Indexing by the intrinsic maximal spectrum gives the source uniqueness up to permutation/isomorphism.

Counterexample: One prime ideal does not imply Artinian

FC04-C08-U010 · § Artin Rings; pp. 89–90; L3310 · after FC04-C08-U005, FC04-C06-U014, FC04-C01-U028 · not formalized

For A=k[x₁,x₂,…] and a=(x₁,x₂²,…,xₙⁿ,…), B=A/a has one prime ideal and is local of dimension 0, but is not Noetherian because that prime is not finitely generated.

Not formalized. partial: MvPolynomial, quotient, Krull-dimension and Noetherian APIs — No checked project/P/H/external declaration realizes the source quotient of the infinite-variable polynomial ring by (x₁,x₂²,…,x_n^n,…), proves it has one prime/local dimension zero, and proves that prime is not finitely generated, hence the ring is not Noetherian.

Searched: N

Construction / comparison: The vector space m/m²

FC04-C08-U011 · § Artin Rings; pp. 89–90; L3312 · after FC04-C01-U028, FC04-C01-U029, FC04-C02-U008, FC04-C02-U033, FC04-C02-U034 · in Mathlib

For a local ring (A,m) with residue field k=A/m, m/m² is naturally a k-vector space. If m is finitely generated, its generator images span m/m², so this vector space is finite-dimensional.

Formalized. Mathlib/RingTheory/Ideal/Cotangent.lean::Ideal.Cotangent; IsLocalRing.CotangentSpace; Ideal.toCotangent; Mathlib/Algebra/Module/SpanRankOperations.lean::IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg — Ideal.Cotangent m is exactly m/m²; for the maximal ideal it carries the residue-field vector-space structure. Finite generation of m makes the cotangent space finite-dimensional, and generator images span it.

Proposition: Proposition 8.8

FC04-C08-U012 · § Artin Rings; pp. 89–90; L3314 · after FC04-C08-U007, FC04-C08-U011, FC04-C08-U004, FC04-C02-U031, FC04-C02-U034 · not formalized

For an Artin local ring (A,m) with residue field k, the following are equivalent: every ideal is principal; m is principal; dim_k(m/m²)≤1.

Not formalized. partial: Mathlib/RingTheory/Ideal/Cotangent.lean::IsLocalRing.finrank_cotangentSpace_le_one_iff; generic IsPrincipalIdealRing APIs — P/H prove exactly dim_k(m/m²)≤1 ↔︎ m principal in a Noetherian local ring, but no checked theorem supplies the remaining Artinian-local implication m principal ⇒ every ideal principal. The nearby DVR TFAE assumes a domain, so it does not realize Proposition 8.8 at the source generality.

Searched: N

Examples / counterexample: Principal-ideal Artin local examples

FC04-C08-U013 · § Artin Rings; pp. 89–90; L3328 · after FC04-C08-U012 · not formalized

Z/(pⁿ) and k[x]/(fⁿ) (f irreducible) satisfy the principal-ideal criterion; k[x²,x³]/(x⁴) does not, since m=(x²,x³), m²=0, and dim(m/m²)=2. The frozen extraction cites “conditions of (8.7)” here, apparently for 8.8.

Not formalized. partial: ZMod, polynomial quotient, principal-ideal-ring and cotangent APIs — P/H cover the positive principal quotient infrastructure, but no checked declaration realizes the complete source bundle, in particular the cusp-ring quotient k[x²,x³]/(x⁴) with m=(x²,x³), m²=0, and two-dimensional m/m².

Searched: N