`S`-integers and `S`-units of fraction fields of Dedekind domains #

Let K be the field of fractions of a Dedekind domain R, and let S be a set of prime ideals in the height one spectrum of R. An S-integer of K is defined to have v-adic valuation at most one for all primes ideals v away from S, whereas an S-unit of Kˣ is defined to have v-adic valuation exactly one for all prime ideals v away from S.

This file defines the subalgebra of S-integers of K and the subgroup of S-units of Kˣ, where K can be specialised to the case of a number field or a function field separately.

Main definitions #

Set.integer: S-integers.
Set.unit: S-units.
TODO: localised notation for S-integers.

Main statements #

Set.unitEquivUnitsInteger: S-units are units of S-integers.
IsDedekindDomain.integer_empty: ∅-integers is the usual ring of integers.
TODO: proof that S-units is the kernel of a map to a product.
TODO: finite generation of S-units and Dirichlet's S-unit theorem.

References #

[D Marcus, Number Fields][marcus1977number]
[J W S Cassels, A Fröhlich, Algebraic Number Theory][cassels1967algebraic]
[J Neukirch, Algebraic Number Theory][Neukirch1992]

Tags #

S integer, S-integer, S unit, S-unit

`S`-integers #

source

def Set.integer {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :

Subalgebra R K

The R-subalgebra of S-integers of K.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[simp]

theorem Set.coe_integer {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :

↑(S.integer K) = {x : K | ∀ v ∉ S, (IsDedekindDomain.HeightOneSpectrum.valuation K v) x ≤ 1}

source

theorem Set.integer_eq {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :

(S.integer K).toSubring = ⨅ (v : IsDedekindDomain.HeightOneSpectrum R), ⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.toSubring

source

theorem Set.integer_valuation_le_one {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (x : ↥(S.integer K)) {v : IsDedekindDomain.HeightOneSpectrum R} (hv : v ∉ S) :

(IsDedekindDomain.HeightOneSpectrum.valuation K v) ↑x ≤ 1

source

@[simp]

theorem IsDedekindDomain.integer_univ (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :

Set.univ.integer K = ⊤

If S is the whole set of places of K, then the S-integers are the whole of K.

source

@[simp]

theorem IsDedekindDomain.integer_empty (R : Type u) [CommRing R] [IsDedekindDomain R] (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :

∅.integer K = ⊥

If S is the empty set, then the S-integers are the minimal R-subalgebra of K (which is just R itself, via Algebra.botEquivOfInjective and IsFractionRing.injective).