Chapter 10. I-smoothness
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 15 definitions, 28 theorems, 9 lemmas, 5 corollaries, 2 examples, 2 counterexamples, 1 construction and 3 remarks.
Of the 65 statements checked against Lean, 4 are formalized somewhere and 61 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 61 | 94% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 4 | 6% | Mathlib states and proves it. |
| checked in total | 65 |
- Canonical source block: FC13 Matsumura Chapter 10,
FC13-C10-U001–FC13-C10-U065, §§28–30, in canonical source-ID order from Foundational corpus units FC13 Matsumura. All 65 IDs are retrieved throughagent-memory, asserted once/in-order, and assigned exactly one route. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280. No project-owned adic smoothness, coefficient/Cohen-ring, p-basis, regular-locus, or weak-Jacobian interface closes a C10 unit, so C10 has noproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Native C10 coverage is narrow but exact: the full Eisenstein criterion U037, formal-smoothness local-to-global U042, local-to-global solvability of linear systems U043, and the fraction-field module-rank definition U050. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493. Targeted P/H/open searches found no source-level I-smooth/I-unramified/I-étale interface, geometrically regular local algebra predicate, coefficient/quasi-coefficient ring package, ramified regular-local predicate, regular locus, weak Jacobian condition, or p-basis/cofinite-field differential package. - Open PR #39289 (
7c2cce3eff4d42f292ba86215e7e3fa10735e925, Cohen structure theorem) and #35560 (1e4c8c2848f36bd73aea213044612c247b1ea91f, corollaries) were inspected at fixed revisions. They contain substantial Cohen-ring, residue-field lifting, flat-extension, and regular-presentation partials, but do not close Matsumura’s whole coefficient-ring bundles; the flat-extension branch also contains an unresolvedsorry. They are therefore evidence recorded inside unmatched rows, notreference-portroutes. - Strict bundle semantics were enforced. Ordinary formal smoothness into adically complete targets is not Matsumura’s I-smoothness; the pinned smooth locus does not close rows that also require regular-locus openness; and presentation-level Jacobian criteria are not substitutes for the rows bundling m-smoothness, regularity, p-bases, arbitrary derivations, or cofinite coefficient fields.
- Three nontrivial P assemblies were compile-checked in isolated Lean files before promotion: U037 descends prime divisibility from the fraction field after Eisenstein/Gauss; U042 uses the open smooth locus and maximal ideals; U043 applies
Submodule.mem_of_localization_maximalto the range of the coefficient map. - Route totals for C10:
mathlib4,project-existing0,package-import0,reference-port0,unmatched61.
Definition: I-smooth, I-unramified and I-etale
For an A-algebra B with I-adic topology, I-smoothness means continuous maps B→C/N lift across square-zero N; I-unramified means at most one lift; I-etale means both. For I=0 these are the 0-smooth/unramified/etale notions of §25.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Lemma: lifting from square-zero to complete targets
If B is I-smooth over A and C is N-adically complete, a continuous A-map B→C/N lifts successively to a continuous A-map B→C.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.1 (transitivity)
For A→B→B′ compatible with I- and I′-adic topologies, I-smoothness of B/A and I′-smoothness of B′/B imply I′-smoothness of B′/A; the same transitivity holds for unramifiedness.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.2 (base change)
If B is I-smooth over A and A′ is an A-algebra, then B⊗_A A′ is I(B⊗A′)-smooth over A′; likewise for I-unramifiedness.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Example: completion and smoothness
For a local ring (A,m) and completion Â,  is mÂ-etale over A. For k→A, A is m-smooth/unramified over k iff  is mÂ-smooth/unramified over k.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Example: formal power series are I-smooth
For B=AX_1,…,X_n and I=(X_1,…,X_n), B is I-smooth over A.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Definition: equal and unequal characteristic
A local ring is equicharacteristic iff it contains a field. Otherwise its residue field has characteristic p while the ring has characteristic 0 or p^n with n>1; this is unequal characteristic.
Not formalized. Pinned Mathlib has EqualCharZero and MixedCharZero, but no positive-characteristic equicharacteristic notion completing Matsumura’s classification (including characteristic p^n, n>1). The whole source definition is therefore not represented.
Definition: coefficient field and quasi-coefficient field
For equicharacteristic local (A,m,K), a coefficient field K′⊆A maps isomorphically to K=A/m. A quasi-coefficient field K′⊆A is one for which K is 0-etale over the image of K′.
Not formalized. Pinned/current/open Mathlib has residue fields and formal étaleness, and PR #39289 proves selected coefficient-field/Cohen lifting statements for complete rings, but no source-level coefficient/quasi-coefficient-field object and no theorem closes this entire unit.
Theorem: Theorem 28.3
Every equicharacteristic local ring has a quasi-coefficient field; if complete, it has a coefficient field. If the residue field is separable over k⊆A one may choose a quasi-coefficient field containing k, and every quasi-coefficient field extends uniquely to a coefficient field of the completion.
Not formalized. Pinned/current/open Mathlib has residue fields and formal étaleness, and PR #39289 proves selected coefficient-field/Cohen lifting statements for complete rings, but no source-level coefficient/quasi-coefficient-field object and no theorem closes this entire unit.
Lemma: regularity versus m-smoothness
If a Noetherian local ring A containing k is m-smooth over k, then A is regular. Conversely, if A is regular and its residue field is separable over k, then A is m-smooth over k.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Definition: I-smoothness relative to a base k
For k→A→B, B is I-smooth over A relative to k if every continuous A-algebra map B→C/N that admits a k-algebra lifting also admits an A-algebra lifting.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.4
For k→A→B with I-adic B, relative I-smoothness over A is equivalent to surjectivity Der_k(B,N)→Der_k(A,N) for every I-power-torsion B-module N, and equivalent to the stated splitting of Ω_{A/k}⊗B/Iv→Ω_{B/k}⊗B/Iv for every v.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.5
If B is I-smooth over A and B_0=B/I, then Ω_{B/A}⊗_B B_0 is a projective B_0-module.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Lemma: lifting a split map from modulo I
Let u:L→M be B-linear with M projective. If I is nilpotent, or L finite with I⊆rad(B), then u has a left inverse iff L/IL→M/IM has a left inverse.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.6
If k→A→B, B is I-smooth over k, and B_0=B/I, then B is I-smooth over A iff Ω_{A/k}⊗A B_0→Ω{B/k}⊗_B B_0 has a B_0-linear left inverse.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Corollary: differential criterion for m-smoothness of a regular local ring
If (A,m,K) is regular local containing k, then A is m-smooth over k iff Ω_k⊗_k K→Ω_A⊗_A K is injective.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Definition: geometrically regular local k-algebra
A Noetherian local k-algebra A is geometrically regular over k if A⊗_k k′ is regular for every finite field extension k′/k.
Not formalized. Targeted P/H/open searches found no GeometricallyRegular local-algebra predicate or Faltings m-smoothness equivalence. Ordinary formal smoothness and geometric reducedness are insufficient for the source bundle.
Theorem: Theorem 28.7 (Faltings criterion)
For a Noetherian local ring A containing k, A is m-smooth over k iff A is geometrically regular over k.
Not formalized. Targeted P/H/open searches found no GeometricallyRegular local-algebra predicate or Faltings m-smoothness equivalence. Ordinary formal smoothness and geometric reducedness are insufficient for the source bundle.
Definition: discrete module and continuous symmetric 2-cocycle
A B-module N is discrete for the I-adic topology if I^vN=0 for some v. A continuous symmetric 2-cocycle f:B×B→N is A-bilinear, symmetric, satisfies the associativity cocycle identity, and vanishes when either argument lies in a high I-power; it splits if f=δg for a continuous A-linear g:B→N.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.8
If B is I-smooth over A, every continuous symmetric 2-cocycle with values in a discrete B-module splits. Conversely, if B/I^n is A-projective for infinitely many n and all such cocycles split, then B is I-smooth over A.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.9 (Grothendieck)
For a local map of Noetherian local rings A→B with closed fibre B_0=B/mB, B is n-smooth over A iff B is A-flat and B_0 is n_0-smooth over the residue field.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Theorem: Theorem 28.10
If (A,m,k) is local, B is A-flat, and B⊗_A k is 0-smooth over k, then B is mB-smooth over A.
Not formalized. Smooth/AdicCompletion.lean proves that ordinary formally smooth algebras lift maps into adically complete targets, but Mathlib has no source-level I-smooth/I-unramified/I-étale topology-dependent notion. Consequently this unit cannot be represented without first formalizing Matsumura’s adic interface.
Definition: p-ring
A DVR of characteristic zero whose maximal ideal is generated by the prime p is called a p-ring.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Theorem: Theorem 29.1
If (A,tA,k) is a DVR and K/k any field extension, there exists a DVR (B,tB,K) containing A with residue field K.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package. Open PR #39289 (7c2cce3eff4d42f292ba86215e7e3fa10735e925) and #35560 (1e4c8c2848f36bd73aea213044612c247b1ea91f) contain Cohen-ring/flat-extension/regular-presentation partials, but do not close the whole source package; the flat-extension development also contains an unresolved sorry.
Remark: flat residue-field extension of a Noetherian local ring
The source records the EGA generalization: for Noetherian local (A,m,k) and field extension K/k, there is a Noetherian flat local A-algebra B with rad(B)=mB and residue field K.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package. Open PR #39289 (7c2cce3eff4d42f292ba86215e7e3fa10735e925) and #35560 (1e4c8c2848f36bd73aea213044612c247b1ea91f) contain Cohen-ring/flat-extension/regular-presentation partials, but do not close the whole source package; the flat-extension development also contains an unresolved sorry.
Theorem: Theorem 29.2
Let A be complete local, R a p-ring with residue field k, and k→K=A/m a field map. Then there is a local homomorphism R→A inducing the prescribed residue-field map.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Corollary: complete p-ring uniqueness
A complete p-ring is uniquely determined up to isomorphism by its residue field.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Definition: coefficient ring
For a complete local ring A of unequal characteristic with residue characteristic p, a coefficient ring A_0⊆A is a complete Noetherian local subring with maximal ideal pA_0 and residue field A_0/pA_0≅A/m. Coefficient fields are included as coefficient rings in equal characteristic.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Theorem: Theorem 29.3
Every complete local ring A with residue characteristic p has a coefficient ring. In characteristic zero it is a complete p-ring; in characteristic p^n it is a quotient R/p^nR of a complete p-ring R.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package. Open PR #39289 (7c2cce3eff4d42f292ba86215e7e3fa10735e925) and #35560 (1e4c8c2848f36bd73aea213044612c247b1ea91f) contain Cohen-ring/flat-extension/regular-presentation partials, but do not close the whole source package; the flat-extension development also contains an unresolved sorry.
Theorem: Theorem 29.4
For complete local rings: finitely generated maximal ideal implies Noetherian; every Noetherian complete local ring is a quotient of a regular local ring and hence universally catenary; and, if equicharacteristic or an unequal-characteristic domain, it is finite over a complete regular local subring with the same residue field.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package. Open PR #39289 (7c2cce3eff4d42f292ba86215e7e3fa10735e925) and #35560 (1e4c8c2848f36bd73aea213044612c247b1ea91f) contain Cohen-ring/flat-extension/regular-presentation partials, but do not close the whole source package; the flat-extension development also contains an unresolved sorry.
Counterexample: finite regular subring can fail in mixed characteristic with zero divisors
The source gives complete mixed-characteristic rings such as RX/(pX) showing Theorem 29.4(iii) may fail without the domain/nonzerodivisor hypothesis.
Not formalized. No checked P/H/open Lean development packages the explicit RX/(pX) obstruction to the finite regular-subring statement.
Definition: quasi-coefficient ring
For local (A,m,K) with char K=p, a quasi-coefficient ring S⊆A is Noetherian local with maximal ideal pS and K 0-etale over S/pS.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Theorem: Theorem 29.5
If C⊆A is Noetherian local with maximal ideal pC and K=A/m is separable over C/pC, then A contains a quasi-coefficient ring S⊇C. If A is flat over C, it is flat over S.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Theorem: Theorem 29.6
Given a quasi-coefficient ring S of a local ring A, its image in the completion  is contained in a unique coefficient ring of Â.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Definition: ramified and unramified regular local rings
For unequal-characteristic local (A,m,K) with char K=p, A is ramified if p∈m² and unramified if p∉m²; equicharacteristic local rings are also called unramified.
Not formalized. Pinned/current Mathlib has mixed-characteristic and regular-local-ring infrastructure but no source-level predicate defined by p∈m² versus p∉m² (with equicharacteristic included as unramified).
Theorem: Theorem 29.7
Every unramified complete regular local ring is a formal power series ring over a coefficient field or a complete p-ring.
Not formalized. Pinned/current Mathlib has DVR, completion, residue-field, p-adic, and local-ring primitives, but not Matsumura’s p-ring/coefficient-ring/quasi-coefficient-ring theorem package.
Lemma: Eisenstein irreducibility criterion
For monic f=Xn+a_1X{n−1}+⋯+a_n, if all a_i lie in a prime P but a_n∉P², then f is irreducible. If A is integrally closed, (f) is prime in A[X].
Formalized. Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean::IsEisensteinAt, Monic.isEisensteinAt_of_mem_of_notMem, IsEisensteinAt.irreducible; Mathlib/RingTheory/Polynomial/GaussLemma.lean::Monic.irreducible_iff_irreducible_map_fraction_map; Mathlib/Algebra/Polynomial/Div.lean::map_dvd_map; Mathlib/RingTheory/Ideal/Maximal.lean::span_singleton_prime — Pinned Eisenstein gives irreducibility from the stated coefficient conditions. For integrally closed A, Gauss transfers irreducibility to Frac(A)[X], where the polynomial is prime; map_dvd_map for a monic divisor descends the prime divisibility condition to A[X], hence (f) is prime. The full assembly was compile-checked against P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: Eisenstein extension
For normal local (A,m), an extension A[X]/(f) defined by an Eisenstein polynomial with coefficients in m and constant term outside m² is an Eisenstein extension; it is a local integral domain with the same residue field as A.
Not formalized. Pinned Mathlib has Polynomial.IsEisensteinAt but no source-level Eisenstein-extension object, local/residue-field structure theorem, or ramified complete-regular-local classification needed for this unit.
Theorem: Theorem 29.8
An Eisenstein extension of a regular local ring is regular. Every ramified complete regular local ring is an Eisenstein extension of an unramified complete regular local subring containing its coefficient ring.
Not formalized. Pinned Mathlib has Polynomial.IsEisensteinAt but no source-level Eisenstein-extension object, local/residue-field structure theorem, or ramified complete-regular-local classification needed for this unit.
Theorem: Theorem 30.1 (Nagata-Zariski-Lipman)
For complete Noetherian local A containing Q, if x_1,…,x_r∈m and derivations D_1,…,D_r have det(D_ix_j) a unit, then A=Cx_1,…,x_r for a subring C and is (x)-smooth over C. If the A-span of the D_i is a Lie algebra, C is exactly the common kernel of the D_i.
Not formalized. Pinned/current Mathlib has ordinary derivations and formal power series, but no Nagata–Zariski–Lipman decomposition or common-kernel coefficient-field theorem matching the source.
Corollary: derivation criterion for regularity and coefficient fields
If A is reduced n-dimensional local containing Q, Â is reduced, and there are n derivations and n elements with invertible derivative matrix, then A is regular and the elements are a regular system of parameters; under the Lie condition the common kernel is a coefficient field of Â.
Not formalized. Pinned/current Mathlib has ordinary derivations and formal power series, but no Nagata–Zariski–Lipman decomposition or common-kernel coefficient-field theorem matching the source.
Theorem: Theorem 30.2
If A is finitely generated over a field k and every maximal localization A_p is 0-smooth over k, then A is 0-smooth over k.
Formalized. Mathlib/RingTheory/FinitePresentation.lean::FinitePresentation.of_finiteType; Mathlib/RingTheory/Smooth/Locus.lean::smoothLocus_eq_univ_iff, isOpen_smoothLocus; Mathlib/Topology/Inseparable.lean::IsOpen.stableUnderGeneralization; Mathlib/RingTheory/Ideal/Maximal.lean::exists_le_maximal — For a finite-type k-algebra, finite presentation is automatic. If every maximal localization is formally smooth, every maximal point lies in the open smooth locus; openness makes the locus stable under generalization, and every prime lies below a maximal ideal, so the locus is all of Spec. smoothLocus_eq_univ_iff then gives formal smoothness. Compile-checked against P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Lemma: local-to-global solvability of linear systems
For A→B and B-module N, a finite linear system with coefficients in B and constants in N has a global solution if it has a solution after localizing at every maximal ideal of A.
Formalized. Mathlib/RingTheory/LocalProperties/Submodule.lean::Submodule.mem_of_localization_maximal — A finite linear system is membership of the constant vector in the range of its coefficient linear map. Submodule.mem_of_localization_maximal says exactly that membership in a submodule can be checked at every maximal localization, yielding the global solution. This range formulation was compile-checked against P.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 30.3 (Jacobian/smoothness criterion)
For S=k[X_1,…,X_n], I⊆P, R=S_P, A=R/IR, ht(IR)=r and I generated by f_i, the source gives equivalent conditions: a rank-r Jacobian condition, 0-smoothness, m-smoothness, Ω_{A/k} free of rank n−r, and A a domain with separable fraction field and Ω_{A/k} free.
Not formalized. Pinned Mathlib has presentation Jacobians and Algebra.FormallySmooth.iff_injective_* local Jacobian criteria, but this source unit additionally bundles m-smoothness, regularity, arbitrary derivations and/or p-basis/cofinite-field clauses not represented by the available API.
Remark: perfect-residue-field simplification of Theorem 30.3
If k is perfect, or the residue field is separable over k, m-smoothness in Theorem 30.3 is equivalent to regularity; over imperfect k this equivalence need not hold.
Not formalized. Pinned Mathlib has presentation Jacobians and Algebra.FormallySmooth.iff_injective_* local Jacobian criteria, but this source unit additionally bundles m-smoothness, regularity, arbitrary derivations and/or p-basis/cofinite-field clauses not represented by the available API.
Definition: Jacobian matrix for arbitrary derivations
For f_1,…,f_t∈A, derivations D_1,…,D_s and prime P, J(f_1,…,f_t;D_1,…,D_s)(P) is the matrix (D_if_j mod P) over A/P.
Not formalized. Pinned Mathlib has presentation Jacobians and Algebra.FormallySmooth.iff_injective_* local Jacobian criteria, but this source unit additionally bundles m-smoothness, regularity, arbitrary derivations and/or p-basis/cofinite-field clauses not represented by the available API.
Theorem: Theorem 30.4
If R is regular, I⊆P and ht(IR_P)=r, every Jacobian matrix built from elements of I and derivations has rank at most r at P. If an r×r derivative determinant is nonzero mod P, then IR_P is generated by those r elements and R_P/IR_P is regular.
Not formalized. Pinned Mathlib has presentation Jacobians and Algebra.FormallySmooth.iff_injective_* local Jacobian criteria, but this source unit additionally bundles m-smoothness, regularity, arbitrary derivations and/or p-basis/cofinite-field clauses not represented by the available API.
Theorem: Theorem 30.5 (Zariski)
For S=k[X_1,…,X_n] in characteristic p, regularity of A=S_P/IS_P is equivalent to a rank-r Jacobian criterion using finitely many derivations associated to a p-basis of k together with the ∂/∂X_i; it is also equivalent to existence of a cofinite subfield k′⊆k over which Ω_{A/k′} is free with the stated rank.
Not formalized. Pinned Mathlib has presentation Jacobians and Algebra.FormallySmooth.iff_injective_* local Jacobian criteria, but this source unit additionally bundles m-smoothness, regularity, arbitrary derivations and/or p-basis/cofinite-field clauses not represented by the available API.
Corollary: openness of smooth and regular loci for finite-type k-algebras
For B=k[X_1,…,X_n]/I, both the 0-smooth locus over k and Reg(B) are open in Spec B.
Not formalized. Algebra.isOpen_smoothLocus proves openness of the formal-smooth locus for finite presentations. No P/H/open source-level regular locus or theorem supplies the second half of Matsumura’s bundled row, so strict bundle semantics leaves it unmatched.
Definition: rank of a module over a domain
For a domain A with fraction field L and A-module M, rank_A M=dim_L(M⊗_A L).
Formalized. Mathlib/RingTheory/Localization/BaseChange.lean::LocalizedModule.equivTensorProduct; Mathlib/LinearAlgebra/Dimension/Localization.lean::IsLocalizedModule.lift_rank_eq — Localization at the nonzero elements is linearly equivalent to Frac(A)⊗_A M, and IsLocalizedModule.lift_rank_eq identifies its fraction-field dimension with Module.rank A M, exactly Matsumura’s definition (up to universe lifts).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 30.6 (Nomura)
For equicharacteristic regular local R with quasi-coefficient field k and completion R=Kx_1,…,x_n, Der_k(R) is free on ∂/∂x_i. Five conditions on Der_k(R)—stability of R under these partials, dual coordinate systems, invertible derivative matrix, freeness of rank n, and rank n—are equivalent.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Definition: weak Jacobian condition (WJ)
For regular R and P of height r, (WJ) at P means there exist r derivations and r elements of P with derivative determinant nonzero mod P. (WJ) in R means this holds at every prime; (WJ)_k restricts to k-derivations.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Theorem: Theorem 30.7
If (A,m) is an n-dimensional Noetherian local domain containing Q and k⊆A has residue transcendence degree r<∞, then Der_k(A) embeds in A^{n+r}; hence it is finite and has rank at most n+r.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Counterexample: imperfect residue fields can enlarge derivation rank
In characteristic p, the source gives a one-dimensional local domain k[X,Y]_(x,y)/(Xp+aYp) with a∉k^p but rank Der_k(A)=2.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Theorem: Theorem 30.8
For a regular local ring R containing Q with quasi-coefficient field k, (WJ)_k at the maximal ideal, rank Der_k(R)=dim R, and (WJ)_k at every prime are equivalent. Under these conditions derivations descend surjectively to R/P and rank Der_k(R/P)=dim R/P.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Definition: cofinite and directed families of subfields
A subfield k′⊆k is cofinite if [k:k′]<∞. A family {k_α} is directed downward if any two contain a third member contained in their intersection.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Construction: directed cofinite family from a p-basis
For k⊆K in characteristic p, choosing a p-basis B of K/k and deleting finitely many basis elements produces a directed family of cofinite intermediate fields k_α with intersection k(K^p).
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Lemma: Lemma 3
If k=∩k_α for a directed family of subfields of K and v_1,…,v_n are k-linearly independent in a K-vector space, then they remain independent over some k_α.
Not formalized. Pinned/current Mathlib has ordinary derivations, module rank, and presentation Jacobians, but no source-level weak-Jacobian condition or the Nomura/Nagata derivation-rank theorem package required by this unit.
Lemma: Lemma 4
For a directed family k⊆k_α⊆K in characteristic p, intersection ∩k_α(Kp)=k(Kp) is equivalent to injectivity Ω_{K/k}→lim Ω_{K/k_α}, to eventual p-independence of each finite p-independent set, and to the corresponding p-basis condition.
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Lemma: Lemma 5
Under the hypotheses of Lemma 4, the intersection property ∩k_α(Kp)=k(Kp) persists after passing to an extension L/K that is separable or finitely generated.
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Lemma: Lemma 6
For a directed family of cofinite K_α⊆K with intersection K^p and finite L/K, the rank of Ω_{L/K′} stabilizes for sufficiently deep finite intermediate subfields K′⊆K_α.
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Theorem: Theorem 30.9 (Nagata)
For S=kY_1,…,Y_n in characteristic p and prime P, a suitable cofinite subfield k_α in any directed family with intersection k^p makes rank Der_{k′}(S/P)=dim(S/P)+rank Der_{k′}(k) for every finite intermediate k^p⊆k′⊆k_α.
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Theorem: Theorem 30.10 (Nagata Jacobian criterion)
For S=kX_1,…,X_n in characteristic p, I⊆P and A=S_P/IS_P, A is regular iff a rank-ht(I) Jacobian condition holds using finitely many coefficient derivations from a p-basis of k together with the formal partial derivatives.
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Remark: separated module of differentials in the power-series criterion
Because Ω for a power-series ring need not be finite, the source replaces it by its associated separated module; Hom into separated modules is unchanged, and the separated Ω-form of Theorem 30.5 is equivalent to Nagata’s criterion.
Not formalized. C09 established that P/H/open Mathlib has no reusable p-basis/p-independence or Hasse–Schmidt-style coefficient-derivation interface. The directed-cofinite-field and separated-differential arguments in this source unit therefore have no compatible route.
Corollary: regular locus of a complete Noetherian local ring is open
For every complete Noetherian local ring A, Reg(A) is open in Spec A.
Not formalized. Pinned/current/open Mathlib has no regularLocus object or theorem proving its openness for complete Noetherian local rings. Cohen-structure PRs provide only partial structural inputs and do not close this corollary.