Chapter 2. Prime ideals
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 31 definitions, 34 theorems, 3 lemmas, 8 corollaries, 8 examples, 1 counterexample, 5 constructions, 1 criterion and 1 other statements.
Of the 92 statements checked against Lean, 50 are formalized somewhere and 42 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 50 | 54% | Mathlib states and proves it. |
| not formalized | 42 | 46% | A documented search found no Lean statement of it anywhere. |
| checked in total | 92 |
- Canonical source block: FC13 Matsumura Chapter 2,
FC13-C02-U001–FC13-C02-U092, §§4–6 plus the appendix to §6, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves the promoted catalogue throughagent-memory, asserts all 92 IDs occur exactly once and in order, and emits exactly one Sweep-II route per unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280on Lean 4.33.0. Project files are Apache-2.0.LeanCategories/Algebra/Ideals.leanalready wraps ideal map/comap and localization extension/contraction, and the project has ideal-level primary-decomposition descriptors plusAffineVarietyDimension; none owns an entire C02 source row more completely than the pinned interfaces once C02’s extra theorem clauses and module-level generality are enforced. No row is therefore reclassified asproject-existingmerely from a partial wrapper. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, repositoryleanprover-community/mathlib4, Apache-2.0, Lean 4.33.0, and directly project-compatible. The generator asserts the local Mathlib checkout is exactly P and verifies every cited pinned path and declaration token before emitting the chapter record. - Current Mathlib was independently refreshed on 2026-09-07 to
H=f15b4f161f6ff698ab91b4494faa75925856d0f5, repositoryleanprover-community/mathlib4, Apache-2.0, Lean 4.34.0-rc2. Current-source and open-PR searches were concentrated on every pinned gap: primary ideals under localization, Theorem 4.3 intermediate-ring recognition, fibre-vanishing and generator loci, catenarity, finite-type dimension=trdeg, Forster–Swan/j-Spec, the Matsumura associated-prime convention, and secondary/attached-prime theory. No exact post-pin declaration closes one of these bundles, so C02 has noreference-portroute. - Search channels used project source; pinned P; current H; open Mathlib PRs; Loogle and LeanSearch through the project LeanSearchClient; Mathlib source/docs; Lean Reservoir/indexed web discovery; and discoverable Lean repositories through GitHub code search. No compatible independent package/import owner was found for a C02 gap, so C02 has no
package-importroute. - Strict bundle semantics were enforced. In particular U008 is not credited without localization preserving primary ideals; U030 is not credited from tensor localization without Tor; U037 is not credited from the free locus alone; U050 is not credited from the algebraically-closed maximal-ideal theorem without the arbitrary-field n-generator clause; and U057 is not promoted from unbundled span-rank ingredients without a source-shaped μ(p,M) interface.
- Associated-prime convention is checked explicitly. Matsumura U066 defines associated primes by exact equality
P=ann(x)for arbitrary rings. Mathlib’s general predicate usesP=radical(ann x)and only proves exact annihilator equivalence underIsNoetherianRing. Hence U066, the general clause in U069, and arbitrary-ring U071 remain unmatched, while the Noetherian rows U068/U070/U072–U074 can safely useisAssociatedPrime_iffand the associated-prime APIs. - The secondary-representation appendix U083–U092 was searched independently rather than conflated with associated-prime/primary-decomposition support. No compatible secondary/P-secondary, attached-prime, or secondary-representation API was found; U089 alone maps to the generic lattice predicate
SupIrred ⊤because that definition is independently exact. - Route totals for C02:
mathlib50,project-existing0,package-import0,reference-port0,unmatched42.
Definition: localisation / ring of fractions
For a multiplicative set S⊆A, a localisation A_S is characterized by a canonical ring map A→A_S taking S to units and initial among ring maps with that property; it is unique up to unique isomorphism.
Formalized. Mathlib/RingTheory/Localization/Defs.lean::IsLocalization, isLocalization_iff, lift, lift_unique; Mathlib/RingTheory/Localization/Basic.lean::algEquiv — IsLocalization is the source localization predicate; lift/lift_unique give the initial mapping property, and algEquiv gives uniqueness up to the canonical algebra isomorphism.
Construction: fractions construction of AS
On A×S set (a,s)∼(b,s′) iff t(s′a−sb)=0 for some t∈S. The equivalence classes a/s form A_S with the usual fraction addition and multiplication, and a↦a/1 is the canonical map.
Formalized. Mathlib/RingTheory/Localization/Defs.lean::Localization M S, mk_eq_of_mk', mk — The canonical Localization S is the quotient-type fraction construction; its mk/mk' API realizes the source numerator-denominator classes and ring operations.
Theorem: kernel and injectivity of localisation
The kernel of A→A_S is {a∈A | sa=0 for some s∈S}; hence the canonical map is injective iff S contains no zero-divisors.
Formalized. Mathlib/RingTheory/Localization/Defs.lean::map_eq_zero_iff, injective, nonZeroDivisors — map_eq_zero_iff gives the annihilation-by-a-denominator kernel. IsLocalization.injective gives injectivity when every denominator is a non-zero-divisor; conversely injectivity plus invertibility of denominators forces the same regularity condition.
Definition: total ring and field of fractions
Localising at the multiplicative set of all non-zero-divisors gives the total ring of fractions. For an integral domain this is its field of fractions.
Formalized. Mathlib/RingTheory/Localization/FractionRing.lean::IsFractionRing, FractionRing — IsFractionRing R K is localization at nonZeroDivisors R; for domains FractionRing R is the field-of-fractions specialization.
Definition: extension and contraction of ideals
For f:A→B, the extension of I⊲A is I^e=IB=f(I)B and the contraction of J⊲B is J^c=f⁻¹(J). One has I{ece}=Ie and J{cec}=Jc, giving a bijection between extended ideals and contracted ideals.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Ideal.map, Ideal.comap, map_comap_map, comap_map_comap — Ideal.map/Ideal.comap are extension and contraction. map_comap_map and comap_map_comap are exactly the ECE/CEC identities, hence identify the images of the two operators.
Lemma: contraction preserves prime and primary ideals
The contraction of a prime ideal is prime. The contraction of a primary ideal is primary.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::comap_isPrime; Mathlib/RingTheory/Ideal/IsPrimary.lean::IsPrimary.comap — Prime ideals contract to prime ideals and primary ideals contract to primary ideals along arbitrary ring homomorphisms.
Definition: primary ideal
A proper ideal J is primary if xy∈J and x∉J imply y^n∈J for some n>0; equivalently every zero-divisor of B/J is nilpotent.
Formalized. Mathlib/RingTheory/Ideal/IsPrimary.lean::isPrimary_iff; Mathlib/RingTheory/IsPrimary.lean::isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul — The elementwise power criterion is the source primary definition, and the quotient theorem identifies it with nilpotence of every zero-divisor on the quotient.
Theorem: Theorem 4.1
Every ideal of A_S is IA_S for an ideal I⊲A. Prime ideals of A_S correspond exactly to prime ideals p⊲A disjoint from S by p↦pA_S; the same extension/contraction statement holds for primary ideals.
Not formalized. Pinned/current Mathlib proves every localized ideal is extended from its contraction (IsLocalization.map_under), gives the exact prime correspondence, and proves contraction-back for a primary ideal disjoint from S. It does not prove that extension of such a primary ideal is primary, so the full prime-and-primary Theorem 4.1 bundle is not credited. Open/current/external search found no exact owner.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: localisation preserves Noetherian and Artinian rings
If A is Noetherian (respectively Artinian), then A_S is Noetherian (respectively Artinian).
Formalized. Mathlib/RingTheory/Localization/Submodule.lean::IsLocalization.isNoetherianRing; Mathlib/RingTheory/Artinian/Ring.lean::localization_artinian — Localization of a Noetherian ring is Noetherian and localization of an Artinian ring is Artinian, with the same source hypotheses.
Example: principal localisation Aa
For a nonnilpotent a, localising at {1,a,a²,…} is denoted A_a; its prime ideals correspond to primes of A not containing a.
Formalized. Mathlib/RingTheory/Localization/Away/Basic.lean::Localization.Away, Submonoid.powers; Mathlib/RingTheory/Localization/Ideal.lean::orderIsoOfPrime — Localization.Away a is localization at powers of a; the prime order isomorphism specializes to primes avoiding a.
Example: local ring Ap
For p∈Spec A, A_p is local with maximal ideal pA_p, and its prime ideals correspond to primes q⊆p of A.
Formalized. Mathlib/RingTheory/Localization/AtPrime/Basic.lean::Localization.AtPrime, primeSpectrumOrderIso, map_eq_maximalIdeal — Localization.AtPrime p is local with maximal ideal the extension of p, and primeSpectrumOrderIso identifies its primes with the interval of primes below p.
Example: localisation at 1+I
For a proper ideal I, S=1+I is multiplicative and primes of A_S correspond to primes p with I+p≠A.
Not formalized. Generic submonoid/localization infrastructure is present, but no pinned/current/open/external declaration packages S={1+i | i∈I} as a submonoid together with the exact prime criterion I+p≠A. The explicit source example is therefore unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: saturation of a multiplicative set
The saturation S~= {a∈A | ab∈S for some b∈A} is multiplicative; A_S=A_{S~}, and S~ is maximal among T with A_T=A_S. Equivalently a∈S~ iff a/1 is a unit in A_S.
Formalized. Mathlib/Algebra/Group/Submonoid/Saturation.lean::Submonoid.saturation, mem_saturation_iff, saturation_le_iff_le; Mathlib/RingTheory/Localization/Defs.lean::algebraMap_isUnit_iff; Mathlib/RingTheory/Localization/Basic.lean::of_le_of_exists_dvd — Submonoid.saturation has membership ∃b, ab∈S; algebraMap_isUnit_iff identifies this with becoming a unit after localization, and the localization recognition theorem gives the same localized ring for saturated denominators.
Theorem: Theorem 4.2
Localisation commutes with quotients: for I⊲A and the image S̄⊆A/I, A_S/IA_S ≅ (A/I)_{S̄}.
Formalized. Mathlib/RingTheory/Localization/Ideal.lean::IsLocalization.of_surjective, Algebra.algebraMapSubmonoid; Mathlib/RingTheory/Localization/Basic.lean::IsLocalization.algEquiv — Pinned Mathlib registers S/IS as a localization of A/I at the image of S via IsLocalization.of_surjective; algEquiv identifies it with the canonical localization, giving A_S/IA_S ≃ (A/I)_{S̄}.
Definition: residue field κ(p)
For p∈Spec A, κ(p)=A_p/pA_p is the residue field of A_p and is canonically the fraction field of A/p.
Formalized. Mathlib/RingTheory/Localization/AtPrime/Basic.lean::equivQuotMaximalIdeal; Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean::IsFractionRing — equivQuotMaximalIdeal identifies the local quotient with A/p, and the residue-field ideal API installs it as a fraction ring of A/p, exactly κ(p).
Theorem: Theorem 4.3
If A→B→A_S satisfies the stated factorisation and denominator condition, then A_S is also a localisation of B: A_S≅B_T, where T consists of elements mapping to units in A_S, equivalently the saturation of the image of S.
Not formalized. Mathlib has generic recognition theorems for localizations and localization-of-localization, but no declaration takes Matsumura’s intermediate ring B with the stated factorization and denominator-clearing hypothesis and concludes A_S ≃ B_T. Current/open/external search found no exact owner.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: Theorem 4.3, Corollary 1
If p∈Spec A, S=A∖p, and B satisfies Theorem 4.3, then for P=pA_p∩B one has A_p≅B_P.
Not formalized. At-prime localization and nested-localization APIs are present, but no declaration realizes the intermediate-ring B from Theorem 4.3 and the contracted prime P under exactly the source hypotheses. The generic localization-at-prime equivalence is not a substitute for the missing B-recognition step.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: Theorem 4.3, Corollary 2
If S contains no zero-divisors and A⊆B⊆A_S, then A_S is a ring of fractions of B.
Not formalized. Pinned Mathlib embeds a localization as a subalgebra of a fraction ring, but no checked declaration proves that every intermediate ring A⊆B⊆A_S is itself a base ring whose localization recovers A_S. Current/open/external searches were negative.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: Theorem 4.3, Corollary 3
For multiplicative subsets S⊆T of A, with T′ the image of T in A_S, one has (A_S)_{T′}≅A_T.
Formalized. Mathlib/RingTheory/Localization/LocalizationLocalization.lean::isLocalization_of_submonoid_le, localization_isScalarTower_of_submonoid_le; Mathlib/RingTheory/Localization/Basic.lean::IsLocalization.algEquiv — For S≤T, Mathlib makes the T-localization a localization of the S-localization at the image of T; the canonical algEquiv is the source (A_S)_{T′} ≃ A_T.
Corollary: Theorem 4.3, Corollary 4
If P is prime and disjoint from S, then (A_S){PA_S}≅A_P; in particular P⊆Q gives (A_Q){PA_Q}≅A_P.
Formalized. Mathlib/RingTheory/Localization/LocalizationLocalization.lean::localizationLocalizationAtPrimeIsoLocalization — The displayed algebra equivalence identifies localization of A_S at a prime with localization of A at its contraction; specializing to PA_S gives (A_S)_{PA_S} ≃ A_P, including P⊆Q.
Definition: spectrum and maximal spectrum
Spec A is the set of prime ideals and m-Spec A the set of maximal ideals.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Defs.lean::structure PrimeSpectrum; Mathlib/RingTheory/Spectrum/Maximal/Defs.lean::structure MaximalSpectrum — PrimeSpectrum A and MaximalSpectrum A are exactly Spec A and m-Spec A.
Construction: Zariski topology on Spec A
For I⊲A, V(I)={p∈Spec A | I⊆p}; the sets V(I) are the closed sets of the Zariski topology. m-Spec A carries the subspace topology.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::zariskiTopology, zeroLocus; Mathlib/RingTheory/Spectrum/Maximal/Topology.lean::zariskiTopology — Prime-spectrum closed sets are zero loci V(I), and the maximal-spectrum topology is induced from the prime spectrum.
Construction: basic open sets D(a)
D(a)=Spec A∖V(aA); every Zariski-open subset is a union of basic opens D(a), so these form a basis.
Formalized. Mathlib/RingTheory/Spectrum/Prime/Topology.lean::basicOpen, isTopologicalBasis_basic_opens, basicOpen_eq_zeroLocus_compl — basicOpen a is D(a), and isTopologicalBasis_basic_opens says these opens form a basis, hence every open is their union.
Construction: contravariant spectrum functor
A ring map f:A→B induces the continuous map Spec B→Spec A, P↦f⁻¹(P), functorially and contravariantly. If f⁻¹(P)=p, P is said to lie over p.
Formalized. Mathlib/RingTheory/Spectrum/Prime/RingHom.lean::PrimeSpectrum.comap, comap_id, comap_comp; Mathlib/RingTheory/Spectrum/Prime/Topology.lean::continuous_comap — PrimeSpectrum.comap f is contraction of prime ideals, continuous for the Zariski topology, and comap_id/comap_comp give the contravariant functorial laws.
Comparison: maximal spectrum is not functorial; point closures
A maximal ideal of B can contract to a nonmaximal prime of A, so m-Spec is not functorial. The closure of {p} in Spec A is V(p), hence {p} is closed iff p is maximal and Spec A is generally not T₁.
Not formalized. Pinned Mathlib proves PrimeSpectrum.closure_singleton and isClosed_singleton_iff_isMaximal, but no checked declaration packages the source comparison showing failure of maximal-spectrum functoriality via a domain embedded in its fraction field. Strict bundle semantics rejects the partial topology-only match.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Construction: localisation of modules
For an A-module M, M_S consists of fractions m/s with the usual equivalence relation; it is an A_S-module. The canonical map M→M_S has kernel {m | sm=0 for some s∈S}; for S=A∖p write M_p.
Formalized. Mathlib/Algebra/Module/LocalizedModule/Basic.lean::LocalizedModule, mkLinearMap, mem_ker_mkLinearMap_iff — LocalizedModule S M is the fraction-module construction and mem_ker_mkLinearMap_iff gives exactly the annihilation-by-a-denominator kernel; prime localization is the prime-complement specialization.
Definition: support of a module
Supp(M)={p∈Spec A | M_p≠0}. If M is finite, Supp(M)=V(ann M), hence is closed.
Formalized. Mathlib/RingTheory/Support.lean::def Module.support, support_eq_zeroLocus — Module.support R M is defined by nontriviality of every prime localization, and for finite M support_eq_zeroLocus identifies it with V(ann M).
Theorem: Theorem 4.4
There is a canonical A_S-linear isomorphism M_S≅M⊗_A A_S.
Formalized. Mathlib/RingTheory/Localization/BaseChange.lean::LocalizedModule.equivTensorProduct — LocalizedModule.equivTensorProduct is the canonical localized-module/tensor-product linear equivalence with the source fraction formula.
Theorem: Theorem 4.5
Localisation M↦M_S is an exact covariant functor from A-modules to A_S-modules.
Formalized. Mathlib/Algebra/Module/LocalizedModule/Basic.lean::LocalizedModule.map, map_id, map_comp; Mathlib/Algebra/Module/LocalizedModule/Exact.lean::LocalizedModule.map_exact — Linear maps localize functorially and exact sequences remain exact, exactly Matsumura Theorem 4.5.
Corollary: localisation commutes with tensor products and Tor
As a consequence of exactness/tensor realization, localisation commutes with tensor products and Tor.
Not formalized. Pinned Mathlib has the exact tensor-localization equivalences and localization exactness, but searches found no declaration stating localization commutes with Tor. Since the source row explicitly bundles tensor products and Tor, the tensor-only match is insufficient.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 4.6
If x∈M maps to 0 in M_m for every maximal ideal m of A, then x=0.
Formalized. Mathlib/RingTheory/LocalProperties/Submodule.lean::Module.eq_zero_of_localization_maximal — Module.eq_zero_of_localization_maximal is exactly the theorem that an element vanishing in every maximal localization is zero.
Theorem: Theorem 4.7
For a domain A with fraction field K, viewed inside K, A=⋂_{m∈m-Spec A} A_m.
Formalized. Mathlib/RingTheory/Spectrum/Maximal/Localization.lean::MaximalSpectrum.iInf_localization_eq_bot — The theorem is explicitly documented as a domain being the intersection of its localizations at all maximal ideals inside its fraction field.
Definition: denominator and numerator ideals of a fraction
For x∈Frac(A), {a∈A | ax∈A} is the denominator ideal of x; its product with x is the numerator ideal.
Not formalized. The denominator ideal appears internally in the proof of the maximal-localization intersection theorem, but no pinned/current/open/external declaration exports Matsumura’s denominator ideal {a | ax∈A} or its numerator ideal xI as reusable objects. Internal proof-local data is not credited.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 4.8
If M is finite and M⊗_A κ(m)=0 for every maximal ideal m, then M=0.
Not formalized. Local Nakayama and IsLocalRing.subsingleton_tensorProduct plus maximal-local detection provide the ingredients, but no checked declaration states the source theorem that a finite module with all maximal residue-field fibres zero is zero. Strict source-shaped mapping therefore leaves the row unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 4.9
For a ring map A→B and a finite B-module M, if M⊗_A κ(p)=0 for every p∈Spec A, then M=0.
Not formalized. Pinned/current Mathlib has fibre, support, localization, and finite-module APIs, but no declaration with a ring map A→B, M finite over B, and vanishing of all A-residue-field fibres implying M=0. Open/current/external search found no exact route.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Counterexample: maximal fibres do not suffice in Theorem 4.9
Theorem 4.9 cannot in general be checked only at maximal ideals of A: for a local domain A with fraction field B and M=B, the fibre over the maximal ideal vanishes although M≠0.
Not formalized. The fraction field and residue-field APIs can express the example, but no checked declaration owns the local-domain/fraction-field counterexample as a reusable theorem or example. Strict example semantics therefore leaves it unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 4.10
For finite M, the locus where M_p is generated by r elements is open. If M is finitely presented, the locus where M_p is free is open.
Not formalized. Pinned Mathlib proves Module.isOpen_freeLocus for finitely presented modules, exactly part (ii), but no declaration was found for openness of the locus where a finite module is generated locally by at most r elements. The two-part source theorem is therefore unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: combinatorial dimension
The combinatorial dimension dim X of a topological space is the supremum of lengths of strict chains of irreducible closed subsets. For a subspace Y⊆X, dim Y≤dim X.
Formalized. Mathlib/Topology/KrullDimension.lean::topologicalKrullDim, topologicalKrullDim_subspace_le — topologicalKrullDim is explicitly the supremum of lengths of chains of irreducible closed subsets, and the subspace theorem gives dim Y≤dim X.
Definition: Krull dimension, height and coheight
dim A is the supremum of lengths of strict chains of prime ideals. For p∈Spec A, ht p is the supremum of descending prime chains from p and coht p the supremum of ascending chains; ht p=dim A_p, coht p=dim A/p, and ht p+coht p≤dim A.
Formalized. Mathlib/RingTheory/KrullDimension/Basic.lean::ringKrullDim; Mathlib/RingTheory/Ideal/Height.lean::Ideal.height, IsLocalization.AtPrime.ringKrullDim_eq_height; Mathlib/RingTheory/KrullDimension/NonZeroDivisors.lean::ringKrullDim_quotient; Mathlib/Order/KrullDimension.lean::krullDim_eq_iSup_height_add_coheight_of_nonempty — Mathlib’s order-theoretic dimension is the prime-chain invariant; Ideal.height is prime height, AtPrime dimension equals height, quotient prime spectra give coheight, and the general height+coheight formula yields the source inequality.
Example: dimension one PIDs
Every PID that is not a field has Krull dimension one.
Formalized. Mathlib/RingTheory/KrullDimension/PID.lean::IsPrincipalIdealRing.ringKrullDim_eq_one — For a domain with principal ideals that is not a field, the pinned theorem states ringKrullDim R = 1 exactly.
Example: Artinian rings have dimension zero
Every Artinian ring has dimension zero: all of its prime ideals are maximal.
Formalized. Mathlib/RingTheory/Artinian/Module.lean::IsArtinianRing.isPrime_iff_isMaximal; Mathlib/RingTheory/HopkinsLevitzki.lean::isArtinianRing_iff_isNoetherianRing_krullDimLE_zero — Every prime of an Artinian ring is maximal and the Hopkins–Levitzki dimension characterization supplies Krull dimension ≤0; for the source nonzero rings this is dimension zero.
Example: zero-dimensional domains are fields
An integral domain of Krull dimension zero is a field.
Formalized. Mathlib/RingTheory/KrullDimension/Zero.lean::Ring.KrullDimLE.isField_of_isDomain — A domain satisfying Krull dimension ≤0 is a field, exactly the source zero-dimensional-domain example.
Example: polynomial-ring prime chain
For a field k, (0)⊂(X₁)⊂⋯⊂(X₁,…,Xₙ) is a prime chain in k[X₁,…,Xₙ], so dim k[X₁,…,Xₙ]≥n.
Not formalized. Pinned Mathlib proves the stronger numerical result MvPolynomial.ringKrullDim_of_isNoetherianRing, but no checked declaration owns the displayed chain (0)⊂(X₁)⊂⋯⊂(X₁,…,Xₙ) as the source example. Strict concrete-example semantics does not replace the chain by a dimension equality.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: height of an ideal
ht I=inf{ht p | p∈Spec A, I⊆p}; one has ht I+dim(A/I)≤dim A.
Not formalized. Ideal.height is defined exactly as the infimum of heights of minimal primes over I and quotient Krull dimension is formalized, but no pinned/current/open/external declaration states the full arbitrary-ideal inequality ht I + dim(A/I) ≤ dim A. The definition alone does not cover the bundled inequality.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: dimension of a module
dim M:=dim(A/ann M). If M is finite, this is the combinatorial dimension of Supp(M)=V(ann M).
Formalized. Mathlib/RingTheory/KrullDimension/Module.lean::Module.supportDim, supportDim_eq_ringKrullDim_quotient_annihilator; Mathlib/RingTheory/Support.lean::support_eq_zeroLocus — The source quotient dimension is ringKrullDim (A ⧸ ann M); for finite M Mathlib proves it equals the Krull dimension of Supp M, while support_eq_zeroLocus identifies that support with V(ann M).
Definition: saturated prime chain and catenary ring
A prime chain is saturated if no prime lies strictly between consecutive terms. A ring is catenary if for every p⊂p′ there are saturated chains from p to p′ and all such chains have the same finite length.
Not formalized. Pinned/current Mathlib has chain/height infrastructure but no Catenary/IsCatenary declaration matching Matsumura’s saturated-chain definition. Open PRs mentioning catenarity do not supply a compatible pinned/importable route for this source unit.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Criterion: catenary dimension equality
In a catenary local domain, ht p+coht p=dim A for every p. Conversely, for a Noetherian local domain, this equality for all p implies catenarity (proved later as Theorem 31.4).
Not formalized. The source equivalence depends on a catenary-ring predicate not present at P/H, and targeted open/external search found no compatible declaration for the local-domain height+coheight criterion. Later specialized Cohen–Macaulay catenarity work does not match this bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 5.1
If L/k is algebraic and α₁,…,αₙ∈L, then k[α₁,…,αₙ]=k(α₁,…,αₙ). The kernel of k[X₁,…,Xₙ]→k(α₁,…,αₙ) can be generated by n polynomials f_i(X₁,…,X_i), each monic in X_i.
Not formalized. Pinned/current Mathlib formalizes algebraic and integral finite extensions and minimal polynomials, but no checked declaration gives the finite tower k[α₁,…,αₙ]=k(α₁,…,αₙ) together with an n-generator kernel by triangular polynomials monic in successive variables. The full bundle remains unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 5.2
If A=k[α₁,…,αₙ] is a finite-type domain over a field and trdeg_k A>0, then A is not a field.
Formalized. Mathlib/RingTheory/Jacobson/Ring.lean::finite_of_finite_type_of_isJacobsonRing; Mathlib/RingTheory/AlgebraicIndependent/Transcendental.lean::trdeg_eq_zero_iff — If a finite-type k-domain were a field, Zariski’s lemma makes it finite/algebraic over k, and trdeg_eq_zero_iff forces transcendence degree zero. Contraposition gives Matsumura Theorem 5.2.
Theorem: Theorem 5.3
For a maximal ideal m⊂k[X₁,…,Xₙ], the residue field is algebraic over k and m is generated by n elements. If k is algebraically closed, m=(X₁−a₁,…,Xₙ−aₙ).
Not formalized. Pinned Mathlib has Zariski’s lemma for the residue-field algebraicity clause and, over an algebraically closed field, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton. No declaration was found for the arbitrary-field assertion that every maximal ideal of k[X₁,…,Xₙ] is generated by n elements, so the whole source theorem is unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: algebraic zero
For Φ⊆k[X₁,…,Xₙ] and an algebraic closure k̄, a tuple a∈k̄ⁿ is an algebraic zero of Φ when f(a)=0 for every f∈Φ.
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::zeroLocus, zeroLocus_span — MvPolynomial.zeroLocus over an extension field is exactly the set of tuples at which every polynomial of the chosen set/ideal vanishes; zeroLocus_span passes between a set Φ and its generated ideal.
Theorem: Theorem 5.4 (Hilbert Nullstellensatz)
If Φ⊆k[X₁,…,Xₙ] has no algebraic zero, then (Φ)=(1). More generally, if f vanishes at every algebraic zero of Φ, then f^ν∈(Φ) for some ν>0.
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::vanishingIdeal_zeroLocus_eq_radical, zeroLocus_span, mem_vanishingIdeal_iff — The theorem is stated for a coefficient field k and an algebraically closed extension K. Combined with zeroLocus_span, it gives both no-zero⇒(Φ)=1 and vanishing-on-all-zeros⇒membership in √(Φ), equivalently some positive power lies in (Φ).
Theorem: Theorem 5.5
If A is a finite-type algebra over a field and I is proper, then √I is the intersection of all maximal ideals containing I.
Formalized. Mathlib/RingTheory/Jacobson/Ring.lean::isJacobsonRing_of_finiteType, Ideal.radical_eq_jacobson — A field is Jacobson, finite-type algebras over it are Jacobson, and in a Jacobson ring radical I = jacobson I, i.e. the intersection of maximal ideals containing I.
Definition: Hilbert / Jacobson ring
A ring is Hilbert (Jacobson) if every prime ideal is an intersection of maximal ideals.
Formalized. Mathlib/RingTheory/Jacobson/Ring.lean::IsJacobsonRing, isJacobsonRing_iff_sInf_maximal — IsJacobsonRing is equivalent to every prime ideal being the infimum/intersection of maximal ideals above it, exactly Matsumura’s Hilbert-ring definition.
Theorem: Theorem 5.6
For a finite-type integral domain A over a field k, dim A=trdeg_k A.
Not formalized. Pinned/current Mathlib defines both Krull dimension and algebraic transcendence degree, but searches found no theorem identifying them for an arbitrary finite-type integral domain over a field. Project AffineVarietyDimension defines the transcendence-degree side only and does not close this equality. No current/open/external exact owner was found.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: dimension of polynomial rings over fields
For a field k, dim k[X₁,…,Xₙ]=n.
Formalized. Mathlib/RingTheory/KrullDimension/Polynomial.lean::MvPolynomial.ringKrullDim_of_isNoetherianRing; Mathlib/RingTheory/KrullDimension/Field.lean::ringKrullDim_eq_zero_of_field — For finite variable type, polynomial Krull dimension is base dimension plus the number of variables; over a field this is exactly n.
Definition: local number of generators μ(p,M)
For finite M and p∈Spec A, μ(p,M)=dim_{κ(p)}(M⊗κ(p)) is the cardinality of a minimal basis of M_p; if p⊇p′ then μ(p,M)≥μ(p′,M).
Not formalized. Pinned Mathlib has Ideal.Fiber, TensorProduct.spanFinrank_top_eq_of_residueField, and base-change monotonicity of spanFinrank, which are the correct ingredients for μ(p,M). No checked declaration packages Matsumura’s μ(p,M) definition together with minimal-generator identification and specialization monotonicity p⊇p′. Under strict whole-row semantics the assembled ingredients are not credited as an existing source-shaped interface.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 5.7 (Forster)
For Noetherian A and finite M, setting b(M)=sup{μ(p,M)+coht p | p∈Supp M}, M is generated by at most b(M) elements.
Not formalized. Pinned/current Mathlib, open PRs, Loogle/LeanSearch, Reservoir, and indexed Lean repositories produced no compatible theorem for the Forster bound sup(μ(p,M)+coht p).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: j-prime and j-Spec
A j-prime is a prime ideal expressible as an intersection of maximal ideals; j-Spec A is the set of j-primes with the subspace topology from Spec A.
Not formalized. No pinned/current/open/external Lean declaration was found for Swan’s j-prime ideals or the j-Spec subspace. Jacobson-ring APIs are related but define a property of the whole ring, not Matsumura’s j-Spec for an arbitrary ring.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: closed and irreducible subsets of j-Spec
Closed subsets of j-Spec correspond naturally to closed subsets of m-Spec. If m-Spec is Noetherian then so is j-Spec and they have the same combinatorial dimension. Every irreducible closed subset of j-Spec has a unique generic point P, and equals V(P)∩j-Spec.
Not formalized. Because no j-Spec object is formalized in the searched compatible sources, the closed-set correspondence, Noetherian/dimension comparison, and generic-point theorem have no exact route.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: j-dimension and Swan local bound b(p,M)
For P∈j-Spec, j-dim P is dim(V(P)∩j-Spec). For finite M, set b(P,M)=0 when M_P=0 and otherwise j-dim P+μ(P,M).
Not formalized. No compatible declaration defines j-dimension or the local Swan bound b(p,M); generic topological Krull dimension and fibre finrank APIs do not supply the j-Spec-specific object.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 5.8 (Swan)
If m-Spec A is Noetherian, M is finite, and r=sup{b(p,M) | p∈j-Spec A}<∞, then M is generated by at most r elements.
Not formalized. Searches of pinned/current Mathlib, open PRs, LeanSearch/Loogle, Reservoir, and discoverable Lean repositories found no theorem matching Matsumura’s j-Spec Swan bound.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: basic element at a prime
For p∈Spec A and x∈M, x is basic at p if its image in M⊗κ(p) is nonzero; equivalently μ(p,M/Ax)=μ(p,M)−1.
Not formalized. Nonzero residue-field fibres, quotient modules, and generator-rank APIs are available, but no checked declaration defines Matsumura’s “basic at p” predicate together with the exact decrement identity μ(p,M/Ax)=μ(p,M)−1.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Lemma: simultaneously basic element
If M is finite and p₁,…,pₙ∈Supp(M), there exists x∈M basic at every p_i.
Not formalized. No pinned/current/open/external declaration was found asserting existence of one element basic at finitely many prescribed primes in Supp(M).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Swan noncommutative generator bound
Let A be commutative, Λ an A-algebra not necessarily commutative, and M a finite left Λ-module. If m-Spec A is Noetherian and every M_p needs at most r Λ_p-generators, then M needs at most r+d Λ-generators, where d=dim(m-Spec A).
Not formalized. No compatible Lean declaration was found for the stated noncommutative A-algebra generalization with r+d generators. The commutative generator-rank infrastructure is strictly weaker.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: associated primes and prime divisors
P∈Spec A is associated to M if P=ann(x) for some x∈M; Ass_A(M) is the set of associated primes. Associated primes of A/I are called prime divisors of I.
Not formalized. Mathlib defines IsAssociatedPrime I M generally using the radical of an element annihilator. Matsumura defines P=ann(x) exactly for arbitrary rings. Mathlib proves the definitions equivalent under IsNoetherianRing, but U066 itself has no Noetherian hypothesis, so the general Mathlib predicate is not an exact match.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: zero-divisor and regular element on a module
a∈A is a zero-divisor for M if ax=0 for some nonzero x∈M; otherwise a is M-regular.
Formalized. Mathlib/RingTheory/Regular/IsSMulRegular.lean::IsSMulRegular, isSMulRegular_iff_right_eq_zero_of_smul — IsSMulRegular M a is exactly injectivity of multiplication by a on M, i.e. a is M-regular; its negation is the source zero-divisor condition.
Theorem: Theorem 6.1
For a nonzero module over a Noetherian ring, every maximal annihilator ann(x) is associated, so Ass(M) is nonempty; the set of zero-divisors on M is exactly ⋃_{P∈Ass(M)}P.
Formalized. Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean::isAssociatedPrime_iff, associatedPrimes.nonempty, biUnion_associatedPrimes_eq_zero_divisors, exists_le_isAssociatedPrime_of_isNoetherianRing — Under the source Noetherian hypothesis isAssociatedPrime_iff removes Mathlib’s radical and recovers exact annihilators. Maximal annihilators are therefore associated, associatedPrimes.nonempty gives nonemptiness, and the union theorem is exactly the zero-divisor statement.
Theorem: Theorem 6.2
For S⊆A multiplicative and an A_S-module N, associated primes over A_S correspond to the associated primes over A under contraction. If A is Noetherian, Ass(M_S)=Ass(M)∩Spec(A_S), under the standard identification of primes disjoint from S.
Not formalized. Mathlib has strong localization theorems for its radical-based associated-prime predicate and under Noetherianity they agree with Matsumura. The first clause of Matsumura 6.2 is for arbitrary A and exact annihilator-associated primes, so the full row cannot be credited from the weaker/different general predicate; the Noetherian second clause is only a partial match.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Corollary: associated primes after localisation at p
For Noetherian A, M an A-module and p∈Spec A, Ass_{A_p}(M_p) consists exactly of qA_p with q∈Ass_A(M) and q⊆p.
Formalized. Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean::preimage_comap_associatedPrimes_eq_associatedPrimes_of_isLocalizedModule, mem_associatedPrimes_atPrime_of_mem_associatedPrimes; Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean::isAssociatedPrime_iff — Under Noetherianity Mathlib’s associated-prime predicate is Matsumura’s exact annihilator predicate, and the localization theorem identifies precisely the primes below p with the associated primes after localizing at p.
Theorem: Theorem 6.3
For an exact sequence 0→M′→M→M″→0, Ass(M)⊆Ass(M′)∪Ass(M″).
Not formalized. Pinned Mathlib proves associatedPrimes.subset_union_of_exact for its radical-based general associated-prime predicate. Without Noetherianity that conclusion does not recover Matsumura’s exact-annihilator definition, so the arbitrary-ring source theorem remains unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 6.4
A nonzero finite module over a Noetherian ring admits a finite filtration 0=M₀⊂⋯⊂M_r=M whose successive quotients are A/P_i for prime ideals P_i.
Formalized. Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean::IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime — The theorem is explicitly a finite chain from 0 to M whose successive quotients are linearly equivalent to A/p_i for prime ideals p_i, exactly Matsumura 6.4.
Theorem: Theorem 6.5
For finite M over Noetherian A, Ass(M) is finite, Ass(M)⊆Supp(M), and the minimal elements of Ass(M) and Supp(M) coincide.
Formalized. Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean::associatedPrimes.finite; Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean::minimalPrimes_annihilator_subset_associatedPrimes; Mathlib/RingTheory/Ideal/AssociatedPrime/Basic.lean::isAssociatedPrime_iff_exists_injective_linearMap; Mathlib/RingTheory/Support.lean::support_eq_zeroLocus; Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean::exists_minimalPrimes_le — Finiteness is direct. An associated prime embeds A/P in M and hence lies in support; minimal primes over ann(M) lie in Ass(M), while support_eq_zeroLocus identifies them with the minimal support points. Together these give Ass⊆Supp and equality of the two minimal sets.
Definition: isolated and embedded associated primes
For finite M over Noetherian A, the minimal elements of Supp(M) are the isolated associated primes; the remaining associated primes are embedded. For I⊲A, minimal prime divisors of I are exactly the minimal primes containing I.
Formalized. Mathlib/RingTheory/Ideal/AssociatedPrime/Finiteness.lean::associatedPrimes.finite; Mathlib/RingTheory/Ideal/AssociatedPrime/Localization.lean::minimalPrimes_annihilator_subset_associatedPrimes; Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean::minimalPrimes — With U073’s pinned identifications, isolated associated primes are exactly the minimal elements of Ass/Support and embedded primes are the remaining associated primes; for A/I these minimal associated primes are precisely minimal primes over I.
Definition: primary submodule
N⊂M is primary if x∉N and ax∈N imply a^νM⊆N for some ν>0; equivalently every zero-divisor on M/N lies in √ann(M/N). Primary ideals are the case M=A.
Formalized. Mathlib/RingTheory/IsPrimary.lean::Submodule.IsPrimary, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul — Mathlib’s primary-submodule predicate is literally the Matsumura condition x∉N, ax∈N ⇒ ∃n, a^n⊤≤N; the quotient theorem gives the equivalent nilpotent zero-divisor formulation.
Theorem: Theorem 6.6
For finite M over Noetherian A, N is primary iff Ass(M/N) is a singleton {P}. In that case ann(M/N) is primary and its radical is P.
Not formalized. Pinned Mathlib has primary submodules, Noetherian associated-prime equivalence, and Lasker decompositions, so the theorem is derivable. However, no checked declaration states the full iff N primary ↔︎ Ass(M/N)={P} together with primary annihilator and radical P; current/open/external search found no source-shaped owner, so strict mapping leaves the row unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: P-primary submodule
If Ass(M/N)={P}, N is called P-primary, or primary belonging to P.
Not formalized. Mathlib can express a primary submodule with a specified radical of its colon, but no checked declaration packages Matsumura’s source definition “Ass(M/N)={P}” as a P-primary submodule notion. The missing U076 bridge prevents treating the alternative presentation as an exact existing route.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 6.7
The intersection of two P-primary submodules of the same module is P-primary.
Formalized. Mathlib/RingTheory/IsPrimary.lean::IsPrimary.inf, isPrimary_finsetInf — Submodule.IsPrimary.inf says the intersection of primary submodules with equal radical colon is primary with that same radical, exactly the P-primary intersection theorem after the standard Noetherian identification.
Definition: reducible and irreducible submodule
A submodule N⊂M is reducible if N=N₁∩N₂ with both N_i strictly larger than N; otherwise it is irreducible.
Formalized. Mathlib/Order/Irreducible.lean::InfIrred, not_infIrred — For the submodule lattice, InfIrred N says N is not maximal/top and N=N₁⊓N₂ forces one factor to equal N; not_infIrred gives exactly the reducible decomposition by two strict supersubmodules.
Theorem: finite irreducible decompositions in Noetherian modules
Every submodule of a Noetherian module is a finite intersection of irreducible submodules.
Formalized. Mathlib/Order/Irreducible.lean::exists_infIrred_decomposition; Mathlib/RingTheory/Noetherian/Defs.lean::isNoetherian_iff — Noetherianity makes the submodule lattice well-founded upward, and exists_infIrred_decomposition expresses every submodule as a finite infimum/intersection of irreducible submodules.
Definition: decompositions and primary components
A finite intersection expression of N is a decomposition; it may be irredundant, irreducible, or primary. Grouping equal associated primes in an irredundant primary decomposition gives a shortest primary decomposition; its factors are the primary components, including the P-primary component terminology.
Formalized. Mathlib/RingTheory/Lasker.lean::IsMinimalPrimaryDecomposition, exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition — IsMinimalPrimaryDecomposition records finite intersection equality, primary components, distinct component radicals, and irredundancy; the reduction theorem groups/reduces any primary decomposition to this shortest form.
Theorem: Theorem 6.8 (primary decomposition)
For finite M over Noetherian A: every irreducible submodule is primary; in an irredundant primary decomposition N=⋂N_i with Ass(M/N_i)={P_i}, Ass(M/N)={P_i}; every proper N has a primary decomposition; and for a minimal associated prime P of M/N, the P-primary component is the inverse image of N_P in M and is uniquely determined.
Formalized. Mathlib/RingTheory/Lasker.lean::InfIrred.isPrimary, Submodule.isLasker, image_radical_eq_associated_primes, comap_localized₀_eq_iInf — Pinned Mathlib proves irreducible⇒primary and that every submodule of a Noetherian module has a primary decomposition. Minimal-decomposition radicals are exactly associated primes, and the localization-comap uniqueness theorem specializes to a singleton minimal associated prime to give the canonical P-primary component.
Definition: secondary and P-secondary module
A nonzero A-module M is secondary if for every a∈A, multiplication by a on M is either surjective or nilpotent. Then P=√ann(M) is prime and M is P-secondary; every nonzero quotient of a P-secondary module is P-secondary.
Not formalized. No pinned/current/open/external declaration defines Matsumura/Macdonald secondary or P-secondary modules with the surjective-or-nilpotent scalar action and radical-annihilator prime statement.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Example: secondary-module examples
The fraction field of a domain is (0)-secondary; Z[p⁻¹]/Z is (0)-secondary; if (A,P) is local and every element of P is nilpotent then A is P-secondary; for maximal P, A/Pⁿ is P-secondary.
Not formalized. Because the compatible searched libraries have no secondary-module predicate, none owns the four displayed source examples as secondary-module theorems. Adjacent fraction-field, Prüfer-group, local-ring, and quotient APIs are insufficient.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: secondary representation and minimality
A secondary representation is M=N₁+⋯+N_r with each N_i secondary. It is minimal if the primes √ann(N_i) are distinct and no summand is redundant; sums of P-secondary submodules are P-secondary, so every secondary representation can be made minimal.
Not formalized. No compatible declaration defines a finite sum of secondary submodules as a secondary representation or packages its minimality and equal-prime merging theorem.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: attached prime
P is attached to M if M has a P-secondary quotient; Att(M) denotes the set of attached primes.
Not formalized. Searches found no compatible Att(M)/attached-prime notion defined through P-secondary quotients. Incidental occurrences of the words “attached prime” in downstream repositories were not this commutative-algebra interface.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 6.9
If M=N₁+⋯+N_r is a minimal secondary representation and P_i=√ann(N_i), then Att(M)={P₁,…,P_r}.
Not formalized. No pinned/current/open/external declaration formalizes minimal secondary representations or proves that their component primes equal the attached primes.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 6.10
For an exact sequence 0→M′→M→M″→0, Att(M″)⊆Att(M)⊆Att(M′)∪Att(M″).
Not formalized. No compatible attached-prime API exists in the searched libraries, so the exact-sequence inclusions of Matsumura 6.10 have no route.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Definition: sum-irreducible module
M is sum-irreducible if it is nonzero and cannot be expressed as a sum of two proper submodules.
Formalized. Mathlib/Order/Irreducible.lean::SupIrred, not_supIrred — For submodules, SupIrred ⊤ says the whole module is nonzero and cannot be the sum/supremum of two proper submodules, exactly Matsumura’s sum-irreducible definition.
Lemma: Artinian sum-irreducible modules are secondary
Every Artinian sum-irreducible module is secondary.
Not formalized. The sum-irreducible side is expressible as SupIrred ⊤, but no compatible secondary-module predicate/theorem exists, so the lemma cannot be assigned an exact route.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Theorem 6.11
Every Artinian module has a secondary representation.
Not formalized. No pinned/current/open/external declaration formalizes secondary representations, hence no theorem states that every Artinian module has one.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07
Theorem: Sharp secondary-representation theorem
Every injective module over a Noetherian ring has a secondary representation (Sharp).
Not formalized. Targeted searches found no Lean formalization of Sharp’s theorem that every injective module over a Noetherian ring has a secondary representation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=f15b4f161f6ff698ab91b4494faa75925856d0f5; open/external search 2026-09-07