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 #
@[simp]
theorem
Set.integer_carrier
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
↑(Set.integer S K) = {x | ∀ (v : IsDedekindDomain.HeightOneSpectrum R), ¬v ∈ S → ↑(IsDedekindDomain.HeightOneSpectrum.valuation v) x ≤ 1}
def
Set.integer
{R : Type u}
[CommRing R]
[IsDomain 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.
Instances For
theorem
Set.integer_eq
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
Subalgebra.toSubring (Set.integer S K) = ⨅ (v : IsDedekindDomain.HeightOneSpectrum R) (_ : ¬v ∈ S),
(Valuation.valuationSubring (IsDedekindDomain.HeightOneSpectrum.valuation v)).toSubring
theorem
Set.integer_valuation_le_one
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(x : { x // x ∈ Set.integer S K })
{v : IsDedekindDomain.HeightOneSpectrum R}
(hv : ¬v ∈ S)
:
S-units #
@[simp]
theorem
Set.unit_coe
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
↑(Set.unit S K) = {x | ∀ (v : IsDedekindDomain.HeightOneSpectrum R), ¬v ∈ S → ↑(IsDedekindDomain.HeightOneSpectrum.valuation v) ↑x = 1}
def
Set.unit
{R : Type u}
[CommRing R]
[IsDomain 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ˣ.
Instances For
theorem
Set.unit_eq
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
:
Set.unit S K = ⨅ (v : IsDedekindDomain.HeightOneSpectrum R) (_ : ¬v ∈ S),
ValuationSubring.unitGroup (Valuation.valuationSubring (IsDedekindDomain.HeightOneSpectrum.valuation v))
theorem
Set.unit_valuation_eq_one
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(x : { x // x ∈ Set.unit S K })
{v : IsDedekindDomain.HeightOneSpectrum R}
(hv : ¬v ∈ S)
:
↑(IsDedekindDomain.HeightOneSpectrum.valuation v) ↑↑x = 1
@[simp]
theorem
Set.unitEquivUnitsInteger_symm_apply_coe
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(x : { x // x ∈ Set.integer S K }ˣ)
:
↑(↑(MulEquiv.symm (Set.unitEquivUnitsInteger S K)) x) = Units.mk0 ↑↑x (_ : ↑↑x = 0 → False)
@[simp]
theorem
Set.val_unitEquivUnitsInteger_apply_coe
{R : Type u}
[CommRing R]
[IsDomain R]
[IsDedekindDomain R]
(S : Set (IsDedekindDomain.HeightOneSpectrum R))
(K : Type v)
[Field K]
[Algebra R K]
[IsFractionRing R K]
(x : { x // x ∈ Set.unit S K })
:
↑↑(↑(Set.unitEquivUnitsInteger S K) x) = ↑↑x
def
Set.unitEquivUnitsInteger
{R : Type u}
[CommRing R]
[IsDomain 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.