Chapter 11. Applications of complete local rings
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 11 definitions, 23 theorems, 7 lemmas, 7 corollaries, 1 example, 1 counterexample and 1 construction.
Of the 51 statements checked against Lean, 3 are formalized somewhere and 48 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 48 | 94% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 3 | 6% | Mathlib states and proves it. |
| checked in total | 51 |
- Canonical source block: FC13 Matsumura Chapter 11,
FC13-C11-U001–FC13-C11-U051, §§31–33, in canonical source-ID order from Foundational corpus units FC13 Matsumura. All 51 IDs are retrieved throughagent-memory, asserted once/in-order, and assigned exactly one route. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280. No project-owned catenary, G-ring/excellence, Nagata-ring, or normalization theorem closes a C11 unit more completely than pinned Mathlib. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native C11 coverage is concentrated in the normalization tail:integralClosure A (FractionRing A),IsIntegralClosure.finitefor finite separable extensions, and Noether normalization. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493. Targeted P/H/open searches found no catenary/equidimensional/formally-catenary predicates, G-ring/excellence/Nagata-ring interfaces, geometrically-regular regular homomorphisms, or general Krull-ring/Mori–Nagata development. - Strict bundle semantics were enforced.
Ideal.Fiberplus completion does not by itself create a formal-fibre interface; smooth maps are not substituted for EGA regular homomorphisms; and U043 is not credited from the separable normalization theorem because the source explicitly includes the purely inseparable case. - No compatible open PR supplied a complete additional C11 row.
- Route totals for C11:
mathlib3,project-existing0,package-import0,reference-port0,unmatched48.
Theorem: Theorem 31.1
Let A be Noetherian and P prime. There are only finitely many primes P′⊋P with ht(P′/P)=1 but ht P′>ht P+1.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Theorem: Theorem 31.2 (Ratliff weak existence theorem)
If p⊂P are primes in a Noetherian ring, ht p=h and ht(P/p)=d>1, then there are infinitely many primes p′ with p⊂p′⊂P, ht p′=h+1, and ht(P/p′)=d−1. The extraction misreads the displayed label as “32.2”.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Lemma: Lemma 1
If A is Noetherian, P has height h>1, and a∈P has ht(aA)=1, then there are infinitely many primes Q⊂P with a∉Q and ht Q=h−1.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Theorem: Theorem 31.3 (Ratliff strong existence theorem)
Let A be a Noetherian domain, p⊂P primes with ht p=h>0 and ht(P/p)=d. For every 0≤i<d there are infinitely many primes p′⊂P with ht p′=h+i and ht(P/p′)=d−i.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Theorem: Theorem 31.4
A Noetherian local domain A is catenary iff ht p+coht p=dim A for every prime p.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Definition: equidimensional ring
A finite-dimensional ring A is equidimensional if dim(A/p)=dim A for every minimal prime p.
Not formalized. P/H have Krull dimension, minimal primes, completion and localization, but no reusable equidimensional, formally-equidimensional, or formally-catenary interface matching the source definition.
Lemma: Lemma 2
If a local ring is equidimensional and catenary, then ht p₂=ht p₁+ht(p₂/p₁) whenever p₁⊂p₂.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Theorem: Theorem 31.5
For a flat local homomorphism A→B of Noetherian local rings, if B is equidimensional and catenary then A is equidimensional and catenary, and B/pB is equidimensional for every p∈Spec A.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Corollary: equidimensional quotient of a regular local ring has equidimensional completion
If A is an equidimensional quotient of a regular local ring, then its completion is equidimensional.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Definition: formally equidimensional / quasi-unmixed
A Noetherian local ring is formally equidimensional (quasi-unmixed) when its completion is equidimensional.
Not formalized. P/H have Krull dimension, minimal primes, completion and localization, but no reusable equidimensional, formally-equidimensional, or formally-catenary interface matching the source definition.
Theorem: Theorem 31.6
If A is formally equidimensional Noetherian local, then: every A_p is formally equidimensional; for every ideal I, A/I is equidimensional iff formally equidimensional; an equidimensional local ring essentially of finite type over A is formally equidimensional; and A is universally catenary.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Definition: formally catenary local ring
A Noetherian local ring A is formally catenary if A/p is formally equidimensional for every prime p. Theorem 31.6 gives formally catenary ⇒ universally catenary.
Not formalized. P/H have Krull dimension, minimal primes, completion and localization, but no reusable equidimensional, formally-equidimensional, or formally-catenary interface matching the source definition.
Construction: completion of finite intermediate normalization rings
For a local domain R with normalization R′ and a finite intermediate R⊆S⊆R′, S is semilocal and its m-adic completion is S=R⊗_R S; inside the total quotient ring of R, one has R⊆S⊆R⊗_R R′.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Theorem: Theorem 31.7
For a Noetherian local ring A, the following are equivalent: A is formally catenary; A is universally catenary; A[X] is catenary.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Lemma: Theorem 31.7, Lemma 3
For a catenary local domain R whose completion has a minimal prime Q of dimension d strictly between 1 and dim R, each intermediate height 1,…,d−1 occurs among primes whose completed extension has a minimal prime above Q of the complementary dimension.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Lemma: Theorem 31.7, Lemma 4
Under the stated nonequidimensional-completion primary-decomposition hypotheses, one can choose b,c∈m and δ in the complementary primary components so that b−δ lies in the distinguished primary component, (b,δ)R=(b,c)R, and c/b is integral over R but not in R.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Lemma: Theorem 31.7, Lemma 5
With c/b from Lemma 4, the finite birational extension S=R[c/b] has a maximal ideal of height one.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Corollary: universal catenarity iff A[X] is catenary
A Noetherian ring A is universally catenary iff A[X] is catenary.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Corollary: low-dimensional catenarity
Every Noetherian ring of dimension at most two is catenary; every Noetherian ring of dimension at most one is universally catenary.
Not formalized. Targeted P/H/open searches found no catenary/universally-catenary predicate and no Ratliff prime-chain existence theorem; Krull-height infrastructure alone does not supply this source result.
Definition: formal fibre
For Noetherian local (A,m) with completion A, the fibre of A→A over p∈Spec A is called the formal fibre of A at p. Formal fibres of A/I are also formal fibres of A.
Not formalized. Ideal.Fiber and adic completion allow reconstruction, but no FormalFiber/equivalent declaration packages fibres of A→Â and the quotient compatibility in this row.
Definition: geometrically regular algebra over a field
A Noetherian k-algebra A is geometrically regular over k if A⊗_k k′ is regular for every finite field extension k′/k; equivalently this may be checked at maximal localizations.
Not formalized. P/H have regular rings, fibres, flatness and smooth/formally-smooth maps, but no geometrically-regular algebra or EGA regular-homomorphism predicate matching this unit.
Definition: regular homomorphism
A homomorphism A→B of Noetherian rings is regular if it is flat and every fibre B⊗_Aκ(p) is geometrically regular over κ(p).
Not formalized. P/H have regular rings, fibres, flatness and smooth/formally-smooth maps, but no geometrically-regular algebra or EGA regular-homomorphism predicate matching this unit.
Definition: G-ring
A Noetherian ring A is a G-ring if A_p→(A_p)^ is regular for every prime p; equivalently all formal fibres of all localizations are geometrically regular.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem: Theorem 32.1
Regular homomorphisms are transitive. If A→B→C has regular composite and B→C is faithfully flat, then A→B is regular.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem: Theorem 32.2
If A→B is faithfully flat and regular, then regularity, normality, reducedness, Cohen–Macaulayness and Gorensteinness are equivalent for A and B. If B is a G-ring, then A is a G-ring.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem: Theorem 32.3
Every complete Noetherian local ring is a G-ring.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem: Theorem 32.4
If A_m→(A_m)^ is regular for every maximal ideal m of a Noetherian ring A, then A is a G-ring.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem: Theorem 32.5
For a Noetherian semilocal ring A, it suffices for the G-ring property that for every finite A-algebra domain C, maximal m of C and B=C_m, each localization (B*)_Q with Q∩B=0 be regular. The source notes this condition is also necessary.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem: Theorem 32.6 (Mizutani)
If R is regular and the weak Jacobian condition holds in R[X_1,…,X_n] for every n≥0, then R is a G-ring.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Corollary: finite-type algebras over a field are G-rings
Every ring finitely generated over a field, and every localization of such a ring, is a G-ring.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Corollary: reducedness and normality pass to completion for essentially finite-type local rings
Local rings essentially of finite type over a field are G-rings; consequently reducedness and normality pass to their completions.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Example/remark: characteristic-zero WJ sources of G-rings
If a regular characteristic-zero ring R satisfies WJ, then its polynomial extensions are G-rings. In particular convergent power-series rings over R or C are G-rings.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Theorem/remark: G-rings under polynomial and power-series extension
The source records Grothendieck’s theorem that A a G-ring implies A[X] a G-ring; Rotthaus proved the formal-power-series analogue for semilocal A, while Nishimura produced a G-ring A with AX not a G-ring in general.
Not formalized. No P/H/open G-ring predicate or formal-fibre geometric-regularity theorem package was found; completion and smoothness APIs are not substitutes under strict semantics.
Definition: excellent and quasi-excellent rings
A Noetherian ring is excellent if it is universally catenary, is a G-ring, and Reg(B) is open for every finitely generated A-algebra B. It is quasi-excellent when the last two conditions hold.
Not formalized. No P/H/open excellent/quasi-excellent ring predicate or stability theorem was found; the defining G-ring and regular-locus interfaces are themselves absent.
Theorem/remark: stability and basic examples of excellence
The source records that the defining excellence conditions are stable under localization, finitely generated extension and quotient; for semilocal Noetherian rings the G-condition implies openness of regular loci; complete Noetherian local rings are excellent.
Not formalized. No P/H/open excellent/quasi-excellent ring predicate or stability theorem was found; the defining G-ring and regular-locus interfaces are themselves absent.
Definition: acceptable ring
Sharp’s acceptable rings are the Gorenstein analogue of excellent rings: formal fibres of all localizations are required to be Gorenstein and the Gorenstein loci replace regular loci in the openness condition.
Not formalized. No Sharp acceptable-ring formal-fibre/Gorenstein-locus interface was found in P/H/open compatible sources.
Theorem: Andre regularity theorem quoted in §32
If A→B is a local homomorphism of Noetherian local rings, A is quasi-excellent, and B is m_B-smooth over A, then the homomorphism is regular.
Not formalized. The theorem requires quasi-excellence, regular homomorphisms and m-smoothness; C10/C11 found no compatible source-level interfaces for these notions.
Theorem: dimension-of-intersection inequality
For P,P′ prime in R=k[X_1,…,X_n] and Q minimal over P+P′, dim R/Q≥dim R/P+dim R/P′−n, equivalently ht Q≤ht P+ht P′.
Not formalized. P has Krull height theorems and regular-local infrastructure, but no Serre intersection inequality ht Q ≤ ht P + ht P′ for arbitrary primes as stated here.
Theorem/remark: dimension-of-intersection inequality in regular local rings
The same height inequality holds in arbitrary regular local rings: equal characteristic follows via Cohen structure and the diagonal argument; the unramified mixed-characteristic case is analogous; Serre proved the general ramified case using intersection multiplicities.
Not formalized. P has Krull height theorems and regular-local infrastructure, but no Serre intersection inequality ht Q ≤ ht P + ht P′ for arbitrary primes as stated here.
Definition: derived normal ring
For a Noetherian domain A with fraction field K, its derived normal ring A′ is the integral closure of A in K.
Formalized. Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean::integralClosure; Mathlib/RingTheory/Localization/FractionRing.lean::FractionRing — For a domain A, integralClosure A (FractionRing A) is exactly Matsumura’s derived normal ring A′.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: finite integral closure in a finite separable extension
If A is a Noetherian normal domain with fraction field K, L/K is finite separable, and A′ is the integral closure of A in L, then A′ is a finite A-module.
Formalized. Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean::IsIntegralClosure.finite — IsIntegralClosure.finite exactly states finiteness over a Noetherian integrally closed domain for a finite separable extension of its fraction field.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: Noether normalization
If A=k[x_1,…,x_n] is a finitely generated k-algebra, there are algebraically independent y_1,…,y_r∈A such that A is integral over k[y_1,…,y_r].
Formalized. Mathlib/RingTheory/NoetherNormalization.lean::exists_integral_inj_algHom_of_fg, exists_finite_inj_algHom_of_fg — Pinned Noether normalization gives an injective polynomial-algebra map into A over which A is integral, indeed finite, matching the source lemma.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: finite normalization for affine domains
If A is a finitely generated integral domain over a field, then its derived normal ring is finite as an A-module; the source handles both separable and purely inseparable field-extension cases.
Not formalized. P has Noether normalization and finite integral closure for finite separable fraction-field extensions, but no checked theorem closes the purely inseparable case required by Matsumura’s all-characteristics result.
Theorem: finite normalization for complete local domains
If A is a complete Noetherian local domain, then its derived normal ring is finite over A.
Not formalized. P/H integral-closure APIs do not contain the complete-local finite-normalization theorem or the reduced-completion equivalences/counterexample package required by this unit.
Corollary: reduced completion implies finite normalization
If A is Noetherian local and its completion is reduced, then the integral closure of A in its total ring of fractions is finite over A.
Not formalized. P/H integral-closure APIs do not contain the complete-local finite-normalization theorem or the reduced-completion equivalences/counterexample package required by this unit.
Counterexample: nonreduced rings with a regular maximal-ideal element have nonfinite normalization
If A is nonreduced local and its maximal ideal contains a non-zero-divisor, then the integral closure in the total quotient ring is not finite over A.
Not formalized. P/H integral-closure APIs do not contain the complete-local finite-normalization theorem or the reduced-completion equivalences/counterexample package required by this unit.
Theorem: one-dimensional reduced-completion criterion
For a one-dimensional Noetherian local domain A, the completion is reduced iff the derived normal ring is finite over A.
Not formalized. P/H integral-closure APIs do not contain the complete-local finite-normalization theorem or the reduced-completion equivalences/counterexample package required by this unit.
Theorem: Rees reduced-completion criterion
A reduced Noetherian local ring A has reduced completion iff for every finite subset T of its total quotient ring, the integral closure of A[T] in that total quotient ring is finite over A[T].
Not formalized. P/H integral-closure APIs do not contain the complete-local finite-normalization theorem or the reduced-completion equivalences/counterexample package required by this unit.
Definition: Nagata ring
A Noetherian ring A is Nagata if for every prime P and finite field extension L/κ(P), the integral closure of A/P in L is finite over A/P. The source also records the equivalent formulation using geometrically reduced formal fibres and openness of normal loci for finite A-algebra domains.
Not formalized. No P/H/open Nagata/Japanese-ring predicate packages finite normalization in residue-field extensions together with the formal-fibre/normal-locus equivalence.
Theorem: Mori–Nagata integral closure theorem
For a Noetherian domain A, its derived normal ring A′ is a Krull ring; over every prime P of A only finitely many primes P′ of A′ occur, and each fraction field κ(P′) is finite over κ(P).
Not formalized. C04 established that P/H/open Mathlib has no general Krull-ring interface, so the source Krull normalization theorem with finite fibres/residue extensions has no route.
Corollary/remark: Noetherianity of normalization in dimension at most two
The derived normal ring of a Noetherian domain of dimension at most two is Noetherian, using Krull–Akizuki and Mori–Nishimura; Nagata constructed a dimension-three counterexample.
Not formalized. The Krull–Akizuki/Mori–Nishimura normalization theorem and dimension-three counterexample are absent from P/H/open compatible sources.