Chapter 3. Rings and Modules of Fractions (pp. 36–42)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 4 definitions, 10 propositions, 6 corollaries, 6 constructions, 1 convention, 1 notation and 5 other statements.
Of the 33 statements checked against Lean, 27 are formalized somewhere and 6 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 26 | 79% | Mathlib states and proves it. |
| not formalized | 6 | 18% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 1 | 3% | This repository states and proves it. |
| checked in total | 33 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first for localization, ideal extension/contraction, localized modules, flatness, and local-global interfaces. U026 is project-owned; the other source-shaped interfaces are delegated to Mathlib. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, was checked declaration-wise. - Current/open Mathlib: upstream
29ea5de9cb981cb62dfa7979aaff0851f50c603a(Apache-2.0, Lean v4.34.0-rc2), denotedH, was rechecked 2026-09-06 for the strict negative rows. - External search: targeted indexed/GitHub searches were performed for the concrete
1+𝔞, integer-localization and geometric examples and for finite annihilator/colon localization. No complete external Lean owner was found; because these are new negative judgments rather than inherited external rows, there is no stale external revision being carried forward. Ndenotes dated 2026-09-06 negative evidence after project-first search, P/H, open/current work, installed packages, and targeted external search. Generic localization infrastructure is not credited for an explicit source example or a missing finite-generation theorem.
Definition: Multiplicatively closed subset
S⊂A with 1∈S and closed under multiplication.
Formalized. Submonoid R — A submonoid contains 1 and is closed under multiplication, exactly the source multiplicatively closed subset.
Construction: Ring of fractions S⁻¹A
On A×S set (a,s)~(b,t) iff (at−bs)u=0 for some u∈S; equivalence classes a/s receive the usual fraction addition and multiplication.
Formalized. Mathlib/RingTheory/Localization/Defs.lean::Localization; Localization.mk — The quotient relation on numerator/denominator pairs is the source cross-multiplication relation up to the standard witness orientation, and the quotient carries the usual ring operations.
Construction: Canonical localization map A→S⁻¹A
f(x)=x/1; it need not be injective.
Formalized. algebraMap R (Localization S); Localization.mk_one; IsLocalization.subsingleton — The canonical map is x ↦ x/1. If 0 ∈ S, every localization is subsingleton, so for any nontrivial base ring the map cannot be injective; this realizes the source warning that injectivity need not hold.
Reusable comparison: Field of fractions as a localization
If A is a domain and S=A−{0}, then S⁻¹A is the field of fractions of A.
Formalized. Mathlib/RingTheory/Localization/FractionRing.lean::FractionRing; IsFractionRing; IsLocalization at nonZeroDivisors — For a domain, localization at the nonzero elements is its fraction field.
Definition: Ring of fractions
S⁻¹A is called the ring of fractions of A with respect to S.
Formalized. Localization S; IsLocalization S — Mathlib uses the same ring-of-fractions object, parameterized by the localization submonoid.
Proposition 3.1: Universal property of localization
If g:A→B sends every s∈S to a unit, there is a unique h:S⁻¹A→B with g=h∘f, necessarily h(a/s)=g(a)g(s)⁻¹.
Formalized. Mathlib/RingTheory/Localization/Basic.lean::IsLocalization.lift; lift_mk'; ringHom_ext — A map sending denominators to units extends uniquely, and lift_mk' gives the formula g(a) g(s)⁻¹.
Characterization: Three structural properties of S⁻¹A
The canonical map sends S to units; kernel elements are annihilated by some s∈S; every localized element is f(a)f(s)⁻¹. These characterize S⁻¹A up to isomorphism.
Formalized. Mathlib/RingTheory/Localization/Defs.lean::IsLocalization; map_units; map_eq_zero_iff; surj — The typeclass records exactly the three source properties: denominators become units, kernel elements are annihilated by a denominator, and every element is a fraction.
Corollary 3.2: Recognition criterion for a localization
A map g:A→B satisfying the three localization properties identifies B uniquely with S⁻¹A.
Formalized. Mathlib/RingTheory/Localization/Basic.lean::IsLocalization.algEquiv; Localization.algEquiv; isLocalization_of_algEquiv — Any algebra satisfying the localization structure is uniquely isomorphic over the base ring to the canonical localization.
Construction / definition: Localization A𝔭 at a prime
For prime 𝔭 take S=A−𝔭 and write A_𝔭=S⁻¹A; its fractions with numerator in 𝔭 form the unique maximal ideal, so A_𝔭 is local. Passing A→A_𝔭 is localization at 𝔭.
Formalized. Mathlib/RingTheory/Localization/AtPrime/Basic.lean::Localization.AtPrime; IsLocalization.AtPrime.under_maximalIdeal; AtPrime.map_eq_maximalIdeal; local-ring instance — Localization at the prime complement is local, with unique maximal ideal the extension of the prime.
Notation / construction: Principal localization Af
For S={f^n}_{n≥0}, write A_f=S⁻¹A.
Formalized. Mathlib/RingTheory/Localization/Away/Basic.lean::Localization.Away; Submonoid.powers — Localization.Away f is localization at the powers of f, exactly A_f.
Reusable example: Localization at 1+𝔞
For any ideal 𝔞, S=1+𝔞 is multiplicatively closed.
Not formalized. partial: generic Submonoid constructors and ideal arithmetic — Neither P nor H has a declaration packaging 1 + 𝔞 as a multiplicatively closed submonoid; targeted current/open/external Lean search found no exact owner. Generic closure infrastructure is not credited for this explicit reusable example.
Searched: N
Reusable example: Localizations of Z
Z_(p) consists of rationals with denominator prime to p; Z_f consists of rationals whose denominator is a power of f.
Not formalized. partial: Rat.isFractionRing; Localization.AtPrime; Localization.Away — P/H formalize the generic localizations of ℤ, but no checked declaration identifies ℤ_(p) with rationals whose denominator is prime to p and ℤ_f with denominators a power of f as the source bundle states.
Searched: N
Reusable geometric example: Polynomial localization along a variety
For A=k[t₁,…,tₙ] and prime 𝔭, A_𝔭 consists of rational functions f/g with g∉𝔭; for infinite k it is interpreted as functions defined at almost all points of V(𝔭).
Not formalized. partial: Localization.AtPrime; RatFunc; polynomial/zero-locus APIs — P/H realize the algebraic localization at a prime but not the source geometric interpretation as rational functions defined at almost all points of V(𝔭) over an infinite field; targeted external Lean search found no complete owner.
Searched: N
Construction: Module of fractions S⁻¹M
On M×S set (m,s)~(m′,s′) iff t(sm′−s′m)=0 for some t∈S; classes form an S⁻¹A-module. Write M_𝔭 and M_f in the corresponding cases.
Formalized. Mathlib/Algebra/Module/LocalizedModule/Basic.lean::LocalizedModule; IsLocalizedModule; LocalizedModule.mk — The quotient/fraction module and its localization-ring action realize the source S⁻¹M, including prime and principal specializations.
Construction: Localization of a module homomorphism
u:M→N induces S⁻¹u:m/s↦u(m)/s, compatible with composition.
Formalized. Mathlib/RingTheory/Localization/Module.lean::LocalizedModule.map; map_mk; map_id; map_comp — A linear map localizes by m/s ↦ u(m)/s and is functorial.
Proposition 3.3: Exactness of localization
If M′→M→M″ is exact at M, its localization is exact at S⁻¹M.
Formalized. Mathlib/Algebra/Module/LocalizedModule/Exact.lean::LocalizedModule.map_exact; IsLocalizedModule.map_exact — Localization preserves exactness at the middle module exactly as Proposition 3.3.
Convention: Localized submodule convention
For M′⊂M, exactness makes S⁻¹M′→S⁻¹M injective, so S⁻¹M′ is henceforth regarded as a submodule.
Formalized. U016 plus Submodule.toLocalized; LocalizedModule.map_injective_iff interfaces — Localization of a submodule inclusion remains injective, and the localized submodule API realizes it as a submodule of the localized ambient module.
Corollary 3.4: Localization commutes with finite sums, intersections, quotients
S⁻¹(N+P)=S⁻¹N+S⁻¹P, S⁻¹(N∩P)=S⁻¹N∩S⁻¹P, and S⁻¹(M/N)≅S⁻¹M/S⁻¹N.
Formalized. Submodule.localized'_iSup; localized'_inf; localizedQuotientEquiv — Localization preserves sums and intersections and the quotient localization is canonically linearly equivalent to the quotient by the localized submodule.
Proposition 3.5: Localization as tensor product
There is a unique S⁻¹A-linear isomorphism S⁻¹A⊗_A M→S⁻¹M sending (a/s)⊗m to am/s.
Formalized. Mathlib/RingTheory/Localization/BaseChange.lean::LocalizedModule.equivTensorProduct; pure-tensor lemmas — This is the canonical S⁻¹A ⊗_A M ≃ S⁻¹M equivalence with the source fraction formula.
Corollary 3.6: Localization ring is flat
S⁻¹A is flat as an A-module.
Formalized. Mathlib/RingTheory/Flat/Localization.lean::IsLocalization.flat — Every localization ring is flat over the base ring.
Proposition 3.7: Localization commutes with tensor product
S⁻¹M⊗_{S⁻¹A}S⁻¹N≅S⁻¹(M⊗_A N), with (m/s)⊗(n/t)↦(m⊗n)/(st).
Formalized. IsLocalization.tensorProduct_isLocalizedModule; IsLocalization.moduleTensorEquiv; IsLocalizedModule.linearEquiv — The tensor product of localized modules is itself the localization of the original tensor product, and the canonical equivalences give the stated S⁻¹M ⊗_{S⁻¹A} S⁻¹N ≃ S⁻¹(M⊗_A N) formula.
Definition: Local property
A property P of A or an A-module M is local if it holds globally iff it holds after localization at every prime ideal.
Not formalized. partial: Mathlib/RingTheory/LocalProperties/Basic.lean::RingHom.PropertyIsLocal — Mathlib’s PropertyIsLocal is a stronger ring-hom gluing/localization framework, not the source generic predicate on a ring or module defined simply by P(X) ↔︎ ∀ 𝔭, P(X_𝔭). No source-shaped generic definition was found in P/H or indexed external Lean.
Searched: N
Proposition 3.8: Vanishing is local
M=0 iff M_𝔭=0 for every prime 𝔭 iff M_𝔪=0 for every maximal 𝔪.
Formalized. Mathlib/RingTheory/LocalProperties/Submodule.lean::Module.eq_zero_of_localization_maximal; Module.subsingleton_of_localization_maximal; support/localization APIs — The maximal-local converse is explicit; forward localization of zero is trivial. Since maximal ideals are prime, this yields both prime and maximal formulations.
Proposition 3.9: Injectivity and surjectivity are local
φ:M→N is injective iff all φ_𝔭 are injective iff all φ_𝔪 are injective; likewise for surjectivity.
Formalized. Mathlib/RingTheory/LocalProperties/Exactness.lean::injective_of_localized_maximal; surjective_of_localized_maximal; localization preserves injectivity/surjectivity in the forward direction — Injectivity and surjectivity are detected at maximal localizations, hence equivalently at all primes; forward localization is supplied by the exact/localized-map APIs.
Proposition 3.10: Flatness is local
M is flat over A iff each M_𝔭 is flat over A_𝔭 iff each M_𝔪 is flat over A_𝔪.
Formalized. Mathlib/RingTheory/Flat/Localization.lean::Module.flat_of_localized_maximal; Module.flat_iff_of_isLocalization; localized-flat stability — Flatness localizes and is recovered from all maximal localizations; primes give the equivalent stronger family.
Construction: Extension in a localization
For A→S⁻¹A, the extension of an ideal 𝔞 is S⁻¹𝔞; C and E denote the contracted ideals of A and extended ideals of S⁻¹A.
Formalized. LeanCategories/Algebra/Ideals.lean::LeanCategories.Algebra.extendedIdeal; contractedIdeal — The project explicitly names extension and contraction for ideals under Localization S, exactly the source construction and C/E convention.
Searched: repo HEAD
Proposition 3.11: Extended/contracted ideals and primes under localization
Every ideal of S⁻¹A is extended; 𝔞^{ec}=⋃_{s∈S}(𝔞:s); contracted ideals are those on which no s∈S is a zero-divisor modulo 𝔞; primes correspond exactly to primes disjoint from S; localization commutes with finite sums/products/intersections/radicals.
Formalized. Mathlib/RingTheory/Localization/Ideal.lean::IsLocalization.map_under; algebraMap_mem_map_algebraMap_iff; orderIsoOfPrime; map_inf; map_radical; generic Ideal.map_sup/map_mul — Every localized ideal is extended from its contraction; extension–contraction has the saturation membership criterion; primes correspond to primes disjoint from S; sums, products, finite intersections, and radicals commute with localization.
Corollary 3.12: Nilradical localizes
The nilradical of S⁻¹A is S⁻¹𝔑.
Formalized. Mathlib/RingTheory/Localization/Ideal.lean::IsLocalization.map_radical — Applying map_radical to the zero ideal gives localization of the nilradical.
Corollary 3.13: Prime ideals of A𝔭
Prime ideals of A_𝔭 correspond to prime ideals of A contained in 𝔭.
Formalized. Mathlib/RingTheory/Localization/AtPrime/Basic.lean::IsLocalization.AtPrime.orderIsoOfPrime; primeSpectrumOrderIso — Prime ideals of A_𝔭 are order-isomorphic to prime ideals of A contained in 𝔭.
Definition / comparison: Residue field at a prime
For prime 𝔭, localizing at 𝔭 and quotienting by 𝔭 yields the residue field at 𝔭; it is both Frac(A/𝔭) and the residue field of A_𝔭. Localization retains primes below 𝔭, quotient retains primes above 𝔭.
Formalized. IsLocalization.AtPrime.equivQuotMaximalIdeal; Mathlib/RingTheory/LocalRing/ResidueField/Ideal.lean IsFractionRing (R ⧸ I) I.ResidueField; prime-order/quotient correspondences — The local residue field agrees with the fraction field of A/𝔭; AtPrime and quotient prime correspondences encode primes below and above 𝔭 respectively.
Proposition 3.14: Annihilator of a finite module localizes
For finitely generated M, S⁻¹Ann(M)=Ann(S⁻¹M).
Not formalized. partial: localized submodule/kernel APIs; Module.annihilator; finite-generation APIs — No theorem in P or H identifies S⁻¹ Ann(M) with Ann(S⁻¹M) for finite M; targeted current/open/external Lean search also found no complete owner. The result is not credited from generic localization infrastructure alone.
Searched: N
Corollary 3.15: Colon ideals localize when denominator module is finite
For N,P⊂M with P finitely generated, S⁻¹(N:P)=(S⁻¹N:S⁻¹P).
Not formalized. partial: Submodule.annihilator_map_mkQ_eq_colon; localized quotient/submodule APIs — P/H have colon-as-annihilator and localization machinery but no theorem proving (S⁻¹N : S⁻¹P)=S⁻¹(N:P) under finite generation of P; targeted current/open/external Lean search was negative.
Searched: N
Proposition 3.16: Criterion for a prime to be a contraction
For A→B and prime 𝔭⊂A, 𝔭 is the contraction of a prime of B iff 𝔭^{ec}=𝔭.
Formalized. Mathlib/RingTheory/Ideal/Maps.lean::Ideal.comap_map_eq_self_iff_of_isPrime — For a prime 𝔭, extension followed by contraction fixes 𝔭 iff 𝔭 is the contraction of a prime upstairs, exactly Proposition 3.16.