Chapter 8. Flatness revisited
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 5 definitions, 23 theorems, 1 lemma, 5 corollaries, 2 counterexamples, 2 constructions, 3 remarks, 1 formula and 1 other statements.
Of the 43 statements checked against Lean, 2 are formalized somewhere and 41 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| not formalized | 41 | 95% | A documented search found no Lean statement of it anywhere. |
| in Mathlib | 2 | 5% | Mathlib states and proves it. |
| checked in total | 43 |
- Canonical source block: FC13 Matsumura Chapter 8,
FC13-C08-U001–FC13-C08-U043, §§22–24, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves all 43 units throughagent-memory, asserts exact order/uniqueness, and assigns one route per unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280(Lean 4.33.0, Apache-2.0). No project-owned API covers a whole C08 source unit beyond the upstream primitives, so C08 has noproject-existingroute. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, Lean 4.33.0, Apache-2.0. Two source units have complete native assemblies: U006 via height additivity + flat going down + fibre localization, and U036 via Noetherian finite type⇒finite presentation + flat going down + Chevalley openness. - Current Mathlib was refreshed 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493(Lean 4.34.0-rc2). Open-PR searches for Serre conditions, miracle flatness, generic freeness and flat loci were negative. The CM/Gorenstein PR stack from FC13 C06 was searched for flat/base-change/fibre theorems; no exact C08 flat-family owner was found. - Search channels used project source, P, H/current/open Mathlib, source/docs, Loogle/LeanSearch-oriented repository tooling, Reservoir/indexed discovery, and GitHub-wide Lean-code search. Literal searches for “ideal-separated”, “miracle flatness”, “Serre condition”, and source-shaped generic freeness produced no compatible owner.
- Strict bundle semantics were enforced. U005 is not credited from generic associated-graded definitions; U012–U029 are not inferred from separate CM/Gorenstein/flat definitions; U030 is not credited from a derivable tensor/quotient comparison without an exported fibre equivalence; U035 is not replaced by the free locus; and the Nagata-criterion rows U034/U038–U043 are kept distinct from generic topology/local-property machinery.
- Route totals for C08:
mathlib2,project-existing0,package-import0,reference-port0,unmatched41.
Theorem: Theorem 22.1
Let B be a Noetherian A-algebra, M finite over B, and J⊆rad(B). If M/J^{n+1}M is flat over A for every n≥0, then M is flat over A.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Theorem: Theorem 22.2
If B is a Noetherian A-algebra, M finite over B, b∈rad(B) is M-regular, and M/bM is A-flat, then M is A-flat.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Definition: I-adically ideal-separated module
An A-module M is I-adically ideal-separated if a⊗_A M is separated for the I-adic topology for every finitely generated ideal a of A. A finite B-module has this property when B is Noetherian and IB⊆rad(B).
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Construction: graded comparison map for I-adic flatness
For A_n=A/I^{n+1}, M_n=M/I^{n+1}M, the standard maps (In/I{n+1})⊗{A_0}M_0→InM/I{n+1}M assemble to gr_I(A)⊗{A_0}M_0→gr_I(M).
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Theorem: Theorem 22.3 (local flatness criterion)
If I is nilpotent, or A is Noetherian and M I-adically ideal-separated, then A-flatness of M is equivalent to the listed Tor, reduction, associated-graded, and flatness-mod-I^{n+1} conditions; the theorem also records which implications hold without the separation hypothesis.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Theorem: Theorem 22.4
For a local map of Noetherian local rings A→B and finite B-module M, A-flatness is equivalent to flatness after B-adic completion/base extension in the two stated forms; equivalently it may be checked on all m-adic reductions.
Formalized. Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean::Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown; Mathlib/RingTheory/Ideal/GoingDown.lean::Algebra.HasGoingDown.of_flat; Mathlib/RingTheory/Ideal/Height.lean::IsLocalRing.maximalIdeal_height_eq_ringKrullDim; Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean::Ideal.Fiber.localizationAlgEquivQuotient — Flatness supplies going down. Applying the pinned height-additivity theorem to the maximal ideals of the local map and identifying the relative term with the closed-fibre local quotient gives dim B = dim A + dim(B/mB).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Theorem: Theorem 22.5
For a local homomorphism A→B, finite B-modules M,N and u:M→N with N A-flat, u is injective with A-flat cokernel iff u⊗_A k is injective on the closed fibre.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Corollary: regular-sequence criterion across a flat local map
For finite M over B, a sequence x_1,…,x_n in the maximal ideal is M-regular with flat final quotient over A iff M is A-flat and its images in the closed fibre form an (M⊗k)-sequence.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Theorem: Theorem 22.6
For Noetherian A, Noetherian A-algebra B and finite A-flat B-module M, if b∈B is regular on every fibre M/(P∩A)M over maximal P of B, then b is M-regular and M/bM is A-flat.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Corollary: primitive polynomial/power-series hypersurface flatness
If f in A[X_1,…,X_n] or AX_1,…,X_n has coefficients generating the unit ideal of Noetherian A, then f is a non-zero-divisor and the quotient by f is A-flat.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Remark: flatness of graded modules
For a G-graded ring R and graded module M, ordinary R-flatness is equivalent to exactness of tensoring graded exact sequences and to flatness tested against homogeneous ideals; the source records the corresponding graded flatness criteria.
Not formalized. Pinned/current Mathlib has flatness, faithfully-flat, adic, regular-sequence and associated-graded-adjacent infrastructure, but targeted source/open/external searches found no declaration with all hypotheses and conclusions of this Matsumura unit. Constituent flatness lemmas are not credited as a bundled theorem.
Formula: dimension formula for a flat local map
For a flat local homomorphism of Noetherian local rings A→B with closed fibre F=B/mB, dim B=dim A+dim F.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.1 (miracle flatness)
If A is regular local, B is Cohen-Macaulay, and dim B=dim A+dim(B/mB), then a local homomorphism A→B is flat.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Corollary: geometric miracle flatness criterion
For a morphism Y→X of irreducible algebraic k-schemes, if X is regular, Y Cohen-Macaulay, closed points map to closed points, and all closed fibres have the expected constant dimension, then the morphism is flat.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.2
For A→B Noetherian, A-module E and B-module G flat over A: associated primes of G/pG lie over p, and Ass_B(E⊗_A G) is the union over p∈Ass_A(E) of Ass_B(G/pG).
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.3
For a local map A→B, finite A-module M, finite B-module N flat over A, depth_B(M⊗_A N)=depth_A M+depth_B(N/mN).
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Corollary: depth and Cohen-Macaulayness in flat local families
For a flat local map A→B with closed fibre F, depth B=depth A+depth F; consequently B is Cohen-Macaulay iff both A and F are Cohen-Macaulay.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.4
For a flat local homomorphism A→B of Noetherian local rings with closed fibre F, B is Gorenstein iff A and F are both Gorenstein.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.5
If A is Gorenstein, then A[X] and AX are Gorenstein.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.6
If A is a Gorenstein ring containing a field k and K/k is a finitely generated field extension, then A⊗_k K is Gorenstein.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Remark: CM and complete-intersection analogues
Theorems 23.5–23.6 remain true with Cohen-Macaulay in place of Gorenstein; the corresponding complete-intersection statements follow from the complete-intersection version of the flat local theorem.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.7
For a flat local map A→B with closed fibre F: regularity of B implies regularity of A; if A and F are regular, then B is regular.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Counterexample: regular total space can have singular closed fibre
The flat inclusion k[x²](x²)⊂k[x](x) has regular total ring but closed fibre k[x]/(x²), which is nonreduced and singular.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Definition: Serre conditions (Ri) and (Si)
For Noetherian A, (R_i) means A_P is regular for every prime P of height at most i-1; (S_i) means depth A_P is at least min(ht P,i) for every prime P.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Comparison: basic Serre-condition interpretations
(S_0) always holds; (S_1) says there are no embedded associated primes; (R_0)+(S_1) is equivalent to reducedness; satisfying all (S_i) is equivalent to Cohen-Macaulayness. For a domain, (S_1) is equivalent to every prime divisor of a nonzero principal ideal having height one.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.8 (Serre normality criterion)
A Noetherian ring is normal iff it satisfies (R_1) and (S_2).
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Theorem: Theorem 23.9
For a flat local homomorphism A→B and i≥0: (R_i) and (S_i) descend from B to A; if A and all fibre rings satisfy (R_i), respectively (S_i), then B does too.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Corollary: normality and reducedness in flat local families
Under a flat local homomorphism, normality or reducedness descends from B to A; if A and every fibre are normal, respectively reduced, then B is normal, respectively reduced.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Counterexample: normal base and closed fibre do not force normal total space
The source notes examples of normal Noetherian local rings whose completion is nonnormal, showing that normality of the base and closed fibre alone does not force normality of B.
Not formalized. No pinned/current/open declaration was found for this exact flat-family depth/Serre/normality theorem. The open Cohen–Macaulay and Gorenstein branches inspected for FC13 C06 contain definitions/localization/completion results but no matching flat-fibre theorem; generic flat/going-down infrastructure is strictly weaker.
Construction: fibres after quotienting the base
If A′→B′ and I⊲A′, set A=A′/I and B=B′/IB′. For p′⊇I corresponding to p∈Spec A, the fibre of A′→B′ over p′ canonically equals the fibre of A→B over p.
Not formalized. Pinned Ideal.Fiber.algEquivQuotient identifies a fibre with a localized quotient and quotient/tensor APIs make the source comparison derivable, but no checked declaration packages the canonical equality of fibres before and after the specified base quotient. Strict mapping leaves the construction unmatched.
Theorem: generic freeness for finite modules
If A is a Noetherian domain and M is finite, there exists 0≠a∈A such that M_a is a free A_a-module.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Lemma: one-generator algebra filtration lemma
If B is Noetherian, C=B[x], E finite over C, and F⊆E finite over B with CF=E, then E/F has an exhaustive filtration whose successive quotients come from only finitely many isomorphism classes of finite B-modules.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Theorem 24.1 (Hochster-Roberts generic freeness)
Let A be a Noetherian domain, R a finitely generated A-algebra, S a finitely generated R-algebra, E finite over S, M⊆E finite over R, and N⊆R finite over A. For D=E/(M+N), some nonzero a∈A makes D_a a free A_a-module.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Theorem 24.2 (topological Nagata criterion)
For Noetherian A, a subset U⊆Spec A is open iff it is stable under generalization and, for every P∈U, U contains a nonempty open subset of V(P).
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Theorem 24.3
If A is Noetherian, B a finitely generated A-algebra, and M finite over B, then {P∈Spec B | M_P is A-flat} is open.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Remark: finite-type flat maps are open
If A is Noetherian and B is a finitely generated flat A-algebra, the map Spec B→Spec A is open.
Formalized. Mathlib/RingTheory/FinitePresentation.lean::RingHom.FinitePresentation.of_finiteType; Mathlib/RingTheory/Ideal/GoingDown.lean::Algebra.HasGoingDown.of_flat; Mathlib/RingTheory/Spectrum/Prime/Chevalley.lean::PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation — Over a Noetherian source, finite type is equivalent to finite presentation. Flatness gives going down, and the pinned Chevalley theorem then states that the induced map on prime spectra is open, exactly the source remark.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d
Definition: local property loci
For a property P of local rings, P(A)={p∈Spec A | A_p has P}. The source writes Reg(A), CI(A), Gor(A), and CM(A) for the regular, complete-intersection, Gorenstein, and Cohen-Macaulay loci.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Definition: ring-theoretic Nagata criterion (NC)
A local-ring property P satisfies (NC) if for every Noetherian A, whenever P(A/p) contains a nonempty open subset of Spec(A/p) for every prime p, the locus P(A) is open.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Theorem 24.4 (Nagata)
The Nagata criterion holds for regular local rings; hence the regular locus is open under the criterion’s hypotheses.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Theorem 24.5
The Nagata criterion holds for Cohen-Macaulay local rings.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Definition: normal flatness along a closed subset
For Noetherian A, I⊲A, B=A/I, Y=V(I), and finite M, M is normally flat along Y when gr_I(M)=⊕InM/I{n+1}M is flat over B. If B is local, this is equivalent to every graded piece being B-free.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Theorem 24.6
The Nagata criterion holds for Gorenstein local rings.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.
Theorem: Greco-Marinari complete-intersection Nagata criterion
The source records that the Nagata criterion also holds for complete-intersection local rings.
Not formalized. Targeted pinned/current/open Mathlib and GitHub-wide Lean searches found no source-level declaration for this generic-freeness/Nagata/locus notion. Module.freeLocus and other local-property infrastructure cover only adjacent special cases and are not promoted by name or derivability alone.