The ring of S-integers of a Dedekind domain is a Dedekind domain #
Let R be a Dedekind domain with fraction field K and S a set of height-one primes of R.
Mathlib/RingTheory/DedekindDomain/SInteger.lean defines the subalgebra of S-integers
{x : K | ∀ v ∉ S, v x ≤ 1} as Set.integer S K, but proves nothing about its ring
structure.
This file shows it is again a Dedekind domain, as anonymous instances: IsIntegrallyClosed,
IsNoetherianRing and Ring.DimensionLEOne are proved for S.integer K, and the
IsDedekindDomain instance is then inferred.
The key step is integer_map_comap_eq: every ideal of the S-integers is generated by its
contraction to R, proved through the denominator ideal Algebra.denIdeal K x = (R : x) of
an element of K. That contraction is packaged as IsDedekindDomain.integerIdealUnder — Mathlib's
Ideal.under —
carrying nonzeroness along (integer_comap_ne_bot) so it lands in (Ideal R)⁰ — the dual of
Mathlib's ClassGroup.extendedIdeal, and the ideal-level companion of the spectrum-level
integerPrimeUnder.
Note that the S-integers are not in general a localization of R, so the ring has to be
handled as a general overring of R rather than a ring of fractions. Localizing at
{r : R | r ≠ 0 ∧ ∀ v ∉ S, v r = 1} can give a strictly smaller ring: if Cl(R) ≅ ℤ is
generated by the class of a single prime v and S = {v}, no power v ^ k with k ≠ 0 is
principal, so that monoid is just the units of R, yet the S-integers strictly contain R.
This is a prerequisite for the Selmer-group finiteness that
TauCetiRoadmap/EllipticCurves/README.md §Layer 6 needs for weak Mordell–Weil: the S-class
group and S-units in that statement are those of this ring.
Adapted from Michael Stoll's elliptic-curves formalisation
(github.com/MichaelStollBayreuth/EllipticCurves, EllipticCurves/Mathlib/SIntegers.lean at the
roadmap's pin 66889eada51a, Apache 2.0, by Michael Stoll), which the roadmap names as the
provenance for its Layer 6 Mordell–Weil lane. Following this repository's convention for adapted
material, the upstream authorship is credited here rather than in the copyright header. Ported
with the source's blanket import Mathlib narrowed to the modules actually used. The
class-group half of that source file is
TauCeti/RingTheory/DedekindDomain/SInteger/ClassGroup.lean, which computes Cl(𝒪_S) as
IsDedekindDomain.integerClassGroupEquiv and consumes this file.
Membership in the S-integers is the valuation condition defining it. Mathlib states
Set.integer through Subalgebra.copy, but provides no membership lemma; this is it.
The ring of S-integers is integrally closed: it is an intersection of valuation subrings
of K, each of which is integrally closed in K.
Primes in S become the unit ideal #
For v ∈ S the inverse v⁻¹ of v as a fractional ideal consists of S-integers, because an
element y with y * v ⊆ R can have a pole only at v. As v * v⁻¹ = 1, the extension of
v
to 𝒪_S is therefore the unit ideal, which is what makes 𝒪_S bigger than R. This is where
the invertibility of nonzero ideals is used — the Dedekind property enters elsewhere too,
through Noetherianity and dimension one.
An element of the inverse fractional ideal v⁻¹ is w-integral at every height-one prime
w ≠ v: it can have a pole only at v.
For v ∈ S, the extension of v to the ring of S-integers is the unit ideal.
Ideals of 𝒪_S are extended from R #
Let I be an ideal of 𝒪_S and J = I ∩ R its contraction. For x ∈ I the denominator ideal
𝔡 x = {r : R | r * x ∈ R} is divisible only by primes in S, because x is w-integral for
w ∉ S. Hence 𝔡 x * 𝒪_S = ⊤ by integer_map_asIdeal_eq_top, so 1 = ∑ dᵢ cᵢ with dᵢ ∈ 𝔡 x and
cᵢ ∈ 𝒪_S, and x = ∑ (dᵢ * x) * cᵢ exhibits x as an element of J * 𝒪_S, since
dᵢ * x ∈ R ∩ I = J.
Noetherianity is immediate from this: J is finitely generated as R is Noetherian, hence so
is its extension I.
The denominator ideal of an element that is integral at a prime w — that is,
w.valuation K x ≤ 1, the only hypothesis taken — is not contained in w.asIdeal: integrality
at w produces a denominator away from w.
The denominator ideal of an S-integer extends to the unit ideal of 𝒪_S: all its prime
factors lie in S, and each of those extends to the unit ideal by integer_map_asIdeal_eq_top.
Every ideal of 𝒪_S is extended from R.
The Dedekind property #
The ring of S-integers is Noetherian: every ideal is extended from the Noetherian
ring R by integer_map_comap_eq.
The contraction to R of any nonzero ideal of 𝒪_S is nonzero: if it were zero, the ideal
would be map ⊥ = ⊥ by integer_map_comap_eq.
The contraction to R of a nonzero ideal of 𝒪_S, as a nonzero ideal. The dual of Mathlib's
ClassGroup.extendedIdeal, and the ideal-level companion of the spectrum-level
integerPrimeUnder.
Equations
- IsDedekindDomain.integerIdealUnder K S I = ⟨Ideal.under R ↑I, ⋯⟩
Instances For
The ring of S-integers has Krull dimension at most 1: the contraction to R of a
nonzero prime is maximal, and equalities of ideals lift back through integer_map_comap_eq.
The ring of S-integers of a Dedekind domain is a Dedekind domain.