S-integers and S-units of fraction fields of Dedekind domains #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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.