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.unit_equiv_units_integer
: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
- J W S Cassels, A Frölich, Algebraic Number Theory
- J Neukirch, Algebraic Number Theory
Tags #
S integer, S-integer, S unit, S-unit
S
-integers #
@[simp]
theorem
set.integer_carrier
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
(S.integer K).carrier = ((⨅ (v : is_dedekind_domain.height_one_spectrum R) (H : v ∉ S), v.valuation.valuation_subring.to_subring).copy {x : K | ∀ (v : is_dedekind_domain.height_one_spectrum R), v ∉ S → ⇑(v.valuation) x ≤ 1} _).carrier
def
set.integer
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
subalgebra R K
The R
-subalgebra of S
-integers of K
.
Equations
- S.integer K = {carrier := ((⨅ (v : is_dedekind_domain.height_one_spectrum R) (H : v ∉ S), v.valuation.valuation_subring.to_subring).copy {x : K | ∀ (v : is_dedekind_domain.height_one_spectrum R), v ∉ S → ⇑(v.valuation) x ≤ 1} _).carrier, mul_mem' := _, one_mem' := _, add_mem' := _, zero_mem' := _, algebra_map_mem' := _}
theorem
set.integer_eq
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
(S.integer K).to_subring = ⨅ (v : is_dedekind_domain.height_one_spectrum R) (H : v ∉ S), v.valuation.valuation_subring.to_subring
theorem
set.integer_valuation_le_one
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K]
(x : ↥(S.integer K))
{v : is_dedekind_domain.height_one_spectrum R}
(hv : v ∉ S) :
S
-units #
@[simp]
theorem
set.unit_coe
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
noncomputable
def
set.unit
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
The subgroup of S
-units of Kˣ
.
Equations
- S.unit K = (⨅ (v : is_dedekind_domain.height_one_spectrum R) (H : v ∉ S), v.valuation.valuation_subring.unit_group).copy {x : Kˣ | ∀ (v : is_dedekind_domain.height_one_spectrum R), v ∉ S → ⇑(v.valuation) ↑x = 1} _
theorem
set.unit_eq
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
S.unit K = ⨅ (v : is_dedekind_domain.height_one_spectrum R) (H : v ∉ S), v.valuation.valuation_subring.unit_group
theorem
set.unit_valuation_eq_one
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K]
(x : ↥(S.unit K))
{v : is_dedekind_domain.height_one_spectrum R}
(hv : v ∉ S) :
@[simp]
theorem
set.unit_equiv_units_integer_symm_apply_coe
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K]
(x : (↥(S.integer K))ˣ) :
@[simp]
theorem
set.coe_unit_equiv_units_integer_apply_coe
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K]
(x : ↥(S.unit K)) :
@[simp]
theorem
set.coe_inv_unit_equiv_units_integer_apply_coe
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K]
(x : ↥(S.unit K)) :
noncomputable
def
set.unit_equiv_units_integer
{R : Type u}
[comm_ring R]
[is_domain R]
[is_dedekind_domain R]
(S : set (is_dedekind_domain.height_one_spectrum R))
(K : Type v)
[field K]
[algebra R K]
[is_fraction_ring R K] :
The group of S
-units is the group of units of the ring of S
-integers.