Chapter 5. Integral Dependence and Valuations (pp. 59–66)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 9 definitions, 4 theorems, 9 propositions, 3 lemmas, 8 corollaries, 1 example, 1 construction and 4 other statements.
Of the 39 statements checked against Lean, 32 are formalized somewhere and 7 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 28 | 72% | Mathlib states and proves it. |
| not formalized | 7 | 18% | A documented search found no Lean statement of it anywhere. |
| in lean-categories | 2 | 5% | This repository states and proves it. |
| in a Lean package | 2 | 5% | A library available as a Lake dependency has it. |
| checked in total | 39 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first. Project HEAD351cba0287077eadfcd7c71a78ec4a509ce8c966owns the integrally-closed-domain and valuation-ring category wrappers used at U020 and U029; the remaining source-shaped results are delegated to Mathlib. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, contains everymathlibroute below. Critical declaration names were compile-checked against the project pin. - Current/open Mathlib: upstream
5aedf732b6987e8c26ab3c9ebc855314f82b045f(Apache-2.0), denotedH, was refreshed 2026-09-06. The only change from the immediately preceding checked29ea5de9cb981cb62dfa7979aaff0851f50c603aisscripts/nolints.json, so none of the C05 Lean-source positives or negatives changed; targeted open-PR searches did not resolve the strict gaps. - Package-import route:
Eisanthropics/fermats-last-theorem@aa2d8b34692b16c70f699536de0d8e75b9a3e9ef(Apache-2.0), pathP2M/Sol/S_ValuationSubring_exists_ringHom_extend_of_isAlgClosed.lean. Its lakefile pins MathlibPand toolchain v4.33.1; the module was independently built against this repository’s Lean v4.33.0 and pinP. U031–U032 use its exportedChevalleyHompartial-homomorphism graph/Zorn/local-ring API. - External negative search: U003 was checked against current/open Mathlib, broad indexed/GitHub Lean search, and ATLAS
e8b31c5cb0bec89b487ce33fe525a2c0b0f8b9c6(Apache-2.0) without an exact faithful-module criterion. U023–U025 have no checked external owner. For U033–U034,Ereaches the valuation-ring endpoint for its chosen maximal graph internally but does not export the source theorems for an arbitrary supplied maximal pair; TauCeti89947b89f080ff3ad6f83f6842fe23b6d07e2b9fand CBirkbeck2f45865e87d20dd460cc5a14d04850bf03be4570likewise use Mathlib’s alternative maximal-local-subring construction. No checked external owner was found for U036. Ndenotes dated 2026-09-06 negative evidence after project-first search, P/H, open/current work, installed packages, and targeted external Lean search. Alternative proofs are not credited for source-specific construction rows, and partial theorem bundles are not promoted.
Definition: Element integral over a subring
For A⊂B, x∈B is integral over A if it satisfies a monic polynomial xn+a₁x{n−1}+⋯+a_n=0 with a_i∈A.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean::RingHom.IsIntegralElem; IsIntegral — Integrality is existence of a monic polynomial over the base whose evaluation at the element is zero, exactly the source definition.
Example 5.0: Rational numbers integral over Z
A rational r/s in lowest terms integral over Z must have s=±1; hence the elements of Q integral over Z are exactly Z.
Formalized. Mathlib/NumberTheory/Niven.lean::IsIntegral.exists_int_iff_exists_rat; Rat.den_eq_one_iff; Rat.den_div_intCast_eq_one_iff — Specializing the concrete rational/integer theorem to x=q:ℚ gives integral rational ⇒ integer; integer casts are integral. The denominator lemmas recover the source reduced-fraction conclusion that the denominator is a unit, hence ±1.
Proposition 5.1: Equivalent criteria for integrality
x is integral over A iff A[x] is finite as an A-module; equivalently it lies in a finite A-subring and there exists a faithful A[x]-module finite over A. The extraction omits displayed clause (iii), but lines 2316–2318 identify it as the intermediate finite A-subring criterion.
Not formalized. partial: Algebra.finite_adjoin_simple_of_isIntegral; Algebra.IsIntegral.of_finite; IsIntegral.of_mem_of_fg; LinearMap.exists_monic_and_aeval_eq_zero — P/H realize the finite-adjoin and finite-intermediate-subalgebra criteria, but no checked theorem gives the source converse from existence of a faithful A[x]-module finite over arbitrary commutative A. The closest isIntegral_of_smul_mem_submodule assumes a domain ambient algebra and torsion-free module.
Searched: N
Corollary 5.2: Finite generation by finitely many integral elements
If x₁,…,xₙ are integral over A then A[x₁,…,xₙ] is finitely generated as an A-module.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean::Algebra.finite_adjoin_of_finite_of_isIntegral — A finite set of integral generators has module-finite adjoin, exactly the finite-generator corollary.
Corollary 5.3: Integral elements form a subring
The elements of B integral over A form a subring C containing A.
Formalized. Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean::integralClosure; mem_integralClosure_iff — integralClosure A B is the subalgebra whose carrier is exactly the elements integral over A; its structure supplies closure under ring operations and contains the base image.
Definition: Integral closure of A in B
The subring C of all elements of B integral over A.
Formalized. Mathlib/RingTheory/IntegralClosure/Algebra/Basic.lean::integralClosure; mem_integralClosure_iff — Exactly the subring/subalgebra of ambient elements integral over the base.
Definition: A integrally closed in B
A is integrally closed in B when its integral closure in B equals A.
Formalized. Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean::IsIntegrallyClosedIn.integralClosure_eq_bot_iff; isIntegrallyClosedIn_iff — For an injective inclusion, being integrally closed in the ambient ring is equivalent to the integral closure being the embedded base ring (⊥ as a subalgebra).
Definition: B integral over A
B is integral over A when every element of B is integral over A, equivalently the integral closure equals B.
Formalized. Algebra.IsIntegral; Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::integralClosure_eq_top_iff — Every target element is integral over the source iff the integral closure is top, exactly “B integral over A”.
Definition: Integral ring homomorphism / integral A-algebra
For f:A→B, f is integral and B an integral A-algebra when B is integral over f(A).
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean::RingHom.IsIntegral; Mathlib/RingTheory/IntegralClosure/Algebra/Defs.lean::algebraMap_isIntegral_iff — A ring hom is integral exactly when every target element is integral with respect to it; the algebra formulation is its algebra-map specialization.
Comparison: Finite type + integral = finite
An A-algebra that is both of finite type and integral is finite as an A-module.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.finite; Algebra.finite_iff_isIntegral_and_finiteType — Finite type plus integral is equivalent to module-finite, in particular giving the source implication.
Corollary 5.4: Transitivity of integral dependence
If A⊂B⊂C, B is integral over A, and C integral over B, then C is integral over A.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.trans; RingHom.IsIntegral.trans — Integral extensions compose exactly as in Corollary 5.4.
Corollary 5.5: Integral closure is integrally closed in the ambient ring
If C is the integral closure of A in B, then C is integrally closed in B.
Formalized. Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean instance IsIntegrallyClosedIn (integralClosure R A) A — The integral closure is integrally closed in its ambient algebra, exactly Corollary 5.5.
Proposition 5.6: Integral dependence under quotients and localization
If B is integral over A, then B/𝔟 is integral over A/(A∩𝔟), and S⁻¹B is integral over S⁻¹A for multiplicative S⊂A.
Formalized. RingHom.IsIntegral.quotient; Algebra.IsIntegral.quotient; Mathlib/RingTheory/Localization/Integral.lean::isIntegral_localization — Integrality descends to the quotient with contracted base ideal and is preserved after localizing source and target at corresponding submonoids.
Proposition 5.7: Field criterion for integral domain extensions
For integral domains A⊂B with B integral over A, B is a field iff A is a field.
Formalized. Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean::Algebra.IsIntegral.isField_iff_isField — For an injective integral extension of domains, the source is a field iff the target is a field; a source inclusion supplies injectivity.
Corollary 5.8 (extraction reads “Corollary 5.3”): Maximality contracts and reflects in integral extensions
For integral B/A and prime 𝔮⊂B with 𝔭=𝔮∩A, 𝔮 is maximal iff 𝔭 is maximal. The frozen extraction mislabels this line 5.3; the proof and following 5.9 identify it as 5.8.
Formalized. Mathlib/RingTheory/Ideal/GoingUp.lean::isMaximal_of_isIntegral_of_isMaximal_comap; isMaximal_comap_of_isIntegral_of_isMaximal — For a prime upstairs in an integral extension, maximality is equivalent to maximality of its contraction.
Corollary 5.9: Incomparability over one contracted prime
If prime ideals 𝔮⊆𝔮′ of B have the same contraction to A in an integral extension, then 𝔮=𝔮′.
Formalized. Mathlib/RingTheory/Ideal/GoingUp.lean::IsIntegral.comap_lt_comap — Strict inclusion of primes upstairs forces strict inclusion of their contractions; comparable primes with the same contraction therefore coincide.
Theorem 5.10: Lying over
For integral A⊂B and prime 𝔭⊂A, there exists a prime 𝔮⊂B with 𝔮∩A=𝔭.
Formalized. Mathlib/RingTheory/Ideal/GoingUp.lean::exists_ideal_over_prime_of_isIntegral_of_isDomain; exists_ideal_over_prime_of_isIntegral — For an integral inclusion and any prime downstairs, there exists a prime upstairs contracting to it.
Theorem 5.11: Going-up theorem
For integral A⊂B, a chain of primes of B lying over an initial segment of an ascending chain of primes of A extends to a chain lying over the whole chain.
Formalized. Mathlib/RingTheory/Ideal/HasGoingUp.lean::Algebra.HasGoingUp.of_isIntegral; Ideal.exists_ltSeries_of_hasGoingUp — Integral algebras satisfy going up, and the finite strict-chain theorem lifts a whole prime chain with a prescribed initial prime.
Proposition 5.12: Integral closure commutes with localization
If C is the integral closure of A in B and S⊂A multiplicative, then S⁻¹C is the integral closure of S⁻¹A in S⁻¹B.
Formalized. Mathlib/RingTheory/Localization/Integral.lean::IsLocalization.integralClosure; IsLocalization.Away.integralClosure — The integral closure after localization is the localization of the original integral closure, exactly Proposition 5.12.
Definition: Integrally closed domain
An integral domain integrally closed in its field of fractions.
Formalized. LeanCategories/Algebra/Concrete/Rings.lean::LeanCategories.Algebra.IntegrallyClosedDomainCat — The project full subcategory is precisely domains satisfying Mathlib IsIntegrallyClosed, whose fraction-field definition matches the source.
Searched: repo HEAD
Reusable comparison: UFDs and polynomial rings are integrally closed
Z is integrally closed; the same divisibility argument gives every UFD integrally closed, hence k[x₁,…,xₙ] is integrally closed.
Formalized. Mathlib/RingTheory/Polynomial/RationalRoot.lean::UniqueFactorizationMonoid.instIsIntegrallyClosed; Mathlib/RingTheory/Polynomial/UniqueFactorization.lean::MvPolynomial.uniqueFactorizationMonoid — Every UFD is integrally closed; this covers ℤ and, over a field, finite-variable polynomial rings via their UFD structure.
Proposition 5.13: Integral closure is a local property for domains
For a domain A, A is integrally closed iff every A_𝔭 is integrally closed iff every A_𝔪 is integrally closed.
Formalized. Mathlib/RingTheory/IntegralClosure/IntegrallyClosed.lean::isIntegrallyClosed_of_isLocalization; Mathlib/RingTheory/LocalProperties/IntegrallyClosed.lean::IsIntegrallyClosed.of_localization_maximal — Integral closedness localizes at primes, and it is recovered from all maximal localizations; together these give the source prime/maximal local equivalences.
Definition: Element integral over an ideal
For A⊂B and ideal 𝔞⊂A, x∈B is integral over 𝔞 if it satisfies a monic integral-dependence equation whose nonleading coefficients all lie in 𝔞.
Not formalized. partial: Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean coefficient-witness lemmas — No checked project/P/H/external declaration defines “x integral over an ideal I” as the source coefficient condition.
Searched: N
Definition: Integral closure of an ideal in B
The set of elements of B integral over 𝔞.
Not formalized. partial: ideal-integrality witness lemmas in Mathlib/RingTheory/IntegralClosure/Algebra/Ideal.lean — No checked declaration defines the integral closure of an ideal in an ambient algebra.
Searched: N
Lemma 5.14: Integral closure of an ideal as a radical
If C is the integral closure of A in B and 𝔞^e its extension to C, then the integral closure of 𝔞 in B equals r(𝔞^e), hence is closed under addition and multiplication.
Not formalized. partial: integralClosure; ideal extension/radical APIs; IntegralClosure/Algebra/Ideal.lean — No checked theorem identifies the source ideal-integral closure with the radical of its extension to the ring integral closure.
Searched: N
Proposition 5.15: Coefficients of a minimal polynomial for an element integral over an ideal
For integrally closed domain A⊂B and x integral over 𝔞, the coefficients of the minimal polynomial of x over Frac(A) lie in r(𝔞).
Formalized. Mathlib/RingTheory/IntegralClosure/GoingDown.lean::Polynomial.coeff_mem_radical_span_coeff_of_dvd; minpoly.isIntegrallyClosed_dvd; minpoly.isIntegrallyClosed_eq_field_fractions' — From the source ideal-integrality witness polynomial, the pinned lemmas force every nonleading coefficient of the fraction-field minimal polynomial into the radical of the ideal.
Theorem 5.16: Going-down theorem
If A⊂B are domains, A integrally closed, B integral over A, then a descending prime chain of B lying over an initial segment of a descending prime chain of A extends over the full chain.
Formalized. integral-extension Algebra.HasGoingDown instance in Mathlib/RingTheory/IntegralClosure/GoingDown.lean; Mathlib/RingTheory/Ideal/GoingDown.lean::Ideal.exists_ltSeries_of_hasGoingDown — For integral extensions of an integrally closed domain, going down holds and the chain theorem realizes the source descending-prime-chain extension.
Proposition 5.17: Integral closure inside a finite separable field extension is bounded by a finite free A-module
For integrally closed domain A with fraction field K, finite separable L/K, and B the integral closure of A in L, there is a K-basis v₁,…,vₙ of L with B⊆ΣAv_j.
Formalized. Mathlib/RingTheory/DedekindDomain/IntegralClosure.lean::FiniteDimensional.exists_is_basis_integral; integralClosure_le_span_dualBasis — A finite separable field extension admits the required finite basis, and the integral closure is contained in the A-span of the dual basis, giving the source finite-free bound.
Definition: Valuation ring of a field
For a domain B with fraction field K, B is a valuation ring of K if for every x∈K×, either x∈B or x⁻¹∈B.
Formalized. LeanCategories/Algebra/Concrete/Rings.lean::LeanCategories.Algebra.ValuationRingCat; P ValuationRing.iff_isInteger_or_isInteger — The project valuation-ring category uses the exact fraction-field criterion that every nonzero fraction or its inverse lies in the ring.
Searched: repo HEAD + P
Proposition 5.18: Basic properties of valuation rings
A valuation ring B of K is local; every intermediate B⊂B′⊂K is again a valuation ring; B is integrally closed in K.
Formalized. Mathlib/RingTheory/Valuation/ValuationSubring.lean::ValuationSubring.isLocalRing; ValuationSubring.ofLE; integrally-closed instance in Mathlib/RingTheory/Valuation/LocalSubring.lean — Pinned APIs realize locality, stability under intermediate overrings, and integral closedness in the fraction field.
Construction: Zorn poset of partial homomorphism extensions
For field K and algebraically closed Ω, order pairs (A,f) with A⊂K a subring and f:A→Ω by extension; Zorn gives maximal pairs (B,g).
Formalized. P2M/Sol/S_ValuationSubring_exists_ringHom_extend_of_isAlgClosed.lean::ChevalleyHom.IsGraph; ChevalleyHom.graph; ChevalleyHom.Above; ChevalleyHom.exists_maximal — Graph subrings encode the source partial ring homomorphisms into the algebraically closed field, Above is extension of partial maps, and exists_maximal supplies the required Zorn-maximal extension.
Searched: E
Lemma 5.19: A maximal partial-homomorphism domain is local
For a maximal pair (B,g), B is local and ker g is its maximal ideal.
Formalized. P2M/Sol/S_ValuationSubring_exists_ringHom_extend_of_isAlgClosed.lean::ChevalleyHom.isLocalRing; ChevalleyHom.mem_maximalIdeal_iff — For the maximal ChevalleyHom, the graph domain is local and membership in its maximal ideal is equivalent pointwise to vanishing under the homomorphism, exactly m = ker g.
Searched: E
Lemma 5.20: One of B[x], B[x⁻¹] has proper extended maximal ideal
For x∈K× and maximal ideal 𝔪=ker g, either 𝔪[x]≠B[x] or 𝔪[x⁻¹]≠B[x⁻¹].
Not formalized. partial: polynomial-adjoin/ideal-extension APIs — No checked theorem proves for the source maximal pair that one of m[x] or m[x⁻¹] is proper.
Searched: N
Theorem 5.21: Maximal partial-homomorphism domains are valuation rings
A maximal pair (B,g) in Σ has B a valuation ring of K.
Not formalized. partial: E ChevalleyHom.main; P LocalSubring.exists_valuationRing_of_isMax — ChevalleyHom.main proves the valuation dichotomy internally for its chosen maximal graph only to export an existence theorem; neither E nor P states the source theorem for an arbitrary supplied maximal partial-homomorphism pair.
Searched: N
Corollary 5.22: Integral closure as intersection of valuation rings
For A⊂K, the integral closure of A in K is the intersection of all valuation rings of K containing A.
Formalized. Mathlib/RingTheory/Valuation/LocalSubring.lean::iInf_valuationSubring_superset — The integral closure is exactly the intersection of valuation subrings of the field containing the base ring.
Proposition 5.23: Extension of homomorphisms from a finitely generated domain
If A⊂B are domains with B finitely generated over A and v∈B nonzero, some u∈A nonzero has the property that any f:A→Ω with f(u)≠0 extends to g:B→Ω with g(v)≠0 for algebraically closed Ω.
Not formalized. partial: finite-type, localization, algebraically-closed-field APIs — No checked theorem gives the source uniform u≠0 controlling extension of every f:A→Ω to g:B→Ω while preserving g(v)≠0.
Searched: N
Run-in definition: Transcendental over A
For x in the one-generator reduction, “x transcendental over A” means no nonzero polynomial over A has x as a root.
Formalized. Mathlib/RingTheory/Algebraic/Defs.lean::Transcendental; transcendental_iff — Exactly the assertion that no nonzero polynomial over the base vanishes at the element.
Run-in definition: Algebraic over A
Here “x algebraic over A” means algebraic over the field of fractions of A.
Formalized. Mathlib/RingTheory/Algebraic/Defs.lean::IsAlgebraic, instantiated over FractionRing A; Mathlib/RingTheory/Localization/FractionRing.lean — This is precisely algebraicity over the fraction field of the base domain, matching the source convention.
Corollary 5.24: Zariski lemma / Nullstellensatz form
If k is a field and B a finitely generated k-algebra that is itself a field, then B is a finite algebraic extension of k; the text notes this as one form of Hilbert’s Nullstellensatz.
Formalized. Mathlib/RingTheory/Jacobson/Ring.lean::finite_of_finite_type_of_isJacobsonRing; Mathlib/RingTheory/Algebraic/Integral.lean::Algebra.IsAlgebraic.of_finite — A field that is finite type over a field is module-finite and hence algebraic, exactly the source Nullstellensatz/Zariski-lemma form.