Chapter 10. Completions (pp. 100–112)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 15 definitions, 3 theorems, 11 propositions, 4 lemmas, 9 corollaries, 3 examples, 1 counterexample, 5 constructions, 1 notation and 8 other statements.
Of the 60 statements checked against Lean, 39 are formalized somewhere and 21 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 34 | 57% | Mathlib states and proves it. |
| not formalized | 21 | 35% | A documented search found no Lean statement of it anywhere. |
| in another Lean project | 4 | 7% | Some other Lean development has it; using it means porting that code. |
| in lean-categories | 1 | 2% | This repository states and proves it. |
| checked in total | 60 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first at repo HEAD351cba0287077eadfcd7c71a78ec4a509ce8c966.LeanCategories/ForMathlib/AdicCompletionTopology.leanis the sole general whole-row project owner in this chapter: it supplies the topology and topological-ring structure on ring adic completion used forFC04-C10-U018. The file was compiled at this HEAD. Project code has no topology on general module adic completions, no associated-graded construction, and no general Rees grading structure. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, contains the topological-group completion APIs, adic completion/functoriality/exactness/tensor/flatness/local/Krull infrastructure, filtrations/Artin-Rees/Rees algebra, and general graded-ring/module infrastructure cited in the chapter. Source-shaped assemblies for U035, U037, U041, U046, and U047 were compile-checked against P; the first-half declaration-name probe and the project U018 bridge also compiled in the P environment. - Current Mathlib: upstream
5aedf732b6987e8c26ab3c9ebc855314f82b045f(Apache-2.0), denotedH, was rechecked on 2026-09-06 and retains the pinned positive owners. H still has no topology onAdicCompletion I M, no stable-filtration topology theorem, no graded-Noetherian biconditional of U029, no exported grading on the Rees ring/module objects of U030, and no pinned associated-graded/noetherian-completion owners for U053/U054/U059. - Open Mathlib work was rechecked immediately before assembly. PR #33218 remains open at head
3c12745297b7236616f6a23d7c11a8addd85e839(Apache-2.0) and supplies the associated graded ring inMathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean; U053 is thereforereference-port, notmathlib. PR #33220 remains open at head70572cd62395e933e8f6476bcedcee366a5b5e82and supplies the associated graded module; U054 isreference-port. PR #38331 remains open at head700711ddc105006709aa5e9bb98684001a93859aand supplies Noetherianity of general adic completion; U059 isreference-port. Negative evidence for U056 also rechecked PR heads #33225=77d1835b8c0fcd797e8ba34f3513d3bcd4e6ce20and #33227=41854bad257ddac64fd172e8d3d571b633ee0c0e: their filtered/associated-graded map results still do not imply injectivity/surjectivity after completion. - External exact route U012:
LiranShaul/lean-faithfully-flat-descent@f5967aab9067290aed1b7113569c1b9024a9fca4(Apache-2.0),lib/mlSystem.lean::InverseSystem.surjective_limit_of_mittagLeffler_exactplussurjective_is_mittag_leffler. The repository currently pins Leanv4.26.0-rc2and Mathlibd5c9558e75342a10d6321e6a8c798a14f68ae23c; the source file compiled unchanged against this project’s newer P, so U012 is a revision-specificreference-portwith verified compatibility. - External/current inverse-limit search also rechecked
ImperialCollegeLondon/FLT@8ec873aab84b21c4faaef849d5afd56ef79f684d,DE0CH/flt-lean@a5ec7082457bab42553702cdb183b3e034021ab3, andacmepjz/lean-iwasawa@7fffeb8c80fbe13f989f318c23cbb0dcf2230092. They contain inverse-limit infrastructure but no stronger whole-row owner replacing the U012 route or filling U013–U015. - The bundled p-adic example U021 was searched through P/H and indexed external Lean code. Current heads of the most relevant surfaced repositories were rechecked:
rwst/lean-code@ce1619b6418dc263efb911b11ad09409c2083d80,YijunYuan/FormalizedSparse@be9fb43dded873bc7567b486e17e924823e10e41, andCBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434. None supplied the complete source bundle identifyingℤ_pwith the adic completion together with a canonical base-pdigit expansion and convergence statement. - Graded/Rees negatives U023/U029/U030 were searched in P/H, open Mathlib work, and indexed external Lean code.
tom111/BEI-lean@5b3ddff1ffac4a12d16da43df6fc443501f4d680surfaced for graded Noetherian developments but assumes both Noetherianity and finite type rather than proving U029. No externalreesAlgebragrading owner or stable-filtration topology theorem was found. Ndenotes dated 2026-09-06 strict negative evidence after project-first search, P/H, open/current Mathlib, installed packages, and targeted external Lean search. A partial theorem, informal docstring identification, editorially related fact, or one clause of a bundled proposition does not satisfy a canonical unit under strict bundle semantics. This is why U023, U029, U030, U044, and U055 remain unmatched despite substantial nearby formalization.
Definition / comparison: Topological abelian group and zero-neighborhood control
A topological abelian group has continuous addition and inversion. If {0} is closed then the group is Hausdorff; translations are homeomorphisms, so the topology is determined by the neighborhoods of 0.
Formalized. Mathlib/Topology/Algebra/Group/Basic.lean::IsTopologicalAddGroup; Homeomorph.addLeft; map_add_left_nhds_zero; Mathlib/Topology/Algebra/Group/Pointwise.lean::IsTopologicalAddGroup.t2Space_iff_zero_closed — Addition/inversion continuity is the bundled topological-add-group structure. Translation is a homeomorphism, zero-neighborhoods determine all neighborhoods, and in a topological additive group closed {0} is equivalent to Hausdorffness.
Lemma: Lemma 10.1
If H is the intersection of all neighborhoods of 0 in a topological abelian group G, then H is a subgroup, H=closure({0}), G/H is Hausdorff, and G is Hausdorff iff H=0.
Formalized. Mathlib/Topology/Separation/Basic.lean::R0Space.closure_singleton; Mathlib/Topology/Algebra/FilterBasis.lean::AddGroupFilterBasis.t2Space_iff; Mathlib/Topology/Algebra/Group/Quotient.lean::QuotientAddGroup.instT3Space — In a topological additive group the neighborhood-kernel at zero is the closure of {0} and is an additive subgroup. Quotienting by that closed subgroup is Hausdorff; the filter-basis criterion identifies Hausdorffness with trivial intersection.
Definition / construction: Cauchy sequences and completion of a topological abelian group
Assuming 0 has a countable fundamental system of neighborhoods, a sequence is Cauchy if its pairwise differences eventually lie in every zero-neighborhood. Equivalent Cauchy sequences differ by a sequence tending to 0; their classes form the completion Ĝ, with canonical homomorphism φ:G→Ĝ given by constant sequences.
Formalized. Mathlib/Topology/UniformSpace/Completion.lean::UniformSpace.Completion; Completion.denseRange_coe; Mathlib/Topology/Algebra/GroupCompletion.lean::UniformSpace.Completion.toCompl; Mathlib/Topology/UniformSpace/Cauchy.lean::CauchySeq — Mathlib constructs the same Hausdorff completion by Cauchy filters modulo inseparability, without the source’s countable-basis restriction. CauchySeq supplies the sequence formulation when desired, and toCompl is the canonical additive homomorphism.
Comparison: Kernel and injectivity of the completion map
For the canonical map φ:G→Ĝ, ker φ is the intersection of all neighborhoods of 0; hence φ is injective exactly when G is Hausdorff.
Formalized. UniformSpace.Completion.isUniformInducing_coe; SeparationQuotient.mk_eq_mk; R0Space.closure_singleton; UniformSpace.Completion.coe_injective; IsTopologicalAddGroup.t2Space_iff_zero_closed — Equality in the separated completion is exactly source inseparability pulled back along the uniform inducing map. For a topological additive group the inseparability class of zero is closure {0}, i.e. the intersection of its neighborhoods; therefore the completion map is injective exactly in the Hausdorff case.
Construction / convention: Functoriality of completion
A continuous homomorphism f:G→H sends Cauchy sequences to Cauchy sequences and induces a continuous homomorphism f̂:Ĝ→Ĥ; completion respects composition: (g∘f)^=ĝ∘f̂.
Formalized. Mathlib/Topology/Algebra/GroupCompletion.lean::AddMonoidHom.completion; AddMonoidHom.continuous_completion; Mathlib/Topology/UniformSpace/Completion.lean::UniformSpace.Completion.map_comp — A continuous additive homomorphism is uniformly continuous for the canonical group uniformities, extends to completions, and the underlying completion maps satisfy the source composition law.
Construction / example: Topologies defined by descending subgroups
A descending sequence G=G₀⊇G₁⊇⋯ defines a topology by declaring U a zero-neighborhood iff U contains some Gₙ. Each Gₙ is open and closed. The standard example is the p-adic topology on Z with Gₙ=pⁿZ.
Formalized. Mathlib/Topology/Algebra/FilterBasis.lean::AddGroupFilterBasis; AddGroupFilterBasis.hasBasis; open-subgroup/closed-subgroup API; Mathlib/Topology/Algebra/Nonarchimedean/AdicTopology.lean::Ideal.hasBasis_nhds_zero_adic — A descending family of additive subgroups is a zero-neighborhood basis and generates the source topology; basis subgroups are open and hence closed. The principal-ideal adic basis specializes this to the standard p-adic topology on ℤ.
Construction / comparison: Completion as coherent residue classes
For a subgroup topology, a Cauchy sequence determines compatible classes ξₙ∈G/Gₙ, and every coherent family arises this way. Thus Ĝ can equivalently be defined as the group of coherent sequences of residue classes.
Not formalized. partial: UniformSpace.Completion; quotient groups; categorical limits — P/H have both abstract completion and quotient/inverse-limit infrastructure, but no checked bridge identifies completion for an arbitrary descending subgroup topology with coherent residue classes G/G_n, including surjectivity from every coherent family. Targeted current/open/external search found no whole-row owner.
Searched: N
Definition / construction: Inverse system and inverse limit
A sequence of groups Aₙ with transition maps θₙ₊₁:Aₙ₊₁→Aₙ is an inverse system. Its inverse limit lim←Aₙ is the group of coherent sequences (aₙ) with θₙ₊₁(aₙ₊₁)=aₙ. In particular Ĝ≅lim←G/Gₙ.
Not formalized. partial: Mathlib/Order/DirectedInverseSystem.lean::InverseSystem; CategoryTheory.Limits.limit; U007 infrastructure — Inverse systems and categorical inverse limits are formalized, but the row also asserts the specific canonical isomorphism Ĝ ≃ lim G/G_n; that missing bridge prevents strict whole-bundle credit.
Searched: N
Comparison / convention: Topology versus a chosen inverse system
Different descending subgroup sequences can define the same topology and hence the same completion; the topological formulation packages this choice-independence, whereas a single inverse-system presentation depends on the chosen subgroups.
Not formalized. partial: topological completion; inverse-system APIs — P/H have topology and limit interfaces separately, but no checked theorem proves that cofinal/different descending subgroup presentations defining the same topology yield the source completion comparison.
Searched: N
Definition: Surjective inverse system
An inverse system is called surjective when every transition homomorphism θₙ₊₁ is surjective.
Formalized. Mathlib/Order/DirectedInverseSystem.lean::InverseSystem; Function.Surjective — Mathlib’s transition-law structure together with pointwise Function.Surjective is exactly the source notion that every transition homomorphism is surjective.
Definition / construction: Exact sequence of inverse systems
Compatible short exact sequences 0→Aₙ→Bₙ→Cₙ→0 arranged in commuting transition diagrams form an exact sequence of inverse systems and induce maps between their inverse limits.
Formalized. Mathlib/Algebra/Homology/ShortComplex/FunctorEquivalence.lean::ShortComplex.functorEquivalence; functor-category abelian/exactness API; CategoryTheory.Limits.lim.map — A compatible family of short exact sequences is equivalently a functor into short complexes, with exactness checked pointwise. A natural transformation induces the source maps on inverse limits through lim.map.
Proposition: Proposition 10.2
For an exact sequence 0→{Aₙ}→{Bₙ}→{Cₙ}→0 of inverse systems, 0→lim←Aₙ→lim←Bₙ→lim←Cₙ is always exact. If {Aₙ} is surjective, the map lim←Bₙ→lim←Cₙ is also surjective, giving a short exact sequence.
Formalized. LiranShaul/lean-faithfully-flat-descent@f5967aab9067290aed1b7113569c1b9024a9fca4::lib/mlSystem.lean::InverseSystem.surjective_limit_of_mittagLeffler_exact; surjective_is_mittag_leffler — The external theorem proves right exactness on inverse limits under the Mittag-Leffler condition; its surjective-transition lemma specializes exactly to Proposition 10.2. Apache-2.0; source Lean v4.26.0-rc2, Mathlib d5c9558e75342a10d6321e6a8c798a14f68ae23c. The file compiled unchanged against P.
Searched: E
Notation / OCR-sensitive comparison: Derived obstruction Coker d^A
For d^A:∏Aₙ→∏Aₙ used in the proof of 10.2, the source records Coker d^A as a derived-functor inverse-limit object. The frozen extraction garbles both the superscript in d^A and the displayed limit notation; this unit preserves the mathematical role without silently trusting the OCR rendering.
Not formalized. partial: inverse-limit and Mittag-Leffler infrastructure — No checked project/P/H/open/external declaration identifies the source difference map d^A and its cokernel with a lim¹/derived inverse-limit object. The source row is also OCR-sensitive, so partial inverse-limit APIs are not credited.
Searched: N
Corollary: Corollary 10.3
For a short exact sequence 0→G′→G→G″→0, give G the topology from {Gₙ}, G′ the induced topology from {G′∩Gₙ}, and G″ that from {p(Gₙ)}. Then 0→Ĝ′→Ĝ→Ĝ″→0 is exact.
Not formalized. partial: short exact sequences; completion; U012 external theorem — The abstract ingredients exist, but no checked owner assembles the induced subgroup/quotient topologies, identifies their completions with the corresponding residue inverse limits, and proves the displayed completed short exact sequence.
Searched: N
Corollary: Corollary 10.4
For each n, the completion of Gₙ is a subgroup Ĝₙ⊆Ĝ and Ĝ/Ĝₙ≅G/Gₙ.
Not formalized. partial: completion; quotient groups — No checked P/H/open/external theorem identifies the completion of each basis subgroup G_n with a subgroup of Ĝ and proves Ĝ/Ĝ_n ≃ G/G_n as a whole bundle.
Searched: N
Proposition: Proposition 10.5
The completion of a completion is canonically isomorphic to the completion: ≅G. Equivalently, Ĝ is complete. The frozen extraction at L3735 loses one hat and renders this tautologically as “Ĝ≅Ĝ”.
Formalized. Mathlib/Topology/UniformSpace/Completion.lean::UniformCompletion.completeEquivSelf; UniformSpace.Completion.instCompleteSpace — Completion is complete and separated; applying completeEquivSelf to an already complete separated completion gives the canonical idempotence Completion (Completion G) ≃ Completion G.
Definition: Complete topological group
G is complete when its canonical map φ:G→Ĝ is an isomorphism. Under this definition completeness includes Hausdorffness.
Formalized. CompleteSpace; T0Space; UniformCompletion.completeEquivSelf; UniformSpace.Completion.coe_injective — The source’s “canonical completion map is an isomorphism” is Mathlib’s CompleteSpace together with separation (T0Space, equivalent to Hausdorff for topological groups). Under those hypotheses completeEquivSelf is the canonical uniform equivalence, so source completeness includes Hausdorffness exactly as stated.
Definition / construction: a-adic topology and completion of a ring
For an ideal a⊆A, the subgroups aⁿ define the a-adic topology. A is then a topological ring (its ring operations are continuous); it is Hausdorff iff ⋂aⁿ=(0). Its completion  is a topological ring and A→ is a continuous ring homomorphism with kernel ⋂aⁿ.
Formalized. LeanCategories/ForMathlib/AdicCompletionTopology.lean::AdicCompletion.quotientPowTopology; adicCompletionTopologicalSpace; AdicCompletion.instIsTopologicalRing; AdicCompletion.continuous_eval; P Ideal.hasBasis_nhds_zero_adic; AdicCompletion.of; AdicCompletion.of_injective_iff — P supplies the ideal-power adic topology and algebraic coherent-residue completion. The project adds the inverse-limit topology on the completion, topological-ring structure, and continuity of projections; together with the pinned Hausdorff/injectivity criteria this realizes the full ring row. The project file compiled at current repo HEAD.
Searched: repo HEAD + P
Definition / construction: a-adic topology and completion of a module
For an A-module M, the submodules aⁿM define the a-topology. The completion M̂ is a topological Â-module (the scalar action Â×M̂→M̂ is continuous). Every A-linear map f:M→N is continuous for these topologies and induces f̂:M̂→N̂.
Not formalized. partial: P Ideal.adicModuleTopology; AdicCompletion I M; AdicCompletion.map; algebraic Module (AdicCompletion I R) (AdicCompletion I M) — P has the source algebraic module completion and functorial linear maps, but neither P nor H gives a topology on AdicCompletion I M or continuity of the completed scalar action. The project topology bridge is ring-only, so the whole source bundle is not represented.
Searched: N
Example: kx as an adic completion
For A=k[x] and a=(x), the a-adic completion is kx.
Formalized. Mathlib/RingTheory/MvPowerSeries/Equiv.lean::MvPowerSeries.toAdicCompletionAlgEquiv — Specializing the finite-variable theorem to one variable identifies the (x)-adic completion of k[x] with kx, exactly the source example.
Example: p-adic integers as an adic completion
For A=Z and a=(p), Â is the ring of p-adic integers, represented by ∑aₙpⁿ with 0≤aₙ≤p−1; pⁿ→0.
Not formalized. partial: PadicInt; PadicInt.toZModPow; PadicInt.ker_toZModPow; PadicInt.adicCompletionIntegersEquiv; adic convergence APIs — P/H formalize ℤ_p, its compatible residues, completeness, and adic-completion comparisons, but no checked declaration gives the source digit expansion ∑ a_n p^n with 0≤a_n≤p-1 as part of the same bundle. Current external searches (including rwst/lean-code@ce1619b6418dc263efb911b11ad09409c2083d80, YijunYuan/FormalizedSparse@be9fb43dded873bc7567b486e17e924823e10e41, and CBirkbeck/AINTLIB@160e446617a2168c34c95bbe7a76c4105b392434) found no complete owner.
Searched: N
Definition: Filtration, a-filtration, and stable a-filtration
A filtration of M is a descending chain M=M₀⊇M₁⊇⋯. It is an a-filtration if aMₙ⊆Mₙ₊₁ for all n, and stable if aMₙ=Mₙ₊₁ for all sufficiently large n. The filtration (aⁿM) is stable.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.Filtration; Ideal.Filtration.Stable; Ideal.stableFiltration; Ideal.stableFiltration_stable — Ideal.Filtration is a descending module filtration satisfying I • F_n ≤ F_{n+1}; Stable is eventual equality, and the power filtration is proved stable.
Lemma: Lemma 10.6
Any two stable a-filtrations of M have bounded difference; consequently all stable a-filtrations induce the same topology, namely the a-topology.
Not formalized. partial: Mathlib/RingTheory/Filtration.lean::Ideal.Filtration.Stable.bounded_difference — P proves the exact bounded-difference lemma, but Filtration.lean exports no topology generated by an arbitrary filtration and no theorem that bounded difference implies equality of those topologies. H and targeted external Lean search found no whole-row owner.
Searched: N
Definition: Graded ring
A graded ring is a ring A with additive subgroups Aₙ (n≥0) such that A=⊕ₙAₙ and A_mA_n⊆A_{m+n}. Thus A₀ is a subring and each Aₙ an A₀-module.
Formalized. Mathlib/RingTheory/GradedAlgebra/Basic.lean::GradedRing; DirectSum.Decomposition; GradedRing.proj — The internal graded-ring class records multiplication of grades and a direct-sum decomposition; grade zero inherits ring structure and each grade the expected module structure.
Example: Polynomial grading
For A=k[x₁,…,x_r], take Aₙ to be the homogeneous polynomials of degree n.
Formalized. Mathlib/RingTheory/MvPolynomial/Homogeneous.lean::MvPolynomial.homogeneousSubmodule; MvPolynomial.gradedAlgebra; homogeneousComponent — The homogeneous degree-n polynomial submodules form the standard grading of a polynomial algebra, specializing to the source finite polynomial ring.
Definition / convention: Graded module, homogeneous elements, and components
A graded A-module M has M=⊕ₙMₙ with A_mM_n⊆M_{m+n}. Elements lying in some Mₙ are homogeneous of degree n, and every element has a unique finite decomposition into homogeneous components.
Formalized. Mathlib/Algebra/Module/GradedModule.lean::SetLike.GradedSMul; DirectSum.Decomposition; DirectSum.decompose; DirectSum.sum_support_decompose; homogeneous-element API — Mathlib’s internal graded-module interface is a direct-sum decomposition compatible with graded scalar multiplication. decompose has finite support and reconstructs each element uniquely as the sum of homogeneous components.
Definition: Homomorphism of graded modules
A homomorphism f:M→N of graded A-modules is A-linear and satisfies f(Mₙ)⊆Nₙ for every n.
Formalized. Mathlib/RingTheory/GradedAlgebra/RingHom.lean::GradedRingHom; graded linear-map/map_mem API — The graded-map structures require the underlying linear/additive map to send each degree component into the same prescribed degree, exactly the source condition.
Definition / construction: Positive-degree ideal A₊
For a graded ring A, A₊=⊕_{n>0}Aₙ is an ideal of A.
Formalized. Mathlib/RingTheory/GradedAlgebra/Homogeneous/Ideal.lean::HomogeneousIdeal.irrelevant; mem_irrelevant_iff; irrelevant_eq_iSup — The irrelevant ideal is precisely the ideal generated by all nonzero/positive homogeneous degrees; over ℕ this is the source A_+ = ⊕_{n>0} A_n.
Proposition: Proposition 10.7
For a graded ring A, A is Noetherian iff A₀ is Noetherian and A is finitely generated as an A₀-algebra.
Not formalized. partial: Mathlib/RingTheory/GradedAlgebra/Noetherian.lean::GradedRing.GradeZero.isNoetherianRing; generic Algebra.FiniteType.isNoetherianRing; GradedAlgebra.exists_finset_adjoin_eq_top_and_homogeneous — P/H prove A Noetherian implies A_0 Noetherian and prove the forward Hilbert-basis direction from finite type over a Noetherian base, but no checked theorem derives finite generation of an arbitrary ℕ-graded Noetherian ring over A_0. tom111/BEI-lean@5b3ddff1ffac4a12d16da43df6fc443501f4d680 only assumes both hypotheses.
Searched: N
Construction: The graded rings/modules A and M attached to a filtration
For a ring A and ideal a, A*=⊕_{n≥0}aⁿ is a graded ring. If (Mₙ) is an a-filtration, M=⊕ₙMₙ is a graded A-module.
Not formalized. partial: Mathlib/RingTheory/ReesAlgebra.lean::reesAlgebra; Mathlib/RingTheory/Filtration.lean::Ideal.Filtration.submodule; coefficient membership theorems — P/H realize A* and M* as coefficient-restricted polynomial algebra/module objects, and the Rees-algebra docstring identifies the direct-sum mathematics, but no exported GradedRing structure on reesAlgebra or graded-module structure on Filtration.submodule was found. Strict bundle semantics therefore do not credit the informal identification.
Searched: N
Comparison: Noetherianity of A
If A is Noetherian and a=(x₁,…,x_r), then A*=A[x₁,…,x_r] and is Noetherian.
Formalized. Mathlib/RingTheory/ReesAlgebra.lean::reesAlgebra; adjoin_monomial_eq_reesAlgebra; reesAlgebra.fg; Noetherian instance — For a finitely generated ideal the Rees algebra is generated in degree one; over a Noetherian ring the ideal is finitely generated and the Rees algebra is Noetherian, exactly the source comparison.
Lemma: Lemma 10.8
Let A be Noetherian, M finitely generated, and (Mₙ) an a-filtration. Then M* is finitely generated as an A*-module iff the filtration (Mₙ) is stable.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.Filtration.submodule_fg_iff_stable — For finitely generated filtration pieces, finite generation of the filtration’s Rees submodule is equivalent to stability, exactly Lemma 10.8.
Proposition: Proposition 10.9 (Artin–Rees lemma)
Let A be Noetherian, a an ideal, M finitely generated, (Mₙ) a stable a-filtration, and M′⊆M. Then (M′∩Mₙ) is a stable a-filtration of M′. The extraction drops the symbol a before “an ideal in A”.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.Filtration.Stable.inter_right; Stable.of_le — Intersecting a stable filtration with a submodule in a finite module over a Noetherian ring remains stable, exactly Proposition 10.9.
Corollary: Corollary 10.10
For M′⊆M as above, there is k such that (aⁿM)∩M′ = a{n−k}((akM)∩M′) for all n≥k.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.exists_pow_inf_eq_pow_smul — This is the Artin-Rees formula (I^n M) ∩ M' = I^(n-k)((I^k M) ∩ M') after the theorem’s index normalization.
Theorem: Theorem 10.11
For A Noetherian, a an ideal, M finitely generated, and M′⊆M, the filtrations aⁿM′ and (aⁿM)∩M′ have bounded difference. Hence the intrinsic a-topology on M′ equals the topology induced from M.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.Filtration.Stable.bounded_difference; Stable.inter_right; stable power filtration — Applying bounded difference to the intrinsic power filtration on M' and the induced intersection filtration gives exactly the source bounded-difference assertion. The source-shaped assembly was compile-checked against P; equality of the induced adic topologies follows from the same two-sided cofinal bounds.
Named comparison: Strong versus topological Artin–Rees
The source distinguishes the bounded-difference assertion of 10.11 from its topological consequence: Chapter 10 uses the latter, while Chapter 11 needs the stronger bounded-difference form.
Not formalized. partial: U035 strong Artin-Rees theorem — The mathematical strong theorem is formalized, but the source row is specifically the named distinction and later-use comparison between the strong assertion and its topological consequence; no formal declaration owns that editorial comparison as a source-shaped unit.
Searched: N
Proposition: Proposition 10.12
If 0→M′→M→M″→0 is exact with all three modules finitely generated over a Noetherian ring A, then for any ideal a the induced sequence of a-adic completions 0→M̂′→M̂→M̂″→0 is exact.
Formalized. Mathlib/RingTheory/AdicCompletion/Exactness.lean::AdicCompletion.map_injective; map_exact; map_surjective — These three theorems assemble the completed short exact sequence for finite modules over a Noetherian ring. The complete source-shaped sequence was compile-checked against P.
Construction: Natural map Â⊗A M→M̂
The canonical A→ makes  an A-algebra, and M→M̂ induces a natural Â-linear comparison map Â⊗_A M→M̂.
Formalized. Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean::AdicCompletion.ofTensorProduct; ofTensorProduct_tmul; ofTensorProduct_naturality — ofTensorProduct is exactly the canonical  ⊗_A M → M̂ comparison and is natural in M.
Comparison: The natural tensor/completion map can fail both injectivity and surjectivity
For arbitrary A and M, the natural map Â⊗_A M→M̂ need be neither injective nor surjective; Proposition 10.13 records the finite-generation hypotheses that recover surjectivity or an isomorphism.
Not formalized. partial: AdicCompletion.ofTensorProduct; finite-generation recovery theorems — P/H/open/external search found no explicit examples witnessing both possible failures—noninjectivity and nonsurjectivity—of the arbitrary tensor/completion comparison map. Positive finite-generation theorems do not satisfy this row.
Searched: N
Proposition: Proposition 10.13
For any ring A and finitely generated M, the natural map Â⊗_A M→M̂ is surjective. If A is Noetherian, it is an isomorphism.
Formalized. AdicCompletion.ofTensorProduct_surjective_of_finite; ofTensorProduct_bijective_of_finite_of_isNoetherian; ofTensorProductEquivOfFiniteNoetherian — The natural map is surjective for finite modules over any ring and bijective/equivalent for finite modules over a Noetherian ring, exactly Proposition 10.13.
Comparison: Exactness of tensor-completion on finite modules
For A Noetherian, 10.12 and 10.13 identify completion on finitely generated modules with the exact functor M↦Â⊗_A M.
Formalized. U037/U040 owners; Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean::LinearMap.lTensor_exact — The finite-module completion equivalences identify the exact completion sequence with tensoring by Â; the tensor exactness assembly was compile-checked against P.
Proposition: Proposition 10.14
If A is Noetherian and  is its a-adic completion, then  is a flat A-algebra.
Formalized. Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean::AdicCompletion.flat_of_isNoetherian — The adic completion of a Noetherian ring is flat over the original ring, exactly Proposition 10.14.
Named comparison: Completion versus tensor-completion for non-finite modules
For non-finitely-generated modules M↦M̂ need not be exact; M↦Â⊗_A M is exact and agrees with completion on finitely generated modules.
Not formalized. partial: U040/U042 positive finite-module agreement and flat tensor exactness — P/H/open/external search found no source-shaped non-finitely-generated module for which adic completion fails exactness, so the negative comparison row is not formalized as stated.
Searched: N
Proposition: Proposition 10.15
For A Noetherian with a-adic completion Â: (i) â=Âa≅Â⊗_A a; (ii) (aⁿ)^=(â)ⁿ; (iii) aⁿ/aⁿ⁺¹≅âⁿ/âⁿ⁺¹; (iv) â is contained in the Jacobson radical of Â.
Not formalized. partial: adic completion tensor equivalence; mapped-ideal/power APIs; IsAdicComplete.le_jacobson_bot — P supplies clauses corresponding to extension of the ideal, powers, and the Jacobson-radical inclusion, but no exported general isomorphism a^n/a^(n+1) ≃ â^n/â^(n+1) was found. Under strict bundle semantics the missing clause (iii) makes the proposition unmatched.
Searched: N
Proposition: Proposition 10.16
If (A,m) is a Noetherian local ring, then its m-adic completion  is local with maximal ideal m̂.
Formalized. Mathlib/RingTheory/AdicCompletion/LocalRing.lean::AdicCompletion.isLocalRing_of_fg; Noetherian local instance; AdicCompletion.maximalIdeal_eq_map — For a Noetherian local ring the maximal ideal is finitely generated, the maximal-adic completion is local, and its maximal ideal is the mapped/completed original maximal ideal.
Theorem: Theorem 10.17 (Krull’s Theorem)
For A Noetherian, a an ideal, and M finitely generated, the kernel E=⋂_{n≥1}aⁿM of M→M̂ consists exactly of those x∈M annihilated by some element of 1+a.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.mem_iInf_smul_pow_eq_bot_iff; Mathlib/RingTheory/AdicCompletion/Basic.lean::AdicCompletion.of_apply — The filtration theorem characterizes membership in ⋂ I^n M by existence of a scalar congruent to one modulo I fixing the element; rewriting gives annihilation by an element of 1+I. Together with the completion map’s kernel this is exactly 10.17. The assembly was compile-checked.
Named comparison: Localization inside completion for S=1+a
With S=1+a, A→Â and A→S⁻¹A have the same kernel. Every element of S becomes a unit in Â, giving a natural injective homomorphism S⁻¹A→Â.
Formalized. IsLocalization.map_eq_zero_iff; IsLocalization.lift; IsLocalization.lift_injective_iff; Mathlib/RingTheory/AdicCompletion/Basic.lean::IsAdicComplete.le_jacobson_bot; U046 — Elements of 1+I become units in the complete ring, the localization therefore maps to the completion, and the localization kernel criterion plus U046 gives equality of kernels and injectivity. The source-shaped bundle was compile-checked against P.
Counterexample: Failure of Krull’s theorem without Noetherianity
For A=C^∞(R) and a the maximal ideal of functions vanishing at 0, ⋂aⁿ consists of functions flat at 0, whereas annihilation by 1+a corresponds to vanishing on a neighborhood. The function e^{-1/x²} separates the two kernels, so A is not Noetherian.
Not formalized. partial: Mathlib smooth glue/flat-function calculus such as expNegInvGlue.contDiff — No checked Lean development supplies the ring C^∞(ℝ), the maximal ideal at zero, the identification of all ideal powers with vanishing jets, and the e^{-1/x²} kernel separation required by the source counterexample.
Searched: N
Corollary: Corollary 10.18
If A is a Noetherian domain and a≠(1), then ⋂_{n≥1}aⁿ=0.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.iInf_pow_eq_bot_of_isDomain — For a Noetherian domain and proper ideal, the intersection of all powers is zero, exactly Corollary 10.18.
Corollary: Corollary 10.19
If A is Noetherian, a is contained in the Jacobson radical, and M is finitely generated, then ⋂aⁿM=0; equivalently, the a-topology on M is Hausdorff.
Formalized. Mathlib/RingTheory/Filtration.lean::Ideal.iInf_pow_smul_eq_bot_of_le_jacobson; Mathlib/RingTheory/AdicCompletion/Noetherian.lean::IsHausdorff.of_le_jacobson — If the ideal lies in the Jacobson radical, the intersection of its powers acting on a finite module is zero; IsHausdorff.of_le_jacobson packages the equivalent Hausdorff adic-completion condition.
Corollary: Corollary 10.20
For a Noetherian local ring (A,m) and finitely generated M, the m-adic topology on M is Hausdorff; in particular, so is the m-adic topology on A.
Formalized. Mathlib/RingTheory/AdicCompletion/Noetherian.lean::IsHausdorff.of_isLocalRing; maximal-ideal IsHausdorff instance — Specializing U050 to a Noetherian local ring and its maximal ideal gives Hausdorffness for every finite module, and hence for the ring itself.
Corollary: Corollary 10.21
For A Noetherian and p prime, the intersection of all p-primary ideals of A is the kernel of A→A_p.
Not formalized. partial: primary-ideal APIs; localization kernels; Krull intersection — P/H/open/external search found no theorem identifying the intersection of all p-primary ideals with the kernel of A → A_p. The surrounding localization and primary-decomposition ingredients do not constitute the source corollary.
Searched: N
Definition / construction: Associated graded ring Ga(A)
For a ring A and ideal a, G_a(A)=⊕_{n≥0} aⁿ/aⁿ⁺¹, with multiplication induced by representatives: x̄_m x̄_n=overline{x_mx_n}.
Formalized. Mathlib PR #33218 head 3c12745297b7236616f6a23d7c11a8addd85e839, Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean::GradedPiece; AssociatedGraded; graded multiplication/ring instance — Open Apache-2.0 Mathlib PR. The generic associated-graded construction specializes, after the standard descending-to-ascending reindexing, to G_a(A)=⊕ a^n/a^(n+1) with representative multiplication. Because it is absent at P, this remains a revision-specific reference port.
Searched: PR33218
Definition / construction: Associated graded module G(M)
For an A-module M with a-filtration (Mₙ), define G(M)=⊕_{n≥0}Mₙ/Mₙ₊₁, naturally a graded G_a(A)-module; write Gₙ(M)=Mₙ/Mₙ₊₁.
Formalized. Mathlib PR #33220 head 70572cd62395e933e8f6476bcedcee366a5b5e82, Mathlib/RingTheory/FilteredAlgebra/AssociatedGraded.lean; associated-graded module scalar structure and Module (AssociatedGraded ...) — Open Apache-2.0 Mathlib PR. It supplies the quotient graded pieces and natural module structure over the associated graded ring, matching the source G(M) construction after reindexing.
Searched: PR33220
Proposition: Proposition 10.22
For A Noetherian and ideal a: (i) G_a(A) is Noetherian; (ii) G_a(A)≅G_â(Â) as graded rings; (iii) if M is finitely generated and (Mₙ) is a stable a-filtration, then G(M) is finitely generated over G_a(A).
Not formalized. partial: PR #38331 graded-ring Noetherianity support; PR #33218/#33220 associated-graded structures — Current/open work can cover associated-graded Noetherianity, but no checked source supplies the completion graded-ring isomorphism G_a(A) ≃ G_â(Â) together with the finite-generation statement for stable filtered modules. The three-clause source bundle therefore remains unmatched.
Searched: N
Lemma: Lemma 10.23
For a homomorphism φ:A→B of filtered groups (meaning φ(Aₙ)⊆Bₙ), if the induced G(φ):G(A)→G(B) is injective then φ̂ is injective; if G(φ) is surjective then φ̂ is surjective.
Not formalized. partial: Mathlib PR #33225/#33227 filtered and associated-graded hom exactness — The open filtered/associated-graded map work does not prove the source implication “graded map injective/surjective ⇒ completed map injective/surjective.” No complete project/current/external owner was found.
Searched: N
Proposition: Proposition 10.24
Let A be complete in the a-topology, M an A-module with an a-filtration, and suppose M is Hausdorff for the filtration topology. If G(M) is finitely generated over G(A), then M is finitely generated over A.
Not formalized. partial: completion; associated-graded PRs — No checked declaration proves that completeness plus Hausdorffness and finite generation of the associated graded module lift to finite generation of the original filtered module.
Searched: N
Corollary: Corollary 10.25
Under the hypotheses of 10.24, if G(M) is Noetherian as a G(A)-module, then M is Noetherian as an A-module.
Not formalized. partial: U057 ingredients; Noetherian module APIs — No checked declaration lifts Noetherianity of G(M) over G(A) to Noetherianity of the complete Hausdorff filtered module M under the source hypotheses.
Searched: N
Theorem: Theorem 10.26
If A is Noetherian and a is an ideal, then the a-adic completion  is Noetherian.
Formalized. Mathlib PR #38331 head 700711ddc105006709aa5e9bb98684001a93859a, Mathlib/RingTheory/AdicCompletion/Noetherian.lean::AdicCompletion.isNoetherianRing_of_fg; general IsNoetherianRing (AdicCompletion I R) instance — Open Apache-2.0 Mathlib PR. It proves exactly that the adic completion of a Noetherian ring is Noetherian; the result is absent at P/H and therefore is recorded only at this PR revision.
Searched: PR38331
Corollary: Corollary 10.27
If A is Noetherian, then Ax₁,…,xₙ is Noetherian; in particular kx₁,…,xₙ is Noetherian for a field k.
Formalized. Mathlib/RingTheory/MvPowerSeries/Equiv.lean finite-variable IsNoetherianRing (MvPowerSeries σ R) instance; power-series Noetherian infrastructure — For finite σ, formal power series over a Noetherian coefficient ring are Noetherian; specializing to Fin n gives Ax_1,…,x_n, and fields are Noetherian.