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 ofS-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'sS-unit theorem.
References #
- D Marcus, Number Fields
- J W S Cassels, A Fröhlich, Algebraic Number Theory
- J Neukirch, Algebraic Number Theory
Tags #
S integer, S-integer, S unit, S-unit
S-integers #
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
@[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]
:
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
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)
:
@[simp]
theorem
IsDedekindDomain.integer_univ
(R : Type u)
[CommRing R]
[IsDedekindDomain R]
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
If S is the whole set of places of K, then the S-integers are the whole of K.
@[simp]
theorem
IsDedekindDomain.integer_empty
(R : Type u)
[CommRing R]
[IsDedekindDomain R]
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R 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).
S-units #
def
Set.unit
{R : Type u}
[CommRing R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
The subgroup of S-units of Kˣ.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Set.coe_unit
{R : Type u}
[CommRing R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
theorem
Set.unit_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.unit K = ⨅ (v : IsDedekindDomain.HeightOneSpectrum R),
⨅ (_ : v ∉ S), (IsDedekindDomain.HeightOneSpectrum.valuation K v).valuationSubring.unitGroup
theorem
Set.unit_valuation_eq_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.unit K))
{v : IsDedekindDomain.HeightOneSpectrum R}
(hv : v ∉ S)
:
def
Set.unitEquivUnitsInteger
{R : Type u}
[CommRing R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
The group of S-units is the group of units of the ring of S-integers.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Set.val_unitEquivUnitsInteger_apply_coe
{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.unit K))
:
@[simp]
theorem
Set.unitEquivUnitsInteger_symm_apply_coe
{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))ˣ)
: