Chapter 5. Dimension theory
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 17 definitions, 32 theorems, 1 lemma, 2 corollaries, 4 examples, 1 counterexample, 7 constructions, 1 remark and 1 formula.
Of the 66 statements checked against Lean, 11 are formalized somewhere and 55 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 55 | 83% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 6 | 9% | Mathlib states and proves it. |
| in another Lean project | 4 | 6% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 1 | 2% | This repository states and proves it. |
| checked in total | 66 |
- Canonical source block: FC13 Matsumura Chapter 5,
FC13-C05-U001–FC13-C05-U066, §§13–15 and the appendix to §13, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves the promoted catalogue throughagent-memory, asserts all 66 IDs occur once and in order, and emits one route per source unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280(Lean 4.33.0, Apache-2.0).LeanCategories/Algebra/DimensionTheory.leanownsPoincareSeries,HilbertFunction,IsSystemOfParameters, andAffineVarietyDimension. Only U009 is wholly owned by that interface; U028 includes a module-level parameter definition absent from the project, so it is not classified project-existing. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Apache-2.0, Lean 4.33.0. Every native path/token is validated against that exact checkout. Native C05 coverage is concentrated in graded-ring/homogeneous-submodule infrastructure, Krull height, regular-local embedding dimension, fibre rings, and the height/fibre inequality with going-down equality. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493(Lean 4.34.0-rc2). The associated-graded work remains open in PRs #33218–#33220 and is definition-level only for the source bundles here. Mathlib PR #9819, head413e5b872a7c758e0eb91f99cb96d6a61c81f0a2, is an older Apache-2.0 branch on Lean 4.9.0-rc3 that contains the graded Hilbert-basis, finite-piece, Hilbert–Serre and Hilbert-polynomial results. Those four exact semantic owners are recorded asreference-port, not importable package routes. - Search channels used project source, P, current/open Mathlib, Mathlib source/docs, Loogle/LeanSearch-oriented repository tooling, Reservoir/indexed discovery, and GitHub-wide Lean-code search. Targeted searches for Hilbert–Samuel, systems of parameters, analytic independence, catenarity, and dimension formula found no complete compatible owner beyond the project/PRs already recorded.
- Strict bundle semantics were enforced. U003/U004 are not credited from homogeneous/weighted polynomial APIs because pinned quotient grading is missing; U005/U006/U014 are not credited from associated-graded definitions without completion/generation/finiteness theorems; U028 is not credited from the project ring-only parameter predicate; U056 is not credited from polynomial dimension without the formal-power-series equality; and U063–U066 are not credited from
ReesAlgebrawithout the associated-graded/deformation/dimension clauses. - Hilbert polynomial and Hilbert–Samuel polynomial are kept distinct. PR #9819 supplies the former for graded modules (U010–U011) but not the Samuel function, d(M), multiplicity, reductions, or the §14 formulas. U015–U018 and U039–U051 therefore remain unmatched rather than being mapped through a superficially similar polynomial API.
- Route totals for C05:
mathlib6,project-existing1,package-import0,reference-port4,unmatched55.
Definition: graded rings, graded modules and homogeneous elements
For an abelian semigroup G with identity, a G-graded ring is a direct sum R=⊕{i∈G}R_i with R_iR_j⊆R{i+j}; a graded module is M=⊕M_i with R_iM_j⊆M_{i+j}. Elements in a single M_i are homogeneous of degree i, and every element has unique homogeneous terms.
Formalized. Mathlib/RingTheory/GradedAlgebra/Basic.lean::GradedRing; Mathlib/Algebra/DirectSum/Decomposition.lean::Decomposition; Mathlib/Algebra/GradedMulAction.lean::SetLike.GradedSMul — GradedRing is a direct-sum decomposition with graded multiplication; a module decomposition together with GradedSMul gives the graded module condition, and DirectSum.Decomposition supplies unique homogeneous components.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: homogeneous submodule
A submodule N of a graded module M is homogeneous if generated by homogeneous elements; equivalently every homogeneous term of every x∈N lies in N, equivalently N=⊕(N∩M_i).
Formalized. Mathlib/RingTheory/GradedAlgebra/Homogeneous/Submodule.lean::HomogeneousSubmodule, Submodule.IsHomogeneous.mem_iff — HomogeneousSubmodule bundles a submodule generated/componentwise stable under homogeneous pieces; mem_iff is exactly the criterion that every homogeneous component of x lies in N.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Construction: graded quotients and the irrelevant ideal
For homogeneous N, M/N inherits the grading (M/N)i=M_i/(N∩M_i). For an N-graded ring, R+=⊕{n>0}R_n is an ideal and R/R+≅R_0.
Not formalized. Pinned P defines homogeneous submodules and the irrelevant homogeneous ideal, but no quotient-grading constructor for M/N was found. Since the source row bundles quotient grading with the irrelevant-ideal quotient R/R_+≃R_0, the partial irrelevant-ideal API is insufficient.
Example: standard, multigraded and weighted polynomial gradings
Polynomial rings admit total-degree, multidegree, and weighted N-gradings; weighted homogeneous quotients inherit the grading.
Not formalized. Pinned Mathlib has total/multidegree/weighted homogeneous polynomial APIs (MvPolynomial.weightedHomogeneousSubmodule and decomposition), but no pinned homogeneous-quotient grading. The explicit quotient-inherits-grading clause keeps the whole source example unmatched.
Definition: filtration and associated graded ring
A filtration A=J_0⊇J_1⊇⋯ with J_iJ_j⊆J_{i+j} defines gr(A)=⊕{n≥0}J_n/J{n+1}; a completion for the filtration has canonically the same associated graded ring.
Construction: I-adic associated graded ring
For I⊲A, gr_I(A)=⊕_{n≥0}In/I{n+1}; it is generated over A/I by I/I², and if I=(x_1,…,x_r) it is a graded quotient of (A/I)[X_1,…,X_r].
Not formalized. The adic filtration and open associated-graded PRs supply ingredients, but no pinned/current/open declaration proves the complete bundle gr_I(A)=⊕I^n/I^{n+1}, generation over A/I by I/I², and the graded polynomial quotient for finite generators.
Theorem: Theorem 13.1
An N-graded ring R is Noetherian iff R_0 is Noetherian and R is finitely generated as an R_0-algebra by homogeneous elements of positive degree.
Formalized. Mathlib/RingTheory/GradedAlgebra/Noetherian.lean::GradeZero.subring_isNoetherianRing_of_isNoetherianRing, finite_algebra_over_degree_zero_subring — PR #9819 proves the difficult forward direction: a Noetherian N-graded ring has Noetherian degree zero and is finite type over it via homogeneous positive-degree generators. The reverse direction is standard finite-type Noetherianity. PR head is Apache-2.0 Mathlib on Lean 4.9.0-rc3, so it is a reference to port, not an import route.
Searched: leanprover-community/mathlib4 PR #9819 head=413e5b872a7c758e0eb91f99cb96d6a61c81f0a2
Corollary: graded pieces of finite graded modules
If R is Noetherian graded and M is a finite graded R-module, then every M_n is a finite R_0-module.
Formalized. Mathlib/RingTheory/GradedAlgebra/Noetherian.lean::finite_module_over_degree_zero_subring — PR #9819 proves every graded piece of a finite graded module over the source Noetherian graded ring is finite over degree zero, exactly the corollary. Old Lean 4.9.0-rc3 toolchain makes this a porting reference.
Searched: leanprover-community/mathlib4 PR #9819 head=413e5b872a7c758e0eb91f99cb96d6a61c81f0a2
Definition: Hilbert series
If R_0 is Artinian and M is finite graded, define P(M,t)=Σ_{n≥0} length_{R_0}(M_n)t^n.
Formalized. LeanCategories/Algebra/DimensionTheory.lean::LeanCategories.Algebra.PoincareSeries — The project forms the power series with coefficient λ(M_n). Taking λ to be module length over the Artinian degree-zero ring gives exactly Matsumura’s Hilbert series definition.
Searched: repo HEAD=3b2239e161592472b34e02ad3b7da308f9ce7280
Theorem: Theorem 13.2
If R is Noetherian graded with R_0 Artinian, M finite graded, and R=R_0[x_1,…,x_r] with deg x_i=d_i, then P(M,t)=f(t)/∏_i(1-t^{d_i}) for some f(t)∈Z[t].
Formalized. Mathlib/Algebra/HilbertSerre/Theorem.lean::hilbert_serre — PR #9819 proves the Poincare series equals a polynomial numerator times the inverse product of (1-X^{d_i}), exactly Theorem 13.2 for an additive function such as length.
Searched: leanprover-community/mathlib4 PR #9819 head=413e5b872a7c758e0eb91f99cb96d6a61c81f0a2
Corollary: Hilbert polynomial for standard graded modules
When all d_i=1, there is a rational polynomial φ_M(X) of degree d-1 agreeing with n↦length(M_n) for all sufficiently large n; φ_M is the Hilbert polynomial and the numerical function n↦length(M_n) the Hilbert function.
Formalized. Mathlib/Algebra/HilbertSerre/HilbertPolynomial.lean::hilbertPolynomial, AdditiveFunction_eq_hilbertPolynomial_eval, exists_unique_hilbertPolynomial, natDegree_hilbertPolynomial — Under degree-one homogeneous generators, PR #9819 constructs the unique rational Hilbert polynomial and proves eventual agreement with the graded-piece additive function, including its degree formula. This is the source standard-graded Hilbert-polynomial interface.
Searched: leanprover-community/mathlib4 PR #9819 head=413e5b872a7c758e0eb91f99cb96d6a61c81f0a2
Examples: Hilbert functions of polynomial rings and hypersurfaces
The source computes Hilbert functions/polynomials for a polynomial ring, for a homogeneous hypersurface, and for a standard graded domain, relating the growth degree to transcendence degree.
Not formalized. The graded-polynomial and Hilbert-series ingredients exist (including PR #9819), but no checked declaration owns all three source computations for polynomial rings, hypersurfaces, and standard graded domains with the stated transcendence-degree comparison.
Definition: ideal of definition in a semilocal ring
For Noetherian semilocal A with Jacobson radical m, an ideal I with m^ν⊆I⊆m for some ν>0 is an ideal of definition; its I-adic topology equals the m-adic topology.
Not formalized. Pinned/project adic and Jacobson-radical APIs can express the condition m^ν≤I≤m and cofinal adic topologies, but no checked source-shaped declaration packages Matsumura’s semilocal ideal-of-definition definition and topology theorem.
Construction: associated graded module for an ideal of definition
For finite M and ideal of definition I, gr_I(M)=⊕_{n≥0}InM/I{n+1}M is a finite graded module over gr_I(A).
Not formalized. Open associated-graded PR #33220 defines generic graded pieces/modules but does not prove that gr_I(M) is finite over gr_I(A) for a finite module and ideal of definition. No complete compatible owner was found.
Definition: Samuel function and d(M)
χ_IM(n)=length(M/I{n+1}M) is the Samuel function. For n≫0 it is polynomial, and its degree d(M) is independent of the ideal of definition.
Not formalized. Pinned/current Mathlib and external search do not provide the Hilbert–Samuel polynomial invariant required by this unit. PR #9819 concerns graded Hilbert polynomials, not Samuel functions of adic quotients, so it does not close this source statement.
Theorem: Theorem 13.3
For an exact sequence 0→M′→M→M″→0 of finite modules over a semilocal Noetherian ring, d(M)=max(d(M′),d(M″)); for any ideal of definition, the Samuel polynomials of M′ and the correction term in M have the same leading coefficient.
Not formalized. Pinned/current Mathlib and external search do not provide the Hilbert–Samuel polynomial invariant required by this unit. PR #9819 concerns graded Hilbert polynomials, not Samuel functions of adic quotients, so it does not close this source statement.
Definition: δ(M)
δ(M) is the least n for which there exist x_1,…,x_n in the Jacobson radical with length(M/(x_1,…,x_n)M)<∞; if length(M)<∞ set δ(M)=0.
Not formalized. Pinned/current Mathlib and external search do not provide the Hilbert–Samuel polynomial invariant required by this unit. PR #9819 concerns graded Hilbert polynomials, not Samuel functions of adic quotients, so it does not close this source statement.
Theorem: Theorem 13.4
For a finite module M over a semilocal Noetherian ring, dim M=d(M)=δ(M).
Not formalized. Pinned/current Mathlib and external search do not provide the Hilbert–Samuel polynomial invariant required by this unit. PR #9819 concerns graded Hilbert polynomials, not Samuel functions of adic quotients, so it does not close this source statement.
Theorem: Theorem 13.5 (principal ideal / height theorem)
If I=(a_1,…,a_r) in a Noetherian ring and p is a minimal prime over I, then ht p≤r. Hence every proper ideal has finite height; the r=1 case is Krull’s principal ideal theorem.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::Ideal.height_le_card_of_mem_minimalPrimes_span_finset, Ideal.finiteHeight_of_isNoetherianRing, Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes — A prime minimal over an r-generated ideal has height at most r; every ideal in a Noetherian ring has finite height; the principal specialization gives the height-one theorem.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 13.6
If P is prime of height r in a Noetherian ring, then P is minimal over an r-generated ideal; quotienting P by s elements of P leaves height at least r-s; for a suitable r-tuple a_1,…,a_r, the successive quotient heights are exactly r-i.
Not formalized. Pinned Mathlib has Ideal.exists_finset_card_eq_height_of_isNoetherianRing and quotient height bounds, covering the first two numerical ingredients. No checked declaration supplies the final suitably ordered r-tuple with every successive quotient height exactly r-i, so the whole theorem remains unmatched.
Theorem: Theorem 13.7
In a Noetherian graded ring, every prime divisor of a homogeneous ideal is homogeneous; every homogeneous prime P of finite height r admits a saturated chain of homogeneous primes of length r.
Not formalized. Homogeneous ideals and Noetherian graded rings are formalized, but searches found no theorem that every prime divisor of a homogeneous ideal is homogeneous together with the saturated homogeneous-prime chain of prescribed height.
Theorem: Theorem 13.8
For a standard graded k-algebra R=k[ξ_1,…,ξ_s], with irrelevant maximal ideal M and local ring A=R_M: the Hilbert and Samuel functions satisfy φ(n)=χ(n)-χ(n-1); dim R=ht M=dim A=deg φ+1; and gr_m(A)≅R.
Not formalized. This theorem depends simultaneously on the missing Samuel polynomial and associated-graded local-ring comparison. The graded Hilbert polynomial reference port does not establish the full φ/χ/dimension/gr_m(A) bundle.
Theorem: Theorem 13.9
For a Noetherian local ring (A,m), dim A=dim gr_m(A).
Not formalized. No checked P/H/open/external theorem proves dim A = dim gr_m(A) for arbitrary Noetherian local A; the associated-graded object is still open-PR-only and the needed Samuel bridge is absent.
Definition: determinantal ideals
For an r×s matrix M over a Noetherian ring, I_t(M) is the ideal generated by all t×t minors.
Not formalized. Matrix minors/determinants are formalized generically, but no checked declaration packages Matsumura’s determinantal ideals and the associated row/column/local-height theorems. Generic minor arithmetic is not credited for this reusable commutative-algebra unit.
Construction: elementary row/column operations and determinantal ideals
Elementary row/column operations preserve I_t. If M contains a unit entry, such operations reduce it to a block with a 1 and an (r-1)×(s-1) matrix N, with I_t(M)=I_{t-1}(N).
Not formalized. Matrix minors/determinants are formalized generically, but no checked declaration packages Matsumura’s determinantal ideals and the associated row/column/local-height theorems. Generic minor arithmetic is not credited for this reusable commutative-algebra unit.
Lemma: determinantal-height auxiliary lemma
Let (A,P) be Noetherian local, B=A[X], J P-primary and J′⊆PB with J′+XB=JB+XB. Then PB is a minimal prime divisor of J′.
Not formalized. Matrix minors/determinants are formalized generically, but no checked declaration packages Matsumura’s determinantal ideals and the associated row/column/local-height theorems. Generic minor arithmetic is not credited for this reusable commutative-algebra unit.
Theorem: Theorem 13.10 (Eagon)
For an r×s matrix (r≤s) over a Noetherian ring, if P is a minimal prime over the t-minor ideal I_t, then ht P≤(r-t+1)(s-t+1).
Not formalized. Matrix minors/determinants are formalized generically, but no checked declaration packages Matsumura’s determinantal ideals and the associated row/column/local-height theorems. Generic minor arithmetic is not credited for this reusable commutative-algebra unit.
Definition: systems of parameters
For an r-dimensional Noetherian local ring (A,m), r elements of m generating an m-primary ideal form a system of parameters. For finite M of dimension s, y_1,…,y_s in m form a system of parameters of M when M/(y_1,…,y_s)M has finite length.
Not formalized. The project defines LeanCategories.Algebra.IsSystemOfParameters for a local ring as radical of the generated ideal equal to the maximal ideal, matching the ring notion. The source unit also defines systems of parameters for finite modules by finite-length quotient; no checked owner supplies that module-level half, so strict whole-row semantics leaves it unmatched.
Definition: embedding dimension and regular local ring
embdim A=dim_{A/m}(m/m²), the minimal number of generators of m. One has dim A≤embdim A; equality defines a regular local ring, and a parameter system generating m is a regular system of parameters.
Formalized. Mathlib/Algebra/Module/SpanRankOperations.lean::spanFinrank_maximalIdeal_eq_finrank_cotangentSpace; Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::ringKrullDim_le_spanFinrank_maximalIdeal; Mathlib/RingTheory/RegularLocalRing/Defs.lean::IsRegularLocalRing, isRegularLocalRing_iff — The minimal generator count of m equals the residue-field dimension of m/m², Krull dimension is bounded by it, and IsRegularLocalRing is exactly equality. A regular system of parameters is therefore a parameter system generating m.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 14.1
For a system of parameters x_1,…,x_r, dim A/(x_1,…,x_i)=r-i. Moreover one can choose a system of parameters such that every subset generates an ideal whose height equals its cardinality.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Example: a parameter prefix can have too small height
The source gives a two-dimensional quotient of k[X,Y,Z] with a system of parameters {y,x+z} for which ht(y)=0, showing the second clause of Theorem 14.1 needs a suitable choice.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Theorem: Theorem 14.2
For an n-dimensional regular local ring (R,m) and x_1,…,x_i∈m, the following are equivalent: they extend to a regular system of parameters; their images in m/m² are linearly independent; R/(x_1,…,x_i) is regular local of dimension n-i.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Remark: quotient regularity implies extendability without ambient regularity
The implication from regularity of R/(x_1,…,x_i) of dimension n-i to extendability of x_1,…,x_i to a minimal generating set of m does not require R itself to be regular.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Theorem: Theorem 14.3
Every regular local ring is an integral domain.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Theorem: Theorem 14.4
If (A,m,k) is d-dimensional regular local, then gr_m(A)≅k[X_1,…,X_d], and its Samuel function is the binomial coefficient (n+d choose d) for all n≥0.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Definition: analytic independence
Elements y_1,…,y_r∈m are analytically independent if every homogeneous form F over A satisfying F(y_1,…,y_r)=0 has all coefficients in m.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Theorem: Theorem 14.5
Every system of parameters of a d-dimensional Noetherian local ring is analytically independent.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Definition: null-form of a parameter ideal
For q=(x_1,…,x_d) and k=A/m, a homogeneous f∈k[X_1,…,X_d] is a null-form of q if every homogeneous lift F over A satisfies F(x_1,…,x_d)∈q^n m in its degree n.
Not formalized. Pinned/current Mathlib has regular-local, cotangent-space, polynomial and height infrastructure, but no source-shaped declaration for this parameter/analytic-independence/associated-graded statement. Targeted external search did not produce a complete compatible owner.
Definition: multiplicity e(q,M)
For finite M over d-dimensional Noetherian local A and m-primary q, the eventual Samuel polynomial has leading term e(q,M)n^d/d!. This integer is the multiplicity of M relative to q; e(q)=e(q,A), and e(A)=e(m).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Formula: Formulas 14.1–14.4
Multiplicity satisfies the limit formula e(q,M)=lim d!·length(M/qnM)/nd; it is positive when dim M=d and zero when dim M<d; e(qr,M)=rd e(q,M); and q⊇q′ m-primary implies e(q,M)≤e(q′,M).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.6
For an exact sequence 0→M′→M→M″→0 of finite A-modules, e(q,M)=e(q,M′)+e(q,M″).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.7 (associativity formula)
Let p_i be the minimal primes of A with dim A/p_i=d. Then e(q,M) is the sum over these p_i of length_{A_{p_i}}(M_{p_i}) times the multiplicity of the image of q on A/p_i.
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.8
If A is a Noetherian local domain, q an ideal of definition, and M finite of rank s, then e(q,M)=s·e(q).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.9
If x_1,…,x_d is a system of parameters contained in an ideal of definition q and x_i∈q^{v_i}, then successive quotient multiplicities are bounded below by products of the v_i times e(q,M); in particular length(M/(x_1,…,x_d)M)≥v_1⋯v_d e(q,M).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.10
For a parameter ideal q=(x_1,…,x_d), length(A/q)≥e(q); if additionally every x_i∈m^v, then length(A/q)≥v^d e(m).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.11
With q=(x_1,…,x_d), if x_1 is M-regular and A′=A/x_1A, M′=M/x_1M, q′=q/x_1A, then e(q′,M′)=e(q,M).
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.12 (Lech lemma)
For a system of parameters x_1,…,x_d and finite M, e(q,M) is the limit of length(M/(x_1{v_1},…,x_d{v_d})M)/(v_1⋯v_d) as min(v_i)→∞.
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Serre multiplicity formula
For a parameter system x and finite M, the source states Serre’s formula e(q,M)=Σ_i(-1)^i length(H_i(x;M)), expressing multiplicity as the Euler characteristic of Koszul homology.
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Definition: reduction of an ideal
For ideals b⊆a, b is a reduction of a if a{r+1}=bar for some r≥0; then a{r+n}=bn a^r for every n≥0.
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.13
If q is m-primary and b is a reduction of q, then b is m-primary and e(b,M)=e(q,M) for every finite A-module M.
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Theorem: Theorem 14.14
If (A,m) is d-dimensional Noetherian local with infinite residue field and q=(u_1,…,u_s) is m-primary, then d sufficiently general linear combinations of the u_j generate a reduction b of q; equivalently the bad coefficient choices lie in a proper algebraic subset.
Not formalized. No Hilbert–Samuel multiplicity/reduction API matching Matsumura §14 was found in P, current Mathlib, open PRs, or discoverable compatible Lean repositories. Existing generic Multiplicity, Koszul, Rees, and ideal APIs do not supply this source theorem.
Definition: fibre, fibre ring, closed fibre and generic fibre
For A→B and p∈Spec A, the fibre is Spec(B⊗_A κ(p)) and B⊗_A κ(p) is its fibre ring. For local A the fibre over its maximal ideal is the closed fibre; for a domain A the fibre over (0) is the generic fibre.
Formalized. Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean::Ideal.Fiber, PrimeSpectrum.preimageHomeomorphFiber — p.Fiber B is κ(p) ⊗[A] B, and preimageHomeomorphFiber identifies its prime spectrum with the fibre of Spec B→Spec A; maximal/zero-prime specializations are exactly closed/generic fibres.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 15.1
For a homomorphism A→B of Noetherian rings and P∈Spec B with p=P∩A, ht P≤ht p+dim(B_P/pB_P); equality holds if the map is flat, or more generally if going-down holds.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::Ideal.height_le_height_add_of_liesOver, Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown; Mathlib/RingTheory/Ideal/GoingDown.lean::Algebra.HasGoingDown.of_flat; Mathlib/RingTheory/Ideal/Height.lean::IsLocalization.AtPrime.ringKrullDim_eq_height — The pinned height theorem bounds ht P by ht p plus the height of P in the quotient by pB; localizing identifies that term with dim(B_P/pB_P). Under going down equality is explicit, and flatness installs going down.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 15.2
Under going-up for A→B, if p⊃q are primes of A then dim(B⊗κ(p))≥dim(B⊗κ(q)).
Not formalized. Going-up/going-down and fibre rings are formalized separately, but no checked declaration states the monotonic Krull-dimension comparison of fibres under specialization/generalization with the source hypotheses.
Theorem: Theorem 15.3
Under going-down for A→B, if p⊃q are primes of A then dim(B⊗κ(p))≤dim(B⊗κ(q)).
Not formalized. Going-up/going-down and fibre rings are formalized separately, but no checked declaration states the monotonic Krull-dimension comparison of fibres under specialization/generalization with the source hypotheses.
Theorem: Theorem 15.4
For Noetherian A and n indeterminates, dim A[X_1,…,X_n]=dim AX_1,…,X_n=dim A+n.
Not formalized. Pinned Mathlib proves MvPolynomial.ringKrullDim_of_isNoetherianRing, but for formal power series only a lower bound is present. No current/open exact theorem gives dim AX_1,…,X_n=dim A+n, so the bundled equality is unmatched.
Counterexample: maximal ideals of A[X] need not lie over maximal ideals
If A is a DVR with uniformizer t and fraction field K, then (tX-1) is maximal in A[X] with quotient K but contracts to (0) in A.
Not formalized. The DVR, polynomial and quotient-field APIs can express (tX-1), but no checked declaration owns the source maximality/contraction counterexample as a reusable unit.
Example: formal-power-series generic fibres can have excess dimension
The source constructs a map k[Y,Z]→kX whose generic fibre has dimension two, showing fibres of A→AX_1,…,X_n can have dimension strictly larger than n.
Not formalized. No checked declaration realizes Matsumura’s explicit map k[Y,Z]→kX and proves its generic fibre has dimension two.
Definition: universally catenary ring
A Noetherian ring A is universally catenary if every finitely generated A-algebra is catenary; equivalently all polynomial rings A[X_1,…,X_n] are catenary.
Not formalized. No compatible catenary/universally-catenary or commutative-algebra dimension-formula API was found in P/current/open Mathlib or targeted external Lean search. Height and transcendence-degree ingredients alone are not credited.
Theorem: Theorem 15.5 (Cohen dimension inequality)
For a Noetherian domain A, a domain extension B, P∈Spec B and p=P∩A, ht P+trdeg_{κ(p)}κ(P)≤ht p+trdeg_A B.
Not formalized. No compatible catenary/universally-catenary or commutative-algebra dimension-formula API was found in P/current/open Mathlib or targeted external Lean search. Height and transcendence-degree ingredients alone are not credited.
Definition: dimension inequality and dimension formula
The inequality in Theorem 15.5 is called the dimension inequality; A→B satisfies the dimension formula when equality holds for every P∈Spec B. Polynomial extensions satisfy the dimension formula.
Not formalized. No compatible catenary/universally-catenary or commutative-algebra dimension-formula API was found in P/current/open Mathlib or targeted external Lean search. Height and transcendence-degree ingredients alone are not credited.
Theorem: Theorem 15.6 (Ratliff)
A Noetherian ring A is universally catenary iff for every prime p of A and every finitely generated integral-domain extension B of A/p, the dimension formula holds between A/p and B.
Not formalized. No compatible catenary/universally-catenary or commutative-algebra dimension-formula API was found in P/current/open Mathlib or targeted external Lean search. Height and transcendence-degree ingredients alone are not credited.
Construction: ordinary Rees ring R+(A,I)
For I=(a_1,…,a_r) and indeterminate t, R_+(A,I)=⊕{n≥0}I^n t^n=A[a_1t,…,a_rt]⊆A[t]. If A is Noetherian then R+ is Noetherian, and gr_I(A)≅R_+/IR_+.
Not formalized. Pinned Mathlib defines the ordinary ReesAlgebra, but the source unit also requires associated-graded quotient/deformation/dimension or primary-decomposition clauses absent from P. Open associated-graded PRs do not supply these full Rees bundles.
Construction: extended Rees ring and deformation to grI(A)
With u=t^{-1}, R(A,I)=R_+(A,I)[u]⊆A[t,t^{-1}]. It satisfies R/(1-u)R≅A, R/uR≅gr_I(A), and unR∩A=In, so gr_I(A) is the u=0 fibre and A the u=1 fibre.
Not formalized. Pinned Mathlib defines the ordinary ReesAlgebra, but the source unit also requires associated-graded quotient/deformation/dimension or primary-decomposition clauses absent from P. Open associated-graded PRs do not supply these full Rees bundles.
Construction: extension of ideals to the extended Rees ring
For a⊲A, set a′=aA[t,u]∩R(A,I). Distinct ideals remain distinct; primes and primary ideals remain prime/primary; primary decompositions of (0) induce primary decompositions in R, and minimal primes correspond.
Not formalized. Pinned Mathlib defines the ordinary ReesAlgebra, but the source unit also requires associated-graded quotient/deformation/dimension or primary-decomposition clauses absent from P. Open associated-graded PRs do not supply these full Rees bundles.
Theorem: Theorem 15.7
For Noetherian A and proper I, with R=R(A,I) and G=gr_I(A), dim R=dim A+1 and dim G≤dim A; if A is local then dim G=dim A.
Not formalized. Pinned Mathlib defines the ordinary ReesAlgebra, but the source unit also requires associated-graded quotient/deformation/dimension or primary-decomposition clauses absent from P. Open associated-graded PRs do not supply these full Rees bundles.