Chapter 11. Dimension Theory (pp. 116–124)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 14 definitions, 4 theorems, 9 propositions, 2 lemmas, 12 corollaries, 3 examples, 1 construction, 1 remark, 1 convention and 6 other statements.
Of the 53 statements checked against Lean, 18 are formalized somewhere and 35 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 35 | 66% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 15 | 28% | Mathlib states and proves it. |
| in lean-categories | 3 | 6% | This repository states and proves it. |
| checked in total | 53 |
- Project search was performed first at repo HEAD
351cba0287077eadfcd7c71a78ec4a509ce8c966.LeanCategories/Algebra/DimensionTheory.leanis the project owner for exactly three source-facing definitions used here:LeanCategories.Algebra.PoincareSeries(U002),LeanCategories.Algebra.IsSystemOfParameters(U034), andLeanCategories.Algebra.AffineVarietyDimension(U047). The file’s current content was read from HEAD rather than inferred from earlier vault snapshots, and it compiled successfully in the project environment. ItsHilbertFunctionis the raw coefficient function and therefore is not the source’s eventual Hilbert polynomial in U007. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0). P contains the exact length/additivity, regular-element, ideal-height/Krull-height, regular-local, polynomial-regularity, affine function-field, Nullstellensatz, and scheme-stalk dimension APIs cited in the chapter. The U026 source-shaped system-of-parameters existence assembly was compiled against P. A declaration probe covering U029/U032/regular-local/polynomial-dimension interfaces also compiled against P. - Current Mathlib is
H=5aedf732b6987e8c26ab3c9ebc855314f82b045f(Apache-2.0), rechecked on 2026-09-06. H still has no graded-module Hilbert–Serre theorem, no Hilbert–Samuel eventual-polynomial construction, no theorem that regular local rings are preserved/reflected by adic completion, and no theorem equating local Krull dimension of finite-type integral affine algebras with transcendence degree. Directgit grepat H found only the genericPolynomial.hilbertPolybackend for the first family of gaps and no owners for the latter two families. Mathlib/RingTheory/Polynomial/HilbertPoly.leanis deliberately only a backend: it proves eventual coefficient identities for a rational function already presented asp/(1-X)^d, e.g.Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval. It does not derive such a rational form from a finite graded module. Therefore it does not satisfy U003, U005, or the Hilbert–Samuel rows U012–U021/U027.- Current external Hilbert–Samuel search rechecked
ImperialCollegeLondon/FLT@8ec873aab84b21c4faaef849d5afd56ef79f684d(Apache-2.0; Leanv4.34.0-rc2; Mathlibc4a007f4389f67c1f224c4b87984a3470754b53f).FLT/Slop/DimensionTheorem/Defs.lean,DimEqDelta.lean,GrowthLeDelta.lean, andMain.leandefine the exact least-generator invariantminGenPrimaryand prove its equality with Krull dimension and with a growth-order invariant. The development explicitly states that it does not construct the Hilbert–Samuel polynomial or formalize Hilbert–Serre;growthDegis intentionally a replacement. Hence these files are useful negative evidence, not exact reference ports for the source polynomial-degree rows. - GitHub indexed Lean search for
HilbertSerre, graded Hilbert series, Hilbert–Samuel polynomiality, and characteristic-polynomial length growth found no exact owner beyond Mathlib’s rational-function backend and FLT’s explicit growth-order substitute. The external FLT head was checked immediately before assembly. - Current regular-completion search checked P/H and indexed external Lean. No exact theorem
IsRegularLocalRing A ↔︎ IsRegularLocalRing Âor equivalent was found.Mathlib/RingTheory/Regular/RegularSequence.leanstill contains a TODO to apply the relevant regular-sequence theory to localization and completion.DE0CH/flt-lean@a5ec7082457bab42553702cdb183b3e034021ab3was rechecked; itsFermat/FLT/GaloisRepresentation/HardlyRamified/CompleteLocalNoetherian.leanproves complete-local Noetherianity from finite generation of the maximal ideal, not preservation of regularity or the coefficient-field power-series theorem required by U042/U044. - Current affine-dimension search at P/H and indexed external Lean found no theorem containing a Krull-dimension/transcendence-degree bridge for the source finite-type integral affine setting. The project therefore owns only the trdeg definition U047; pinned Mathlib separately owns function fields, Nullstellensatz point/maximal-ideal correspondence, and local/stalk Krull dimension. Their absence of a connecting theorem is the reason U050/U051/U053 remain unmatched.
- For U052, P supplies
Ideal.isMaximal_comap_of_isIntegral_of_isMaximal, going down for integral extensions over integrally closed domains, prime-chain lifting viaIdeal.exists_ltSeries_of_hasGoingDown, andIsLocalization.AtPrime.ringKrullDim_eq_height. No checked theorem or compiled source-shaped assembly gave equality of the two localized dimensions under exactly the source hypotheses without adding Noetherian assumptions, so the whole row remains unmatched. Ndenotes dated 2026-09-06 negative evidence after project-first inspection, P, H/current Mathlib, relevant open/current work, and targeted external Lean search. A theorem phrased in a substitute invariant (growthDeginstead of Hilbert–Samuel polynomial degree), one direction of a biconditional, or a collection of adjacent ingredients without a checked whole-row assembly is not credited under strict bundle semantics.
Construction / comparison: Homogeneous finite-generation setup
For a Noetherian graded ring A, A₀ is Noetherian and A is generated over A₀ by finitely many homogeneous x_i of positive degrees k_i. A finitely generated graded A-module M has homogeneous generators, and each homogeneous component Mₙ is finitely generated over A₀.
Not formalized. partial: GradedRing.GradeZero.isNoetherianRing; homogeneous graded APIs — P proves that degree zero of a Noetherian graded ring is Noetherian and has homogeneous infrastructure, but the source bundle also requires finite homogeneous generation of the whole Noetherian graded ring over degree zero and homogeneous finite generators/component finiteness for every finite graded module. The missing graded Hilbert-basis converse is exactly the C10-U029 gap.
Definition: Poincaré series
For an additive integer-valued function λ on finitely generated A₀-modules, the Poincaré series of M is P(M,t)=∑_{n≥0} λ(Mₙ)tⁿ ∈ Zt.
Formalized. LeanCategories/Algebra/DimensionTheory.lean::LeanCategories.Algebra.PoincareSeries — The project definition sends an invariant λ of modules to the power series with coefficient λ(M n) in degree n, exactly the source formula. Additivity of λ is a surrounding hypothesis, not part of the constructor. The file compiles at current HEAD.
Searched: repo HEAD
Theorem: Theorem 11.1 (Hilbert–Serre)
If A is generated over A₀ by homogeneous x_i of degrees k_i and M is finitely generated graded, then P(M,t)=f(t)/∏_{i=1}s(1−t{k_i}) for some f(t)∈Z[t].
Not formalized. partial: Mathlib/RingTheory/Polynomial/HilbertPoly.lean rational-series coefficient backend — P/H can manipulate a series already known to have denominator (1-X)^d, but contain no theorem deriving the Hilbert–Serre rational form from a finitely generated graded module. Current FLT explicitly records this as still missing.
Definition / notation: The invariant d(M)
d(M) denotes the order of the pole of P(M,t) at t=1; d(A) is defined similarly in this graded setting.
Not formalized. partial: Polynomial.hilbertPoly; power-series algebra — No checked project/P/H/external declaration defines the order of the pole at t=1 of a module Poincaré series as the source invariant d(M).
Corollary: Corollary 11.2
If all algebra generators have degree k_i=1, then for all sufficiently large n, λ(Mₙ) is a rational-coefficient polynomial in n of degree d(M)−1.
Not formalized. partial: Polynomial.coeff_mul_invOneSubPow_eq_hilbertPoly_eval — P proves eventual polynomial coefficients for an already supplied rational function p/(1-X)^d, but without U003 there is no theorem producing that rational form from the graded module and no source-shaped degree d(M)-1 conclusion.
Remark / example: Integer-valued polynomials need not have integral coefficients
A polynomial taking integer values on all integers need not have integer coefficients; the source gives x(x+1)/2.
Not formalized. generic rational/polynomial arithmetic only — The elementary example x(x+1)/2 is readily expressible in Lean, but no checked project/P/H/current external declaration owns the source example as a reusable formalized unit.
Definition / notation: Hilbert function (polynomial)
The eventual polynomial supplied by 11.2 is called the Hilbert function (or Hilbert polynomial) of M with respect to λ.
Not formalized. partial: project LeanCategories.Algebra.HilbertFunction; P Polynomial.hilbertPoly — The project HilbertFunction is the raw coefficient function n ↦ λ(M_n), while the source row names the eventual polynomial supplied by Corollary 11.2. No declaration identifies those notions under the missing eventual-polynomial theorem.
Definition / convention: Non-zero-divisor on a module
For x∈A and an A-module M, the source says x is not a zero-divisor on M when xm=0 with m∈M implies m=0.
Formalized. Mathlib/RingTheory/Regular/IsSMulRegular.lean::IsSMulRegular; isSMulRegular_iff_right_eq_zero_of_smul — IsSMulRegular M x is exactly injectivity of scalar multiplication by x, equivalently x • m = 0 → m = 0.
Searched: P
Proposition: Proposition 11.3
If x∈A_k is not a zero-divisor on M, then d(M/xM)=d(M)−1.
Not formalized. partial: IsSMulRegular; exact-sequence/graded APIs — P/H have the non-zero-divisor and quotient module ingredients, but the conclusion is phrased in the missing pole-order invariant d(M), so no exact owner exists.
Convention / comparison: Length as the additive function over an Artin base
When A₀ is Artin (in particular, a field), the source specializes λ to module length l, which is additive.
Formalized. Mathlib/RingTheory/Length.lean::Module.length; Module.length_ne_top; Module.length_eq_add_of_exact — Module length is finite under the Artinian/Noetherian hypotheses and is additive in short exact sequences, exactly the source specialization of λ to length over an Artin base.
Searched: P
Example: Poincaré series of a polynomial ring over an Artin ring
For A=A₀[x₁,…,x_s] with A₀ Artin and x_i independent of degree 1, Aₙ is free on the degree-n monomials and P(A,t)=(1−t)^{-s}.
Not formalized. partial: monomial bases; project PoincareSeries; power-series identities — P/H have the degree-monomial combinatorics and formal series algebra, but no checked whole-row theorem identifies the length Poincaré series of the standard polynomial ring with (1-t)^{-s}.
Proposition: Proposition 11.4
Let (A,m) be Noetherian local, q m-primary, M finitely generated, and (Mₙ) a stable q-filtration. Then each M/Mₙ has finite length; for large n this length is a polynomial g(n) of degree ≤s, where s is the least number of generators of q; and the degree and leading coefficient depend only on M and q, not the stable filtration.
Not formalized. partial: stable filtrations, module length, Polynomial.hilbertPoly backend — No project/P/H/current external theorem proves eventual polynomiality of length(M/M_n) for stable primary filtrations together with the generator bound and filtration-independence of degree/leading coefficient. Imperial FLT intentionally replaces this polynomial theorem by growth order.
Definition / notation: χq^M and the characteristic polynomial χq
For the q-adic filtration, χ_q^M(n)=l(M/qⁿM) for all large n. For M=A write χ_q(n)=χ_q^A(n), called the characteristic polynomial of the m-primary ideal q.
Not formalized. partial: adic powers and module length — The source definition depends on the missing eventual polynomial in U012; no checked declaration packages χ_q^M as that eventual Hilbert–Samuel polynomial.
Corollary: Corollary 11.5
For all large n, l(A/qⁿ)=χ_q(n), a polynomial of degree at most the least number s of generators of q.
Not formalized. partial: U012 ingredients — P/H do not prove that length(A/q^n) eventually agrees with a polynomial of degree bounded by the least number of generators of q.
Proposition: Proposition 11.6
For a Noetherian local ring (A,m) and any m-primary q, deg χ_q = deg χ_m.
Not formalized. partial: primary ideals, cofinal adic filtrations — Cofinality and primary-ideal infrastructure exist, but the source conclusion compares degrees of Hilbert–Samuel characteristic polynomials, which are not formalized.
Definition / notation: The local invariant d(A)
For a Noetherian local ring A, d(A) is the common degree of the characteristic polynomials χ_q; equivalently d(A)=d(G_m(A)), the pole order at t=1 for the associated graded ring.
Not formalized. partial: associated graded/open PR infrastructure; Polynomial.hilbertPoly — Neither the common degree of the characteristic polynomials nor its equality with the associated-graded Poincaré pole order is formalized as the source invariant d(A).
Definition / notation: The invariant δ(A)
For a Noetherian local ring (A,m), δ(A) is the least number of generators of an m-primary ideal. The source sets the target equality δ(A)=d(A)=dim A.
Not formalized. partial external: FLT DimensionTheorem.minGenPrimary — FLT current HEAD defines exactly the least generator count of a maximal-primary ideal, but the source unit also places it in the target comparison δ(A)=d(A)=dim A; FLT uses a different growth invariant in place of the source Hilbert–Samuel polynomial degree. Strict whole-bundle semantics therefore do not credit the external partial owner.
Proposition: Proposition 11.7
For a Noetherian local ring, δ(A)≥d(A).
Not formalized. partial external: FLT growth-degree inequality — FLT proves the analogous inequality for its growth-order replacement, not the source Hilbert–Samuel polynomial degree d(A). P/H have no exact theorem.
Proposition: Proposition 11.8
Let (A,m) be Noetherian local, q m-primary, M finitely generated, x a non-zero-divisor on M, and M′=M/xM. Then deg χ_q^{M′} ≤ deg χ_q^M−1.
Not formalized. partial: Artin–Rees; IsSMulRegular; length — The algebraic ingredients exist, but the degree comparison deg χ_q^{M/xM} ≤ deg χ_q^M - 1 depends on absent Hilbert–Samuel polynomial objects.
Corollary: Corollary 11.9
If A is Noetherian local and x is a non-zero-divisor, then d(A/(x))≤d(A)−1.
Not formalized. partial: P dimension drop theorem; U019 ingredients — P has Krull-dimension drop for a regular element, but not the source Hilbert–Samuel-degree invariant d(A), so it does not satisfy this row.
Proposition: Proposition 11.10
For a Noetherian local ring A, d(A)≥dim A.
Not formalized. partial: P Krull dimension; external FLT growth-degree equality — Current exact developments compare Krull dimension with growth order, not with the source degree of χ_m; the stated inequality is therefore not represented.
Corollary: Corollary 11.11
Every Noetherian local ring has finite dimension.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::Ideal.finiteHeight_of_isNoetherianRing; local FiniteRingKrullDim instance — Every ideal has finite height in a Noetherian ring; in a local ring the maximal ideal has height equal to ring Krull dimension, giving finite local dimension exactly as stated.
Searched: P
Definition / comparison: Height of a prime ideal
For a prime p⊆A, height(p) is the supremum of lengths of prime chains ending at p; height(p)=dim A_p.
Formalized. Mathlib/RingTheory/Ideal/Height.lean::Ideal.height; IsLocalization.AtPrime.ringKrullDim_eq_height — Mathlib’s ideal height is the chain-height invariant, and localization at a prime has Krull dimension exactly that height.
Searched: P
Corollary: Corollary 11.12
Every prime ideal in a Noetherian ring has finite height; consequently the set of prime ideals satisfies the descending chain condition.
Formalized. Ideal.finiteHeight_of_isNoetherianRing; Ideal.height_strict_mono_of_isPrime_of_isPrime — Every prime has finite height; strict inclusion of primes strictly raises height. Hence any descending chain below a fixed starting prime strictly decreases a finite ordinal height and terminates, yielding the source DCC consequence.
Searched: P
Definition / comparison: Depth of a prime ideal (chain-theoretic usage)
The source defines depth(p) by chains of primes starting at p and notes depth(p)=dim(A/p); unlike height, it may be infinite in a Noetherian nonlocal ring.
Not formalized. partial: quotient Krull dimension and prime-spectrum chains — P/H formalize ringKrullDim (A/p) and chain/coheight notions, but no checked declaration packages the source’s nonstandard term depth(p) with the stated equality and possible infinitude comparison.
Proposition: Proposition 11.13
If A is Noetherian local of dimension d, there exists an m-primary ideal generated by d elements; hence dim A≥δ(A).
Formalized. Ideal.exists_finset_card_eq_height_of_isNoetherianRing; IsLocalRing.maximalIdeal_height_eq_ringKrullDim; Ideal.sInf_minimalPrimes — Applied to the maximal ideal, the pinned height theorem produces a finite generating set whose span has the maximal ideal as a minimal prime and whose cardinality is the local dimension; taking radicals gives an m-primary ideal generated by exactly dim A elements. The source-shaped assembly compiled against P.
Searched: P
Theorem: Theorem 11.14 (dimension theorem)
For any Noetherian local ring A, the following are equal: (i) the maximum length of chains of prime ideals; (ii) the degree of χ_m(n)=l(A/mⁿ); (iii) the least number of generators of an m-primary ideal. In the frozen extraction, clause (iii) and the proof citation are displaced to L4329–L4331.
Not formalized. partial: U026 and P Krull dimension; external FLT growth theorem — P proves the Krull-dimension/parameter-count side, and FLT proves equality with a growth-order replacement, but no checked source proves equality with the degree of the Hilbert–Samuel polynomial χ_m. The three-clause source bundle remains unmatched.
Example: Dimension of the local polynomial ring at the origin
For A=k[x₁,…,xₙ] localized at m=(x₁,…,xₙ), G_m(A) is a polynomial ring in n variables, so dim A_m=n.
Not formalized. partial: MvPolynomial.ringKrullDim_of_isNoetherianRing; MvPolynomial.isRegularRing_of_isRegularRing; MvPolynomial.idealOfVars — P has global polynomial-ring dimension, regularity, and the ideal generated by the variables, but no checked source-shaped owner/assembly was found for dim k[x₁,…,xₙ]_(x₁,…,xₙ)=n.
Corollary: Corollary 11.15
For a Noetherian local ring (A,m) with residue field k, dim A≤dim_k(m/m²).
Formalized. ringKrullDim_le_spanFinrank_maximalIdeal; spanFinrank_maximalIdeal_eq_finrank_cotangentSpace — The pinned height theorem gives dim A ≤ spanFinrank(m), and the cotangent-space theorem identifies this generator rank with dim_k(m/m²).
Searched: P
Corollary: Corollary 11.16
If A is Noetherian and x₁,…,x_r∈A, then every minimal prime p over (x₁,…,x_r) has height at most r.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::Ideal.height_le_card_of_mem_minimalPrimes_span_finset — A prime minimal over the ideal generated by a finite set has height bounded by the cardinality of that set, exactly Corollary 11.16.
Searched: P
Corollary: Corollary 11.17 (Krull principal ideal theorem)
If A is Noetherian and x is neither a zero-divisor nor a unit, every minimal prime over (x) has height 1.
Formalized. Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes; Ideal.height_span_singleton_eq_one_of_mem_nonZeroDivisors — For a non-zero-divisor x, the principal ideal has height one, while every minimal prime over it has height at most one; the infimum characterization of ideal height forces every such minimal prime to have height exactly one.
Searched: P
Corollary: Corollary 11.18
If A is Noetherian local and x∈m is not a zero-divisor, then dim A/(x)=dim A−1.
Formalized. Mathlib/RingTheory/KrullDimension/Regular.lean::ringKrullDim_quotient_span_singleton_succ_eq_ringKrullDim — In a Noetherian local ring, quotienting by a non-zero-divisor in the maximal ideal decreases Krull dimension by exactly one, in the source’s successor formulation.
Searched: P
Corollary: Corollary 11.19
For a Noetherian local ring A, its m-adic completion has the same dimension: dim A=dim Â.
Not formalized. partial: adic completion/local ring APIs — Neither P nor H has a theorem identifying ringKrullDim A with the Krull dimension of its maximal-adic completion; current search also found no compatible external exact owner.
Definition: System of parameters
If d=dim A and x₁,…,x_d generate an m-primary ideal, then x₁,…,x_d are called a system of parameters.
Formalized. LeanCategories/Algebra/DimensionTheory.lean::LeanCategories.Algebra.IsSystemOfParameters — The project predicate says that the radical of the ideal generated by a finite family is the maximal ideal. Under the source context that the family has length d=dim A, this is exactly a system of parameters. The file compiles at current HEAD.
Searched: repo HEAD
Proposition: Proposition 11.20
Let x₁,…,x_d be a system of parameters, q=(x₁,…,x_d), and f(t₁,…,t_d) homogeneous of degree s over A. If f(x₁,…,x_d)∈q^{s+1}, then every coefficient of f lies in m.
Not formalized. partial: homogeneous polynomial and parameter APIs — No checked project/P/H/open/external declaration proves that a homogeneous relation modulo q^{s+1} for a system of parameters forces all coefficients into the maximal ideal.
Corollary: Corollary 11.21
If k⊆A maps isomorphically onto A/m and x₁,…,x_d is a system of parameters, then x₁,…,x_d are algebraically independent over k.
Not formalized. partial: AlgebraicIndependent; project IsSystemOfParameters — P/H have algebraic-independence APIs, but no theorem derives independence of a system of parameters from a coefficient field via Proposition 11.20.
Definition: Regular local ring
A regular local ring is a Noetherian local ring satisfying the equivalent regularity conditions stated immediately in Theorem 11.22; geometrically these generalize local rings at nonsingular points.
Formalized. Mathlib/RingTheory/RegularLocalRing/Defs.lean::IsRegularLocalRing; isRegularLocalRing_iff — Mathlib defines a Noetherian local ring to be regular exactly when the generator rank of its maximal ideal equals its Krull dimension, one of the source’s equivalent regularity conditions.
Searched: P
Theorem: Theorem 11.22
For a Noetherian local ring A of dimension d, maximal ideal m, residue field k, the following are equivalent: G_m(A)≅k[t₁,…,t_d]; dim_k(m/m²)=d; m can be generated by d elements.
Not formalized. partial: IsRegularLocalRing.iff_finrank_cotangentSpace; C10 associated-graded PRs — P gives equivalence between regularity, cotangent-space dimension, and maximal-ideal generator rank, but not the source’s additional isomorphism G_m(A) ≃ k[t₁,…,t_d]. Associated graded structures are themselves only open-PR ports, and no checked theorem supplies this polynomial identification.
Lemma: Lemma 11.23
If a⊆A satisfies ⋂aⁿ=0 and G_a(A) is an integral domain, then A is an integral domain.
Not formalized. partial: separated adic/Krull intersection; associated-graded PRs — No checked P/H/open/external theorem states that a separated filtered ring with integral-domain associated graded ring is itself a domain.
Named comparison: Regular local rings of dimension one are DVRs
The regular local rings of dimension 1 are exactly the discrete valuation rings.
Not formalized. partial: IsRegularLocalRing instance for local principal ideal domains; DVR APIs — P proves the DVR/local-PID direction gives a regular local ring, but no checked converse derives a DVR from one-dimensional regular-local hypotheses. Strict biconditional semantics make the row unmatched.
Named comparison: Regular local rings are integrally closed
The source records the more general implication: if A is local and G_m(A) is an integrally closed domain, then A is integrally closed. Hence regular local rings are integrally closed; the converse fails in dimension >1.
Not formalized. partial: integral-closure APIs; regular-local definitions — No checked owner proves the source general theorem that integrally closed associated graded implies the local ring integrally closed, nor the resulting regular-local implication together with the higher-dimensional converse failure.
Proposition: Proposition 11.24
A Noetherian local ring A is regular if and only if its completion  is regular.
Not formalized. partial: adic completion; regular-local APIs — P/H have no theorem A regular ↔︎ Â regular; current Mathlib search and external indexed search found no exact compatible owner.
Named comparison: Regularity implies analytic irreducibility
Because the completion of a regular local ring is again a regular local domain, the source expresses the geometric consequence as nonsingularity ⇒ analytic irreducibility (one analytic branch locally).
Not formalized. partial: completion/domain terminology — Since regularity of completion and its domain consequence are not formalized in the needed generality, no checked row owner proves the source analytic-irreducibility comparison.
Named comparison: Completion with a coefficient field
If A contains a field k mapping isomorphically to A/m and A is regular of dimension d, then  is a formal power series ring over k in d indeterminates; hence completions of nonsingular d-dimensional local rings over k are isomorphic.
Not formalized. partial: formal power series and adic completion equivalences — P/H can identify the completion of a polynomial ring at the variable ideal with formal power series, but no Cohen-style theorem identifies the completion of an arbitrary equicharacteristic regular local ring with kt₁,…,t_d.
Example: Affine-space local ring is regular
For A=k[x₁,…,xₙ] and m=(x₁,…,xₙ), A_m is regular because its associated graded ring is a polynomial ring in n variables.
Formalized. Mathlib/RingTheory/RegularLocalRing/Polynomial.lean::MvPolynomial.isRegularRing_of_isRegularRing; IsRegularRing.isRegularLocalRing_localization — A polynomial ring in finitely many variables over a field is regular, and localization of a regular ring at every prime is regular local; specializing to the origin maximal ideal gives the source example.
Searched: P
Definition: Field of rational functions k(V)
For irreducible affine V over algebraically closed k, A(V)=k[x₁,…,xₙ]/p for a prime p. The fraction field of this integral coordinate ring is the field of rational functions on V, denoted k(V).
Formalized. Mathlib/AlgebraicGeometry/FunctionField.lean::Scheme.functionField; functionField_isFractionRing_of_affine — For an integral affine scheme, Mathlib’s function field is a field and is a fraction ring of the affine coordinate ring, exactly the source rational-function field construction.
Searched: P
Definition: Dimension of an irreducible affine variety
The dimension of V is defined as the transcendence degree trdeg_k k(V), the maximum number of algebraically independent elements of k(V) over k.
Formalized. LeanCategories/Algebra/DimensionTheory.lean::LeanCategories.Algebra.AffineVarietyDimension — For a prime-presented affine variety, the project forms the quotient coordinate domain, its fraction ring, and defines dimension as Algebra.trdeg over the base field, exactly the source definition. The file compiles at current HEAD.
Searched: repo HEAD
Named comparison: Points and maximal ideals via the Nullstellensatz
For k algebraically closed, points of V correspond bijectively to maximal ideals of A(V).
Formalized. Mathlib/RingTheory/Nullstellensatz.lean::MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton; mem_zeroLocus_iff; quotient ideal correspondence — Over an algebraically closed field every maximal ideal of the polynomial ring is the vanishing ideal of a unique point in the finite-variable setting; restricting to maximal ideals containing the defining prime is equivalent to the point lying in its zero locus, and quotient ideal correspondence gives maximal ideals of the coordinate ring.
Searched: P
Definition: Local dimension of V at a point
If P∈V corresponds to the maximal ideal m⊆A(V), the local dimension of V at P is dim A(V)_m.
Formalized. Mathlib/AlgebraicGeometry/Properties.lean::ringKrullDim_stalk_eq_coheight; IsLocalization.AtPrime.ringKrullDim_eq_height — The local ring at an affine-scheme point is the localization at its prime ideal, and its Krull dimension is the point’s coheight/ideal height. For a closed point this is exactly the source local dimension dim A(V)_m.
Searched: P
Theorem: Theorem 11.25
For every irreducible affine variety V over an algebraically closed field, the local dimension at every point equals dim V.
Not formalized. partial: project AffineVarietyDimension; P local dimension — No checked P/H/current external theorem identifies every maximal-local Krull dimension of a finite-type integral affine algebra over an algebraically closed field with the transcendence degree of its fraction field.
Named comparison: Transcendence dimension bounds local dimension
By 11.21, dim V≥dim A(V)_m for every maximal ideal m corresponding to a point of V; the remaining work in 11.25 is the reverse inequality.
Not formalized. partial: project trdeg definition; P local Krull dimension — Current searches found no theorem proving the source inequality trdeg_k k(V) ≥ dim A(V)_m; the two notions exist but are not connected by a checked declaration.
Lemma: Lemma 11.26
Let B⊆A be integral domains with B integrally closed and A integral over B. If m is maximal in A and n=m∩B, then n is maximal and dim A_m=dim B_n.
Not formalized. partial: Ideal.isMaximal_comap_of_isIntegral_of_isMaximal; IntegralClosure/GoingDown.lean; Ideal.exists_ltSeries_of_hasGoingDown; localization height theorem — P proves contraction of maximal ideals and going down for integral extensions over integrally closed domains, but no checked source-shaped theorem/assembly was found proving equality of the two localized Krull dimensions under exactly the source hypotheses without extra Noetherian assumptions.
Corollary: Corollary 11.27
For every maximal ideal m of A(V), dim A(V)=dim A(V)_m.
Not formalized. partial: U047/U049 infrastructure — This corollary is the same missing transcendence-degree versus local Krull-dimension bridge as U050; no exact owner exists at P/H or in the checked current external sources.