Chapter 9. Discrete Valuation Rings and Dedekind Domains (pp. 93–98)
FC04 — Atiyah & Macdonald, Introduction to Commutative Algebra.
This chapter contains 8 definitions, 3 theorems, 4 propositions, 2 corollaries, 4 examples, 3 constructions and 5 other statements.
Of the 1 statements checked against Lean, 1 are formalized somewhere and 0 are not.
| Status | Statements | Share | What it means |
|---|---|---|---|
| in Mathlib | 1 | 100% | Mathlib states and proves it. |
| checked in total | 1 |
- Project search:
LeanCategories/**outside.lake/.agents/.gitwas searched first. Project HEAD351cba0287077eadfcd7c71a78ec4a509ce8c966explicitly reifies discrete valuation rings and Dedekind domains inLeanCategories/Algebra/Concrete/Rings.lean; those definition rows areproject-existing.LeanCategories/Algebra/FractionalIdeals.leanonly wraps Mathlib’s fractional-ideal/class-group APIs (InvertibleFractionalIdeal,idealClass, principal/trivial-class lemmas, integral-class surjectivity) and does not own a complete U016–U029 source row. - Pinned Mathlib: project pin
db584cd6d46c92f209a44c0f1c829460d327499d(Apache-2.0, Lean v4.33.0), denotedP, contains the DVR TFAE, Dedekind local equivalence, adic valuations, fractional-ideal inversion, ideal factorization, class-group, class-number, and Dirichlet-unit interfaces below. The nontrivial U001 product conversion, U009 primary-power direction, and U024 finite-support/reconstruction bundles were compile-checked against P. - Current/open Mathlib: upstream
5aedf732b6987e8c26ab3c9ebc855314f82b045f(Apache-2.0), denotedH, was refreshed 2026-09-06 and preserves the checked interfaces. Targeted current/open and indexed external searches were used for U013, U020, U021, U028, and U029. - Source defect: the frozen Proposition 9.7 row U021 is false as printed at the field edge under the chapter’s preceding DVR definition: a field is a local domain whose only nonzero fractional ideal is invertible, but a field does not admit the source’s surjective discrete valuation
Kˣ→ℤ. The mapping therefore records the row as unmatched rather than silently adding a nonfield hypothesis. Ndenotes dated 2026-09-06 negative evidence after project-first search, P/H, open/current work, installed packages, and targeted external Lean search. A concrete number-ring example is not credited from separate abstract number-field and Gaussian/Pell infrastructure without the required bridge.
Proposition: Proposition 9.1
In a Noetherian domain of dimension 1, every nonzero ideal has a unique expression as a product of primary ideals with pairwise distinct radicals.
Formalized. Mathlib/RingTheory/Lasker.lean::Submodule.isLasker; IsLasker.exists_isMinimalPrimaryDecomposition; IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf; Mathlib/RingTheory/KrullDimension/Basic.lean::Ideal.IsPrime.isMaximal_of_ne_bot; Mathlib/RingTheory/Finiteness/Ideal.lean::Ideal.exists_radical_pow_le_of_fg; Mathlib/RingTheory/Ideal/Operations.lean::Ideal.prod_eq_iInf_of_pairwise_isCoprime — For a nonzero ideal in a one-dimensional Noetherian domain, a minimal primary decomposition has nonzero prime radicals, hence distinct maximal radicals. Suitable powers of these radicals lie in the components, making distinct components coprime, so their intersection is their product. All associated primes are isolated, so the second uniqueness theorem makes each primary component canonical. The product/existence assembly was compile-checked against P.
Comparison: Prime-power primary ideals and ideal factorization
If every primary ideal in a Noetherian one-dimensional domain is a prime power, then nonzero ideals factor uniquely into prime ideals; localization at a nonzero prime has every nonzero ideal a power of its maximal ideal.
Definition: Discrete valuation
A discrete valuation on a field K is a surjection v:K*→Z satisfying v(xy)=v(x)+v(y) and v(x+y)≥min(v(x),v(y)).
Construction / comparison: Valuation ring attached to a discrete valuation
The valuation ring of v is {0}∪{x∈K*:v(x)≥0}; the source also permits the convention v(0)=+∞.
Examples: p-adic and f-adic discrete valuations
For K=Q, v_p has valuation ring Z_(p); for K=k(x) and irreducible f∈k[x], v_f has valuation ring k[x]_(f).
Definition: Discrete valuation ring
An integral domain A is a discrete valuation ring when it is the valuation ring of a discrete valuation of its fraction field K; then A is local and m={x∈K:v(x)>0}.
Construction / comparison: Ideal structure and a value-one generator in a DVR
Equal valuation gives associated elements and the same principal ideal. Every nonzero ideal is m_k={y∈A:v(y)≥k}; choosing x with v(x)=1 gives m=(x), m_k=(x^k), and A is a Noetherian local domain of dimension 1 with m its only nonzero prime.
Proposition: Proposition 9.2
For a Noetherian local domain A of dimension 1 with maximal ideal m and residue field k, the following are equivalent: A is a DVR; A is integrally closed; m is principal; dim_k(m/m²)=1; every nonzero ideal is a power of m; there is x∈A such that every nonzero ideal is (x^k), k≥0.
Theorem: Theorem 9.3
For a Noetherian domain A of dimension 1, the following are equivalent: A is integrally closed; every primary ideal is a prime power; for every nonzero prime p, A_p is a DVR.
Definition: Dedekind domain
A ring satisfying the equivalent conditions of Theorem 9.3 is called a Dedekind domain.
Corollary: Corollary 9.4
Every nonzero ideal in a Dedekind domain factors uniquely as a product of prime ideals.
Example: Principal ideal domains are Dedekind
Every principal ideal domain is Dedekind: it is Noetherian of dimension 1 and its nonzero-prime localizations are DVRs.
Definition / construction: Ring of integers of a number field
For a finite algebraic extension K/Q, its ring of integers A is the integral closure of Z in K; for K=Q(i), A=Z[i].
Theorem: Theorem 9.5
The ring of integers of an algebraic number field is a Dedekind domain.
Named comparison: Primary decomposition as a generalization of ideal factorization
The source compares 9.4 with Chapter 4 uniqueness: prime powers are replaced by primary ideals, and products by intersections.
Definition / notation: Fractional, integral, and principal ideals; (A:M)
For a domain A with fraction field K, an A-submodule M⊆K is fractional if xM⊆A for some 0≠x∈A. Ordinary ideals are called integral ideals; (u)=Au is principal; (A:M)={x∈K:xM⊆A}.
Comparison: Finite generation of fractional ideals
Every finitely generated A-submodule of K is fractional; conversely, if A is Noetherian, every fractional ideal is finitely generated and has the form x⁻¹a for an integral ideal a.
Definition: Invertible ideal
An A-submodule M⊆K is invertible if MN=A for some N⊆K. The inverse is unique and equals (A:M); every invertible ideal is finitely generated and hence fractional.
Construction / comparison: Group of invertible fractional ideals
Every nonzero principal fractional ideal (u) is invertible with inverse (u⁻¹); the invertible ideals form a multiplicative group with identity A=(1).
Proposition: Proposition 9.6 (invertibility is local)
For a fractional ideal M, invertibility is equivalent to finite generation plus invertibility of every M_p, and equivalently to finite generation plus invertibility of every M_m for maximal m.
Proposition: Proposition 9.7
A local domain A is a DVR if and only if every nonzero fractional ideal of A is invertible.
Theorem: Theorem 9.8
An integral domain A is Dedekind if and only if every nonzero fractional ideal of A is invertible.
Corollary: Corollary 9.9
In a Dedekind domain, the nonzero fractional ideals form a group under multiplication.
Definition / comparison: Group of ideals I
For a Dedekind domain, the group of nonzero fractional ideals is denoted I; by 9.4 it is the free abelian group on the nonzero prime ideals.
Definition / construction: Principal ideals, ideal class group, and unit exact sequence
The map φ:K→I, u↦(u), has image P (principal fractional ideals) and kernel U=A. The ideal class group is H=I/P, giving 1→U→K*→I→H→1.
Named classical comparison: Class number criterion for rings of integers
For the ring of integers A of a number field, H is finite; h=|H| is the class number, and h=1 ⇔ I=P ⇔ A is a PID ⇔ A is a UFD.
Named classical comparison: Structure of the unit group of a number field
For a number field, the torsion units form the finite cyclic group W of roots of unity and U/W is free abelian of rank r₁+r₂−1, where r₁+2r₂=[K:Q].
Example: Units of Z[i]
For K=Q(i), r₁=0,r₂=1 and the units of Z[i] are exactly ±1,±i.
Example: Units of Z[√2]
For K=Q(√2), r₁=2,r₂=0, W={±1}, U/W is infinite cyclic, and the units are ±(1+√2)^n for n∈Z.