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.- TODO: proof that
S-units is the kernel of a map to a product. - TODO: proof that
∅-integers is the usual ring of integers. - TODO: finite generation of
S-units and Dirichlet'sS-unit theorem.
References #
- [D Marcus, Number Fields][marcus1977number]
- [J W S Cassels, A Frölich, Algebraic Number Theory][cassels1967algebraic]
- [J Neukirch, Algebraic Number Theory][Neukirch1992]
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.integer_carrier
{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), v.valuation.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)
:
v.valuation ↑x ≤ 1
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
- S.unit K = (⨅ (v : IsDedekindDomain.HeightOneSpectrum R), ⨅ (_ : v ∉ S), v.valuation.valuationSubring.unitGroup).copy {x : Kˣ | ∀ v ∉ S, v.valuation ↑x = 1} ⋯
Instances For
@[simp]
theorem
Set.unit_coe
{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), v.valuation.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)
:
v.valuation ↑↑x = 1
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.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))ˣ)
:
@[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))
:
↑↑((S.unitEquivUnitsInteger K) x) = ↑↑x