Chapter 4. Primary Decomposition (pp. 50–54)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 9 definitions, 2 theorems, 6 propositions, 2 lemmas, 1 corollary, 1 notation and 8 other statements.
Of the 29 statements checked against Lean, 19 are formalized somewhere and 10 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 14 | 48% | Mathlib states and proves it. |
| not formalized | 10 | 34% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 5 | 17% | This repository states and proves it. |
| checked in total | 29 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first. The project owns source-shaped definitions of primary decompositions, their prime sets, isolated/embedded primes, and ideal extension/contraction. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, contains the primary-ideal and Lasker APIs cited below; it explicitly documents the first and second uniqueness theorems as Atiyah–Macdonald 4.5 and 4.10. - Current/open Mathlib: live upstream
29ea5de9cb981cb62dfa7979aaff0851f50c603a(Apache-2.0), denotedM, was refreshed 2026-09-06. Its only change from previously checked810b3888d0aa94294b18587c453466bc86c1f0fcisMathlib/Combinatorics/SimpleGraph/Maps.lean, so none of the Chapter-4 algebraic negative judgments changes. Relevant open-PR searches found no owner for the strict gaps. - External negative search:
rootkiller6788/mini-commutative-homological-algebra@1812d8da6e788d3ee35920a4d23a5d4ede7dfe46was rechecked; it contains only skeletal/string-level primary-decomposition material for these boundaries, not proofs of the source rows. For localization-preserves-primary,NeoMathlib@a49fe074238f9c6b38e0c4b25c3fb93c80f605eeandduong-ngo/mathlib4@abc669d11b88e163aed1c05b352b5b16889c4ad8were also checked and have only generic contraction APIs. Ndenotes dated 2026-09-06 negative evidence after project-first search, P/M, open/current work, and targeted external Lean search. Concrete examples and strict theorem bundles are not credited from nearby generic infrastructure.
Definition: Primary ideal
A proper ideal 𝔮 such that xy∈𝔮 implies x∈𝔮 or y^n∈𝔮 for some n>0; equivalently A/𝔮≠0 and every zero-divisor of A/𝔮 is nilpotent.
Formalized. Ideal.IsPrimary; Ideal.isPrimary_iff; Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul — The product criterion is the source definition; the quotient theorem gives the equivalent nonzero-quotient/nilpotent-zero-divisor characterization.
Comparison: Prime ideals and contractions of primary ideals
Every prime ideal is primary; the contraction of a primary ideal along a ring homomorphism is primary.
Formalized. Ideal.IsPrime.isPrimary; Ideal.IsPrimary.comap — Every prime is primary, and contraction of a primary ideal along a ring homomorphism is primary.
Proposition 4.1: Radical of a primary ideal is prime
If 𝔮 is primary then r(𝔮) is the smallest prime ideal containing 𝔮.
Formalized. Ideal.isPrime_radical; Ideal.IsPrime.radical_le_iff — The radical of a primary ideal is prime and is the least prime containing it.
Definition: 𝔭-primary ideal
A primary ideal 𝔮 with r(𝔮)=𝔭 is called 𝔭-primary.
Formalized. Ideal.IsPrimary; Ideal.radical — “q is p-primary” is exactly q.IsPrimary ∧ q.radical = p.
Reusable example: Primary ideals of Z
The primary ideals of Z are (0) and (p^n) for primes p.
Not formalized. partial: generic primary/PID/ℤ ideal APIs — No checked declaration classifies all primary ideals of ℤ as (0) and (p^n).
Searched: N
Reusable example: Primary ideal need not be a prime power
In k[x,y], 𝔮=(x,y²) is primary with radical (x,y), and 𝔭²⊊𝔮⊊𝔭.
Not formalized. partial: multivariable-polynomial ideal/radical APIs — No checked declaration realizes q=(x,y²) in k[x,y] together with its radical and strict p²<q<p comparisons.
Searched: N
Reusable counterexample: Prime power need not be primary
In k[x,y,z]/(xy−z²), 𝔭=(x̄,z̄) is prime but 𝔭² is not primary.
Not formalized. partial: quotient-polynomial and primary APIs — No checked declaration realizes the k[x,y,z]/(xy-z²) example with p=(x,z) prime but p² non-primary.
Searched: N
Proposition 4.2: Maximal radical implies primary
If r(𝔞) is maximal then 𝔞 is primary; hence powers of a maximal ideal are primary.
Formalized. Ideal.isPrimary_of_isMaximal_radical; Ideal.radical_pow — Maximal radical implies primary; positive powers of a maximal ideal have that maximal radical and are primary.
Lemma 4.3: Finite intersections of 𝔭-primary ideals
A finite intersection of 𝔭-primary ideals is 𝔭-primary.
Formalized. Ideal.isPrimary_finsetInf; Ideal.radical_finset_inf — A finite nonempty intersection of primary ideals with common radical is primary with the same radical.
Lemma 4.4: Colon of a primary ideal
For 𝔮 𝔭-primary: x∈𝔮 gives (𝔮:x)=(1); x∉𝔮 gives (𝔮:x) 𝔭-primary; x∉𝔭 gives (𝔮:x)=𝔮.
Not formalized. partial: Submodule.IsPrimary.radical_colon_singleton_of_notMem; radical_colon_singleton_eq_ite; colon-top lemmas — P/M determine the radical/top cases but do not prove that (q:x) itself is p-primary for x∉q or the full equality (q:x)=q for x∉p.
Searched: N
Definition: Primary decomposition
An expression 𝔞=⋂_{i=1}^n 𝔮_i as a finite intersection of primary ideals.
Formalized. LeanCategories.Algebra.Ideal.IsPrimaryDecomposition — Exactly a finite intersection of primary ideals equal to the given ideal.
Searched: repo HEAD
Definition: Minimal primary decomposition
A primary decomposition with distinct radicals and no component containing the intersection of all the others; synonyms: irredundant, reduced, normal.
Formalized. Submodule.IsMinimalPrimaryDecomposition / alias Ideal.IsMinimalPrimaryDecomposition — Fields encode intersection equality, primary components, distinct radicals, and irredundancy.
Definition: Decomposable ideal
An ideal admitting a primary decomposition; every primary decomposition can be reduced to a minimal one.
Formalized. IsLasker; Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition — Decomposability is existence of a finite primary decomposition, and every such decomposition reduces to a minimal one.
Theorem 4.5 (1st uniqueness theorem): Associated primes are intrinsic
For a minimal decomposition 𝔞=⋂𝔮_i with 𝔭_i=r(𝔮_i), the 𝔭_i are exactly the prime ideals occurring among r(𝔞:x); hence independent of the decomposition.
Formalized. Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes — Explicitly documented as Atiyah–Macdonald Theorem 4.5; component radicals equal the intrinsic associated primes/colon radicals.
Reusable example: A decomposition with embedded prime
For 𝔞=(x²,xy)⊂k[x,y], 𝔞=(x)∩(x,y)²; the associated primes are (x)⊂(x,y), and 𝔞 is not primary.
Not formalized. partial: primary-decomposition/associated-prime APIs — No checked declaration proves (x²,xy)=(x)∩(x,y)² with the displayed associated primes and non-primaryity.
Searched: N
Definition: Prime ideal associated with / belonging to an ideal
The primes 𝔭_i determined by Theorem 4.5 are said to belong to, or be associated with, 𝔞.
Formalized. LeanCategories.Algebra.Ideal.primaryDecompositionPrimes; P image_radical_eq_associated_primes — The project records component radicals; on a minimal decomposition the pinned first uniqueness theorem identifies them with intrinsic associated primes.
Searched: repo HEAD + P
Definition: Minimal / isolated associated prime
A minimal element among the associated primes of 𝔞.
Formalized. LeanCategories.Algebra.Ideal.isolatedPrime — Minimal among the decomposition primes; after U014 this is exactly a minimal/isolated associated prime.
Searched: repo HEAD
Definition: Embedded associated prime
An associated prime that is not minimal/isolated.
Formalized. LeanCategories.Algebra.Ideal.embeddedPrime — An associated decomposition prime that is not isolated, matching the source after U014.
Searched: repo HEAD
Proposition 4.6: Minimal associated primes are minimal over 𝔞
Every prime 𝔭⊇𝔞 contains a minimal prime belonging to 𝔞; the minimal associated primes are exactly the minimal primes containing 𝔞.
Formalized. Ideal.exists_minimalPrimes_le; Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical; image_radical_eq_associated_primes — Every prime over the ideal contains a minimal associated prime; minimal associated primes are exactly minimal primes over the ideal.
Reusable comparison: Geometric meaning of isolated and embedded primes
For polynomial rings, minimal primes correspond to irreducible components, whereas embedded primes correspond to subvarieties inside those components.
Formalized. Ideal.minimalPrimes.equivIrreducibleComponents; PrimeSpectrum.zeroLocusEquivIrreducibleCloseds — Minimal primes correspond to irreducible components of V(I); the order-reversing prime/irreducible-closed correspondence places nonminimal associated primes inside components.
Reusable counterexample: Embedded primary components are not intrinsic
(x²,xy)=(x)∩(x,y)²=(x)∩(x²,y) gives distinct minimal primary decompositions with the same associated primes.
Not formalized. partial: Lasker uniqueness APIs — No checked declaration proves the two displayed decompositions of (x²,xy) with distinct embedded primary components.
Searched: N
Proposition 4.7: Zero-divisors from associated primes
For decomposable 𝔞, ⋃𝔭_i={x:(𝔞:x)≠𝔞}; if 0 is decomposable, the zero-divisors are the union of primes belonging to 0 and nilpotents are the intersection of its minimal primes.
Not formalized. partial: Module.biUnion_associatedPrimes_eq_zero_divisors (Noetherian); minimal-prime/nilradical APIs — The closest zero-divisor union theorem assumes Noetherianity, while the source assumes only decomposability; the complete weaker-hypothesis bundle is absent.
Searched: N
Proposition 4.8: Localization of a primary ideal
For 𝔮 𝔭-primary: if S meets 𝔭 then S⁻¹𝔮=S⁻¹A; if S∩𝔭=∅ then S⁻¹𝔮 is S⁻¹𝔭-primary and contracts back to 𝔮.
Not formalized. partial: IsLocalization.map_eq_top_of_not_subset; IsLocalization.under_map_of_isPrimary_disjoint — P/M prove discard and contraction-back clauses but not that the surviving extended ideal is primary with localized radical.
Searched: N
Notation / construction: S(𝔞)
For an ideal 𝔞 and multiplicative S, S(𝔞) denotes the contraction to A of S⁻¹𝔞.
Formalized. LeanCategories.Algebra.extendedIdeal; LeanCategories.Algebra.contractedIdeal — S(a) is exactly contraction after extension/localization.
Searched: repo HEAD
Proposition 4.9: Localization of a primary decomposition
Localizing a minimal primary decomposition discards exactly the components whose radicals meet S; the surviving localized components and their contraction give minimal primary decompositions.
Not formalized. partial: IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite; comap_localized₀_eq_iInf — P handles a special submonoid attached to a lower set of associated primes, not arbitrary S; the missing localized-primary clause from U023 is essential.
Searched: N
Definition: Isolated set of associated primes
A set Σ of primes belonging to 𝔞 that is downward closed among the associated primes: 𝔭′⊆𝔭∈Σ and 𝔭′ associated implies 𝔭′∈Σ.
Formalized. comap_localized₀_eq_iInf hypothesis hs₀ : IsLowerSet ... — The lower-set condition on associated primes is exactly the source isolated-set condition.
Theorem 4.10 (2nd uniqueness theorem): Uniqueness for isolated sets
For any isolated set {𝔭_{i_1},…,𝔭_{i_m}}, the intersection 𝔮_{i_1}∩⋯∩𝔮_{i_m} is independent of the chosen minimal decomposition.
Formalized. Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf — Explicitly documented as Atiyah–Macdonald Theorem 4.10; the isolated-set intersection is canonical and independent of decomposition.
Corollary 4.11: Isolated primary components are unique
Primary components corresponding to minimal associated primes are uniquely determined by 𝔞.
Formalized. singleton/minimal-prime specialization of comap_localized₀_eq_iInf — A singleton isolated minimal associated prime has a uniquely determined primary component.
Comparison: Embedded primary components are generally nonunique
Unlike isolated components, embedded primary components are not uniquely determined; in Noetherian rings there can be infinitely many choices.
Not formalized. partial: isolated-component uniqueness only — No checked theorem/example proves general nonuniqueness of embedded primary components or the stronger Noetherian infinite-choice claim.
Searched: N