Chapter 3. Properties of extension rings
FC13 — Matsumura, Commutative Ring Theory.
This chapter contains 13 definitions, 39 theorems, 2 lemmas, 4 corollaries, 12 examples, 2 constructions and 1 remark.
Of the 73 statements checked against Lean, 40 are formalized somewhere and 33 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 39 | 53% | Mathlib states and proves it. |
| not formalized | 33 | 45% | A documented search found no Lean statement of it anywhere. |
| in another Lean project | 1 | 1% | Some other Lean development has it; using it means porting that code. |
| checked in total | 73 |
- Canonical source block: FC13 Matsumura Chapter 3,
FC13-C03-U001–FC13-C03-U073, §§7–9 including the appendix to §7, in canonical source-ID order from Foundational corpus units FC13 Matsumura. The generator retrieves the promoted catalogue throughagent-memory, asserts all 73 IDs occur exactly once and in order, and emits exactly one Sweep-II route per unit. - Project-first inspection used
A=3b2239e161592472b34e02ad3b7da308f9ce7280on Lean 4.33.0, Apache-2.0. Relevant project additions includeLeanCategories/Algebra/ZariskiRing.leanand ring-level adic-completion topology support. They were treated as owners only when they cover an entire source unit; in particular the project Zariski-ring predicate does not cover all of U053’s terminology/invariance/example bundle, so no row is promoted merely because a partial wrapper exists. - Pinned Mathlib is
P=db584cd6d46c92f209a44c0f1c829460d327499d, repositoryleanprover-community/mathlib4, Apache-2.0, Lean 4.33.0, directly project-compatible. The generator asserts the local checkout is exactly P and verifies every cited pinned path/token. Prior FC04 Artin–Rees/completion source-shaped assemblies against this same P were reused only where the FC13 hypotheses and conclusions coincide (notably U043–U048). - Current Mathlib was refreshed independently on 2026-09-07 to
H=e281a66114fe17935e6ea7917a01b714d0c1e493, repositoryleanprover-community/mathlib4, Apache-2.0, Lean 4.34.0-rc2. Open-PR searches were concentrated on purity, Hensel factorization, completion Noetherianity/topology, secondary completion packages, Galois conjugacy of primes, and openness of integral extensions. PR #38331 supplies Noetherianity of adic completion but does not close the larger U050/U055 bundles. - Search channels used project source; pinned P; current H; open Mathlib PRs; Loogle/LeanSearch/Mathlib docs via the repository tooling; Lean Reservoir/indexed discovery; and discoverable external Lean repositories via GitHub code search. No compatible package-import route was found for C03.
FC13-C03-U040has one externalreference-port: repositorykbuzzard/ClassFieldTheory, commitccc3323c6750abca25b49b35106f54eb3a398509, pathClassFieldTheory/Mathlib/RingTheory/HenselPolynomial.lean, Apache-2.0. ItsMonicCoprimeFactors.liftAdicconstruction lifts coprime monic factorizations modulo an ideal in an adically complete ring and records the reductions. That source uses Lean 4.33.0-rc1 and Mathlib26245e682c354e86f2a4a300812fe4673ae107dc; because this is close but not the pinned project toolchain/revision, it is a reference to port, notpackage-import.- Strict bundle semantics were enforced. U004 is not credited from only forward transitivity; U012 is not credited from generic tensor exactness without the intersection+colon theorem; U019 is not credited from the finite local free theorem without the residue-independence/nilpotent clauses; U050/U055 are not credited from only completion Noetherianity; and U069 is not credited from lying-over/incomparability without Galois conjugacy.
- Purity was checked separately. P contains
Ideal.Pure, but that is the ideal special case defined through a flat quotient; no compatible general pure-submodule API was found. Hence U025–U030 remain unmatched rather than being laundered through ideal purity. - General linear topology was separated from adic completion. P has filter-basis/submodule-basis linear topologies, supporting U031, but no checked bridge identifies arbitrary presented linear-topology completion with the inverse limit
lim← M/M_λ; therefore U033–U037 remain unmatched while the I-adic specialization U038 and Noetherian finite-module completion theorems U042–U049 map natively. - Route totals for C03:
mathlib39,project-existing0,package-import0,reference-port1,unmatched33.
Definition: flat and faithfully flat module
An A-module M is flat if tensoring every exact sequence with M preserves exactness. It is faithfully flat if a sequence is exact exactly when its tensor with M is exact; it suffices to test short exact sequences, or injectivity at the left end.
Formalized. Mathlib/RingTheory/Flat/Basic.lean::Module.Flat, iff_rTensor_exact, iff_lTensor_exact; Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean::Module.FaithfullyFlat, rTensor_exact_iff_exact, lTensor_exact_iff_exact — Flatness is exactly preservation of tensor exactness; faithful flatness extends flatness and reflects exactness, with the pinned iff theorems giving Matsumura’s preservation/reflection formulation.
Definition: flat ring homomorphism / flat algebra
A ring map A→B is flat when B is flat as an A-module; B is then a flat A-algebra.
Formalized. Mathlib/RingTheory/Flat/Basic.lean::Module.Flat — A flat A-algebra B is represented exactly by the instance Module.Flat A B for the algebra-map module structure.
Example: localisations are flat
Every localisation A_S is a flat A-algebra.
Formalized. Mathlib/RingTheory/Flat/Localization.lean::IsLocalization.flat — IsLocalization.flat states that every localization is flat over its base ring.
Theorem: transitivity of flatness and faithful flatness
For an A-algebra B and B-module M: B A-flat and M B-flat imply M A-flat; faithful-flat analogues hold; if M is B-faithfully-flat and A-flat then B is A-flat; and if M is faithfully flat over both A and B then B is faithfully flat over A.
Not formalized. Pinned Mathlib has Module.Flat.trans and Module.FaithfullyFlat.trans, but no checked declaration supplies both reverse clauses in Matsumura’s four-part bundle for a B-module M (descent of B-flatness/faithful-flatness from M). Current/open/external search found no whole-bundle owner.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: change of coefficient ring for flatness
For an A-algebra B and A-module M, A-flatness of M implies B-flatness of M⊗_A B; faithful flatness is preserved likewise.
Formalized. Mathlib/RingTheory/Flat/Stability.lean::baseChange; Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean::Faithful flatness is preserved by arbitrary base change — Base change of a flat module is flat, and the faithfully-flat file has the corresponding arbitrary-base-change instance.
Theorem: Theorem 7.1
For A→B and a B-module M, M is flat over A iff M_P is flat over A_p for every prime P of B, where p=P∩A; it suffices to test maximal ideals P.
Formalized. Mathlib/RingTheory/Flat/Localization.lean::flat_iff_of_isLocalization, flat_of_isLocalized_maximal; Mathlib/RingTheory/Localization/AtPrime/Basic.lean::Localization.AtPrime — Localizing at P and its contraction p preserves/refines flatness via flat_iff_of_isLocalization; flat_of_isLocalized_maximal recovers global flatness from maximal localizations. Prime testing follows by the same AtPrime equivalence.
Theorem: Theorem 7.2
For an A-module M, faithful flatness is equivalent to: M is flat and N⊗_A M≠0 for every nonzero N; equivalently, M is flat and mM≠M for every maximal ideal m.
Formalized. Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean::iff_flat_and_proper_ideal, nontrivial_tensorProduct_iff_left, nontrivial_tensorProduct_iff_right — FaithfullyFlat is equivalent to flatness plus every proper ideal acting nontrivially, hence in particular the maximal-ideal test; the tensor nontriviality iff theorems are exactly the nonzero-module criterion.
Definition: fibre of Spec B→Spec A
For A→B and p∈Spec A, the fibre over p is Spec(B⊗_A κ(p)), canonically homeomorphic to {P∈Spec B | P∩A=p}.
Formalized. Mathlib/RingTheory/LocalRing/ResidueField/Fiber.lean::PrimeSpectrum.preimageHomeomorphFiber, Ideal.Fiber — preimageHomeomorphFiber identifies the fibre of Spec B → Spec A over p with Spec(κ(p) ⊗[A] B) as a homeomorphism, exactly the source definition/comparison.
Theorem: Theorem 7.3
For A→B and a B-module M: M is faithfully flat over A iff the image of Supp(M) in Spec A is all of Spec A. If M is finite over B and A-flat, it is faithfully flat iff that image contains m-Spec A.
Not formalized. Pinned Mathlib has faithful-flat spectrum surjectivity and Module.support_subset_preimage_comap, but no equality/source-shaped theorem identifying faithful flatness of an arbitrary B-module M over A with surjectivity of the image of Supp_B(M). The finite/maximal variant is likewise not exported.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Definition: local homomorphism
A homomorphism (A,m)→(B,n) of local rings is local if m maps into n. For a local homomorphism, flatness is equivalent to faithful flatness.
Formalized. Mathlib/Algebra/Group/Units/Hom.lean::IsLocalHom; Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean::Module.FaithfullyFlat.of_flat_of_isLocalHom — IsLocalHom is the maximal-ideal containment condition for local rings; a flat local map is faithfully flat, while faithful flatness already includes flatness.
Example: proper localisations are not faithfully flat
If A_S≠A, then Spec(A_S)→Spec A is not surjective; hence A_S is flat but not faithfully flat over A.
Not formalized. Localization flatness and faithful-flat spectrum criteria are available, but no checked declaration owns the explicit source theorem/example A_S ≠ A ⇒ A_S is not faithfully flat. Strict concrete-example semantics does not credit an easy derivation as an existing mapped unit.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 7.4
For flat M, tensoring preserves intersections of two submodules. Consequently for a flat map A→B, (I₁∩I₂)B=I₁B∩I₂B; if I₂ is finitely generated then (I₁:I₂)B=(I₁B:I₂B).
Not formalized. Flat tensor exactness supplies ingredients for intersection preservation, but no pinned/current/open/external declaration was found for the full two-submodule intersection equality together with the finitely-generated colon equality. The whole theorem remains unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Example: k[x²,x³]⊂k[x] is not flat
For A=k[x²,x³]⊂B=k[x], extension fails to preserve x²A∩x³A, so B is not flat over A.
Not formalized. No checked Lean declaration realizes k[x²,x³] ⊂ k[x] and the displayed failure of intersection preservation as a nonflatness witness.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 7.5
If A→B is faithfully flat, then M→M⊗_A B, m↦m⊗1, is injective for every A-module M; in particular A→B is injective, and IB∩A=I for every ideal I.
Formalized. Mathlib/RingTheory/Flat/FaithfullyFlat/Algebra.lean::Module.FaithfullyFlat.tensorProduct_mk_injective, Ideal.comap_map_eq_self_of_faithfullyFlat — The canonical M → B ⊗ M map is injective for every M; specializing to A gives injectivity of A→B, and the ideal theorem is exactly IB ∩ A = I.
Theorem: Theorem 7.6 (equational criterion)
If M is flat, every finite system Σ_j a_ij x_j=0 in M is obtained as an M-linear combination of solutions over A: x_j=Σ_k b_jk y_k with Σ_j a_ij b_jk=0. Conversely it suffices for this conclusion to hold for a single equation.
Formalized. Mathlib/RingTheory/Flat/EquationalCriterion.lean::tfae_equational_criterion — The equational-criterion development formalizes factorization of finite relations through relations over the base and proves the converse flatness criterion.
Theorem: Theorem 7.7 (ideal criterion for flatness)
M is flat iff for every finitely generated ideal I, the canonical map I⊗_A M→M is injective; then I⊗M≅IM.
Formalized. Mathlib/RingTheory/Flat/Tensor.lean::iff_lTensor_injective, iff_rTensor_injective — Pinned flatness is equivalent to injectivity of tensoring finitely generated ideals; the image of the multiplication map is the product submodule, yielding I⊗M ≃ IM.
Theorem: Theorem 7.8 (Tor criterion)
For an A-module M, the following are equivalent: M is flat; Tor_i^A(M,N)=0 for every A-module N and every i>0; Tor_1^A(M,A/I)=0 for every finitely generated ideal I.
Not formalized. Mathlib’s flatness category file still treats the relation with Tor as future linkage; searches found no theorem equating flatness with vanishing positive Tor or the Tor₁(A/I) criterion. No compatible external exact owner was found.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 7.9
In an exact sequence 0→M′→M→M″→0, if M′ and M″ are flat then M is flat.
Not formalized. Pinned tensor exactness proves the ingredients, but no checked declaration states Matsumura 7.9 as a reusable theorem that an extension of two flat modules is flat. Under strict source-shaped mapping this row is left unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 7.10
For a flat module M over a local ring (A,m), elements whose images in M/mM are linearly independent are linearly independent over A. If M is finite, or if m is nilpotent, every minimal basis of M is an A-basis, so M is free.
Not formalized. Module.free_of_flat_of_isLocalRing proves the finite flat local module is free, but no checked declaration supplies the preceding arbitrary-flat residue linear-independence lifting or the nonfinite nilpotent-maximal-ideal minimal-basis clause. Whole-bundle semantics leaves the theorem unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Corollary: finite flat modules over local rings are faithfully flat and free
For a nonzero finite module over a local ring, flatness, faithful flatness and freeness are equivalent.
Formalized. Mathlib/RingTheory/LocalRing/Module.lean::free_of_flat_of_isLocalRing; Mathlib/RingTheory/Flat/Basic.lean::of_free; Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean::iff_flat_and_proper_ideal — Finite flat modules over a local ring are free. A nonzero finite free module satisfies the maximal/proper-ideal faithful criterion, while faithfully flat implies flat, giving the three-way equivalence.
Theorem: Theorem 7.11
If B is a flat A-algebra, M is finitely presented, and N is any A-module, then Hom_A(M,N)⊗_A B ≅ Hom_B(M⊗_A B,N⊗_A B).
Formalized. Mathlib/Algebra/Module/FinitePresentation.lean::Module.FinitePresentation.isBaseChange_map, LinearMap.baseChangeHom — isBaseChange_map states that under flat base change the canonical Hom base-change map for finitely presented M is a base-change equivalence, exactly Theorem 7.11.
Corollary: Hom commutes with localisation for finitely presented source
For finitely presented M and p∈Spec A, Hom_A(M,N)⊗A A_p ≅ Hom{A_p}(M_p,N_p).
Formalized. Mathlib/Algebra/Module/FinitePresentation.lean::Module.FinitePresentation.linearEquivMapExtendScalars — This declaration is explicitly the linear equivalence between localized Hom_A(M,N) and Hom_{A_p}(M_p,N_p) for finitely presented M.
Theorem: Theorem 7.12
A finitely presented A-module M is projective iff M_m is free over A_m for every maximal ideal m.
Formalized. Mathlib/RingTheory/LocalProperties/Projective.lean::Module.projective_of_localization_maximal; Mathlib/Algebra/Module/Projective.lean::Module.Projective; Mathlib/RingTheory/LocalRing/Module.lean::free_of_flat_of_isLocalRing — A finitely presented module projective at all maximal localizations is globally projective; projective modules localize and finite projectives over local rings are free, giving the iff.
Corollary: finitely presented flat iff projective
A finitely presented A-module is flat iff it is projective.
Formalized. Mathlib/RingTheory/Flat/EquationalCriterion.lean::Flat.projective_of_finitePresentation; Mathlib/RingTheory/Flat/Basic.lean::Flat.of_projective — The forward theorem is explicit and projective modules are flat, exactly the source corollary.
Definition: pure submodule
N⊆M is pure if 0→N⊗E→M⊗E is exact for every A-module E; it suffices to test finitely presented E.
Not formalized. Pinned Mathlib has Ideal.Pure only for ideals via flat quotients, not a general pure-submodule predicate. Current/open/external searches found no compatible general pure-submodule API, so the source module-level statement cannot be credited from the ideal special case.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Example: flat quotients give pure submodules
If M/N is flat, then N is pure in M.
Not formalized. Pinned Mathlib has Ideal.Pure only for ideals via flat quotients, not a general pure-submodule predicate. Current/open/external searches found no compatible general pure-submodule API, so the source module-level statement cannot be credited from the ideal special case.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Example: direct summands are pure
Every direct summand of a module is a pure submodule.
Not formalized. Pinned Mathlib has Ideal.Pure only for ideals via flat quotients, not a general pure-submodule predicate. Current/open/external searches found no compatible general pure-submodule API, so the source module-level statement cannot be credited from the ideal special case.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Example: purity criterion for abelian groups
For A=Z, N⊆M is pure iff N∩mM=mN for every m>0.
Not formalized. Pinned Mathlib has Ideal.Pure only for ideals via flat quotients, not a general pure-submodule predicate. Current/open/external searches found no compatible general pure-submodule API, so the source module-level statement cannot be credited from the ideal special case.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 7.13
N⊆M is pure iff every finite system of linear equations over A with right-hand sides in N that has a solution in M already has a solution in N.
Not formalized. Pinned Mathlib has Ideal.Pure only for ideals via flat quotients, not a general pure-submodule predicate. Current/open/external searches found no compatible general pure-submodule API, so the source module-level statement cannot be credited from the ideal special case.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 7.14
If N is pure in M and M/N is finitely presented, then N is a direct summand of M.
Not formalized. Pinned Mathlib has Ideal.Pure only for ideals via flat quotients, not a general pure-submodule predicate. Current/open/external searches found no compatible general pure-submodule API, so the source module-level statement cannot be credited from the ideal special case.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Definition: linear topology
A directed descending family of submodules {M_λ} defines a linear topology on M by taking cosets x+M_λ as neighbourhoods; it is separated iff ⋂M_λ=0. For a ring, an ideal basis makes multiplication continuous.
Formalized. Mathlib/Topology/Algebra/FilterBasis.lean::RingFilterBasis, ModuleFilterBasis; Mathlib/Topology/Algebra/Nonarchimedean/Bases.lean::SubmodulesBasis, topology — Filter bases of submodules define the coset linear topology, ring filter bases make multiplication continuous, and the Hausdorff/T2 criteria identify separatedness with trivial intersection of the neighbourhood submodules.
Definition: separated quotient associated to a linear topology
M/⋂M_λ is the separated module associated with M.
Not formalized. Generic topological quotient and filter-basis infrastructure exists, but no checked declaration packages the source algebraic separated quotient M / ⋂ M_λ as the separated object attached to an arbitrary linear-topology presentation.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Definition: completion and complete module
The completion is M̂=lim← M/M_λ with its inverse-limit topology. The natural map M→M̂ has dense image; M̂ is complete, and M is complete when M→M̂ is an isomorphism.
Not formalized. Mathlib has abstract uniform completion and adic inverse-limit completion, but no theorem identifies the completion of an arbitrary submodule-basis linear topology with lim← M/M_λ together with density/completeness as this source unit states.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: equivalent linear topologies have the same completion
Two cofinal families of submodules define the same linear topology iff each eventually refines the other; then their inverse-limit completions are canonically isomorphic.
Not formalized. Cofinality/topology tools exist, but without the general inverse-limit linear-completion bridge of U033 there is no checked source-shaped theorem giving canonical isomorphism of the two presented completions.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Construction: closure and quotient topology
The closure of N⊆M is ⋂_λ(N+M_λ). The quotient topology on M/N is defined by the images of M_λ, is separated exactly when N is closed, and the subspace topology on N is defined by N∩M_λ.
Not formalized. Generic topology provides closure and quotient/subspace constructions, but no checked declaration packages all three source formulas relative to an arbitrary descending submodule basis, including closure N = ⋂(N+M_λ).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 8.1
For N⊆M with linear topologies induced from M, 0→N̂→M̂→(M/N)^ is exact and N̂ is the closure of the image of N in M̂. If the topology is defined by a decreasing sequence M₁⊇M₂⊇⋯, the sequence is also right-exact, so (M/N)^≅M̂/N̂.
Not formalized. Pinned adic completion has exactness for finite modules over Noetherian rings, but Matsumura 8.1 is an arbitrary linear-topology completion statement with an additional countable right-exactness clause. No exact compatible owner was found.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Construction: completion of continuous homomorphisms
A continuous linear map M→N induces a unique continuous map M̂→N̂ commuting with the natural maps; likewise continuous ring maps induce continuous maps of completions.
Not formalized. Abstract completion and adic completion have universal maps, but no checked declaration supplies the source map on the inverse-limit completion object from U033 for arbitrary linear topologies.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Definition: I-adic topology and completion
For I⊲A, the I-adic topology on M is defined by {I^nM}; the corresponding completions of A and M are the I-adic completions. I-adic completeness is equivalent to unique convergence of compatible/Cauchy sequences modulo I^n.
Formalized. Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean::adicModuleTopology, hasBasis_nhds_zero_adic; Mathlib/RingTheory/AdicCompletion/Basic.lean::AdicCompletion, IsAdicComplete, IsAdicCauchy, of_bijective_iff — The adic topology is generated by I^n M; AdicCompletion is the compatible quotient-family completion, IsAdicComplete is Hausdorff plus precomplete, and the Cauchy/of-bijective API gives the source sequence/completeness interpretation.
Theorem: Theorem 8.2
If A is I-adically complete then I⊆rad(A). If M is I-adically complete and a∈I, multiplication by 1+a is an automorphism of M.
Formalized. Mathlib/RingTheory/AdicCompletion/Basic.lean::IsAdicComplete.le_jacobson_bot; Mathlib/RingTheory/Jacobson/Ideal.lean::mem_jacobson_bot — Adic completeness gives I ≤ jacobson(0). The Jacobson criterion says a∈jacobson(0) iff all 1+a y are units; hence 1+a is a unit and scalar multiplication by it is an automorphism on any module.
Theorem: Theorem 8.3 (Hensel lemma)
For an m-adically complete local ring (A,m,k), if a monic F∈A[X] reduces to coprime monic factors F̄=gh in k[X], then F lifts to a factorization F=GH by monic G,H reducing to g,h.
Formalized. ClassFieldTheory/Mathlib/RingTheory/HenselPolynomial.lean::MonicCoprimeFactors.liftAdic at ccc3323c6750abca25b49b35106f54eb3a398509 — Apache-2.0 external Lean development. Under IsAdicComplete I R, liftAdic lifts a monic coprime factorization modulo I to monic factors upstairs and the map lemmas recover the prescribed reductions. The repository uses Lean 4.33.0-rc1 and Mathlib 26245e682c354e86f2a4a300812fe4673ae107dc; it is close to but not identical with project P, so this is a source reference to port rather than an import route.
Searched: kbuzzard/ClassFieldTheory@ccc3323c6750abca25b49b35106f54eb3a398509
Theorem: Theorem 8.4
If A is I-adically complete, M is I-adically separated, and M/IM is generated over A/I by the images of w₁,…,w_n, then w₁,…,w_n generate M over A.
Not formalized. Pinned adic completeness and Nakayama APIs do not export Matsumura’s non-finite complete/separated generation theorem from generators modulo I. Current/open/external search found no exact owner.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 8.5 (Artin–Rees)
For Noetherian A, finite M, N⊆M and I⊲A, there exists c>0 such that InM∩N=I{n-c}(I^cM∩N) for every n≥c.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.exists_pow_inf_eq_pow_smul — This is the Artin–Rees formula I^n M ∩ N = I^(n-k)(I^k M ∩ N) for all sufficiently large n under the source Noetherian/finite hypotheses.
Theorem: Theorem 8.6
Under Artin–Rees hypotheses, the I-adic topology on N equals the subspace topology induced by the I-adic topology on M.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.exists_pow_inf_eq_pow_smul, Stable.bounded_difference — Strong Artin–Rees gives two-sided cofinal bounds between the intrinsic I-adic filtration on N and the filtration I^nM∩N; therefore they define the same topology. The identical source-shaped assembly was compile-checked against P during FC04 C10 mapping.
Theorem: Theorem 8.7
For Noetherian A, I⊲A and finite M, the I-adic completion satisfies M̂≅M⊗_A Â. Hence if A is I-adically complete, so is every finite A-module M.
Formalized. Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean::AdicCompletion.ofTensorProductEquivOfFiniteNoetherian; Mathlib/RingTheory/AdicCompletion/Completeness.lean::AdicCompletion.isAdicComplete — For finite M over Noetherian A, the canonical  ⊗_A M → M̂ map is an equivalence; completeness of the completion then gives the source consequence for finite modules over complete A.
Theorem: Theorem 8.8
For Noetherian A, the I-adic completion  is flat over A.
Formalized. Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean::AdicCompletion.flat_of_isNoetherian — The pinned theorem states exactly that the I-adic completion of a Noetherian ring is flat over the original ring.
Theorem: Theorem 8.9 (Krull)
For Noetherian A, I⊲A and finite M, if N=⋂_{n>0}I^nM then there exists a∈A with a≡1 mod I and aN=0.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.mem_iInf_smul_pow_eq_bot_iff — Membership in ⋂ I^nM is equivalent to existence of r∈I with r x=x; taking a=1-r gives a≡1 mod I and annihilates the intersection submodule, exactly Matsumura 8.9.
Theorem: Theorem 8.10 (Krull intersection)
If A is Noetherian and I⊆rad(A), then the I-adic topology on every finite module is separated and every submodule is closed. If A is a Noetherian domain and I is proper, then ⋂_{n≥1}I^n=(0).
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, Ideal.iInf_pow_eq_bot_of_isDomain; Mathlib/RingTheory/AdicCompletion/Noetherian.lean::IsHausdorff.of_le_jacobson — The Jacobson-radical theorem gives separatedness for finite modules; Artin–Rees gives closed submodules, and the domain theorem gives zero intersection for powers of any proper ideal in a Noetherian domain.
Theorem: Theorem 8.11
For Noetherian A, ideals I,J and finite M, I-adic completion satisfies (JM)^=J M̂, equal to the closure of JM in M̂, and (M/JM)^≅M̂/JM̂.
Formalized. Mathlib/RingTheory/AdicCompletion/Exactness.lean::AdicCompletion.map_injective, map_exact, map_surjective; Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean::ofTensorProductEquivOfFiniteNoetherian — Completion is exact on finite modules over a Noetherian ring and is tensoring with Â. Applying exactness to JM ⊂ M → M/JM identifies the completed submodule with J M̂ and the completed quotient with M̂/JM̂; the same assembly was compile-checked against P in FC04 C10.
Example: power-series ring as adic completion
The (X₁,…,X_n)-adic completion of A[X₁,…,X_n] is AX₁,…,X_n.
Formalized. Mathlib/RingTheory/MvPowerSeries/Equiv.lean::MvPowerSeries.toAdicCompletionAlgEquiv — The canonical algebra equivalence identifies multivariable power series with the completion of the polynomial ring at the ideal generated by the variables, exactly the source example.
Theorem: Theorem 8.12
If A is Noetherian and I=(a₁,…,a_n), then Â≅AX₁,…,X_n/(X₁−a₁,…,X_n−a_n); in particular  is Noetherian.
Not formalized. Pinned Mathlib has the power-series completion equivalence but not the displayed quotient presentation by X_i-a_i, and Noetherianity of general Noetherian adic completions appears only in open PR #38331. Neither current master nor that PR closes the full source bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 8.13
For Noetherian A, I⊲A and finite M, the topology on M̂ is both its I-adic topology as an A-module and its IÂ-adic topology as an Â-module.
Not formalized. Pinned Mathlib algebraically identifies finite-module completion with tensor base change, but does not equip general AdicCompletion I M with the two module topologies and prove their equality as stated. The project’s extra adic-completion topology is ring-only.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 8.14
For Noetherian A with the I-adic topology, the following are equivalent: I⊆rad(A); every ideal is closed; Â is faithfully flat over A.
Not formalized. Pinned P has flat completion, Krull/Jacobson separatedness, and faithful-flat criteria, but no checked declaration proves the full equivalence I⊆rad(A) ↔︎ every ideal closed ↔︎ Â faithfully flat. Current/open/external search found no whole-bundle owner.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Definition: Zariski ring and ideal of definition
When the equivalent conditions of Theorem 8.14 hold, A is a Zariski ring and I an ideal of definition. Any ideal defining the same topology is also an ideal of definition; a Noetherian local ring with its m-adic topology is the basic example.
Not formalized. The project defines LeanCategories.Algebra.IsZariskiRing as Noetherian + adic + ideal inside the Jacobson radical, matching the core notion. It does not package the entire source row’s ideal-of-definition terminology, same-topology invariance, and local-ring example; strict whole-row semantics therefore does not classify the row as project-existing.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: Theorem 8.15
If A is semilocal with maximal ideals m₁,…,m_r and I=rad(A)=m₁⋯m_r, then the I-adic completion  decomposes as the product of the m_i-adic completions of the local rings A_{m_i}.
Not formalized. Finite-product and localization/completion APIs exist, but no pinned/current/open/external declaration was found for the semilocal Jacobson-radical completion decomposition into the product of the maximal-adic completions of the localizations.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Corollary: completion package for Noetherian local rings
For a Noetherian local (A,m): ⋂m^n=0; submodules of finite modules are m-adically closed;  is faithfully flat and IÂ∩A=I;  is Noetherian local with maximal ideal m and the same residue field, with Â/mnÂ≅A/mn; and quotients of complete local A by proper ideals are complete local rings.
Not formalized. Pinned P covers Krull intersection, closed submodules, local structure/maximal ideal, residue field, flatness and hence faithful flatness via the local map; however completion Noetherianity is only open PR #38331 and the proper-quotient complete-local package is not exported as one source theorem. The whole row remains unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Remark: completion need not localise to complete rings
Even when A is complete, a localisation A_p need not be complete.
Not formalized. No checked Lean example was found showing a localization of a complete ring that fails to be complete. Positive localization/completion APIs do not satisfy the source remark.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Example: Artinian local rings are complete
Every Artinian local ring is complete for its maximal-ideal-adic topology because some power of the maximal ideal is zero.
Formalized. Mathlib/RingTheory/AdicCompletion/Noetherian.lean::IsAdicComplete, isArtinianRing_iff_isNilpotent_maximalIdeal — Pinned Mathlib installs IsAdicComplete (maximalIdeal A) A for an Artinian local ring, using nilpotence of the maximal ideal, exactly the source example.
Definition: extension ring, integral element and integral extension
For A⊆B, B is an extension ring. An element b∈B is integral over A if it satisfies a monic polynomial over A; B/A is integral if every b∈B is integral.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean::RingHom.IsIntegralElem, RingHom.IsIntegral, Algebra.IsIntegral — Integral elements are exactly roots of monic polynomials over the source; an integral extension means every target element is integral.
Theorem: Theorem 9.1
b∈B is integral over A iff b lies in an intermediate A-subalgebra finite as an A-module. The set of elements of B integral over A is a subring.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean::isIntegral_iff_isIntegral_closure_finite, Algebra.finite_adjoin_simple_of_isIntegral; Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean::integralClosure, mem_integralClosure_iff — An element is integral iff it lies in an appropriate finite intermediate subalgebra; integralClosure is exactly the subalgebra of all integral elements, hence supplies closure under ring operations.
Definition: integral closure, integrally closed domain, normal ring
The integral elements of B over A form the integral closure Ā of A in B; A is integrally closed in B if A=Ā. A domain is integrally closed if integrally closed in its fraction field. Matsumura calls A normal if every A_p is an integrally closed domain.
Not formalized. Pinned Mathlib exactly defines integral closure, integrally closed-in, and integrally closed domains, and documents Matsumura’s normal-ring local condition, but it deliberately has no NormalRing/IsNormalRing declaration. The source row bundles that definition, so the full unit is unmatched.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Theorem: transitivity of integrality
If A⊆C⊆B, B is integral over C, and C is integral over A, then B is integral over A. Consequently the integral closure of A in B is integrally closed in B.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.trans; Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean::IsIntegrallyClosedIn — Integral extensions compose, and the integral closure is integrally closed in its ambient algebra, exactly the source consequence.
Example: UFDs are integrally closed
Every UFD is an integrally closed domain.
Formalized. Mathlib/RingTheory/Polynomial/RationalRoot.lean::instIsIntegrallyClosed — Mathlib installs IsIntegrallyClosed for unique-factorization domains, exactly the source example.
Example: normalisation of the cusp ring
For A=k[t²,t³]⊂k[t]=B⊂k(t), B is the integral closure of A in k(t); A≅k[X,Y]/(Y²−X³) is not integrally closed.
Not formalized. No checked declaration realizes k[t²,t³] ⊂ k[t] together with the cusp quotient presentation and proves that k[t] is its integral closure in k(t).
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Example: integral closure commutes with localisation
If Ā is the integral closure of A in B, then the integral closure of A_S in B_S is Ā_S. Hence localisations of integrally closed domains are integrally closed.
Formalized. Mathlib/RingTheory/Localization/Integral.lean::IsLocalization.integralClosure; Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean::isIntegrallyClosed_of_isLocalization — The integral closure after localization is itself the localization of the original integral closure; integrally closed domains remain integrally closed after localization.
Theorem: Theorem 9.2
Let A be integrally closed with fraction field K and L/K algebraic. α∈L is integral over A iff the minimal polynomial of α over K has all coefficients in A.
Formalized. Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean::minpoly.isIntegrallyClosed_eq_field_fractions, minpoly.isIntegrallyClosed_dvd — For an element algebraic over the fraction field, integrality over the integrally closed base is equivalent to its fraction-field minimal polynomial descending to the base; this is exactly the coefficient-membership criterion.
Example: quadratic integral closure in a UFD
If A is a UFD with 2 invertible and s∈A is square-free, then A[√s] is integrally closed.
Not formalized. Generic UFD, squarefree, integral-closure and quadratic-extension APIs are present, but no checked declaration proves the source theorem that A[√s] is integrally closed under the stated UFD/2-invertible/squarefree hypotheses.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Lemma: integral domain extension field criterion
If B is a domain integral over a subring A, then A is a field iff B is a field.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.isField_iff_isField — For an injective integral extension of domains, the target is a field iff the source is a field, exactly the source lemma for an inclusion.
Lemma: maximal ideals under integral extensions
For integral A⊆B, contraction of a maximal ideal of B is maximal; every maximal ideal of A has a prime of B lying over it, and every such prime is maximal.
Formalized. Mathlib/RingTheory/Ideal/GoingUp.lean::isMaximal_comap_of_isIntegral_of_isMaximal, isMaximal_of_isIntegral_of_isMaximal_comap, exists_ideal_over_prime_of_isIntegral — Maximality is preserved/reflected between a prime upstairs and its contraction in an integral extension, and lying-over supplies a prime over every maximal ideal downstairs.
Theorem: Theorem 9.3
For integral A⊆B and p∈Spec A: a prime of B lies over p; distinct primes over p are incomparable. If A is integrally closed with fraction field K, L/K is normal, and B is the integral closure of A in L, then all primes of B over p are conjugate under Aut(L/K).
Not formalized. Pinned Mathlib has lying-over and incomparability (IsIntegral.comap_lt_comap), but no checked general theorem that all primes of the integral closure over p are conjugate under Aut(L/K) for a normal field extension. Specialized number-theory developments do not cover the general bundle.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07
Definition: going-up and going-down properties
Going-up means p⊂p′ and P over p can be lifted to P⊂P′ over p′. Going-down is the dual lifting statement starting from P′ over p′.
Formalized. Mathlib/RingTheory/Ideal/HasGoingUp.lean::Algebra.HasGoingUp; Mathlib/RingTheory/Ideal/GoingDown.lean::Algebra.HasGoingDown — These classes encode exactly the source lifting conditions for comparable primes.
Theorem: Theorem 9.4
Integral extensions satisfy going-up. If B is a domain integral over an integrally closed domain A, then going-down also holds.
Formalized. Mathlib/RingTheory/Ideal/HasGoingUp.lean::Algebra.HasGoingUp.of_isIntegral; Mathlib/RingTheory/IntegralClosure/GoingDown.lean::Algebra.HasGoingDown — Integral extensions satisfy going up; a domain integral over an integrally closed domain receives the going-down instance, matching the source hypotheses.
Theorem: Theorem 9.5
Every flat A-algebra B satisfies going-down over A.
Formalized. Mathlib/RingTheory/Ideal/GoingDown.lean::Algebra.HasGoingDown.of_flat — The pinned instance states exactly that every flat algebra satisfies going down.
Theorem: Theorem 9.6
If A⊆B are domains, A is integrally closed and B integral over A, then Spec B→Spec A is open. More precisely, for t∈B with minimal-degree monic relation tn+a₁t{n−1}+⋯+a_n=0, the image of D(t) is ⋃_i D(a_i).
Not formalized. Pinned/current Mathlib has openness results under finite-presentation/Chevalley hypotheses, but no theorem for an arbitrary integral domain extension over an integrally closed domain with the explicit image D(t)=⋃D(a_i) formula. Open/external search found no exact owner.
Searched: P=db584cd6d46c92f209a44c0f1c829460d327499d; H=e281a66114fe17935e6ea7917a01b714d0c1e493; open/external search 2026-09-07