# 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 of S-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's S-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} [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
(S.integer K) = {x : K | vS, v.valuation x 1}
def Set.integer {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra 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
theorem Set.integer_eq {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
(S.integer K).toSubring = ⨅ (v : ), ⨅ (_ : vS), v.valuation.valuationSubring.toSubring
theorem Set.integer_valuation_le_one {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : (S.integer K)) (hv : vS) :
v.valuation x 1

## S-units #

@[simp]
theorem Set.unit_coe {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
(S.unit K) = {x : Kˣ | vS, v.valuation x = 1}
def Set.unit {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] :

The subgroup of S-units of Kˣ.

Equations
• S.unit K = (⨅ (v : ), ⨅ (_ : vS), v.valuation.valuationSubring.unitGroup).copy {x : Kˣ | vS, v.valuation x = 1}
Instances For
theorem Set.unit_eq {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
S.unit K = ⨅ (v : ), ⨅ (_ : vS), v.valuation.valuationSubring.unitGroup
theorem Set.unit_valuation_eq_one {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : (S.unit K)) (hv : vS) :
v.valuation x = 1
@[simp]
theorem Set.unitEquivUnitsInteger_symm_apply_coe {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : ((S.integer K))ˣ) :
((S.unitEquivUnitsInteger K).symm x) = Units.mk0 x
@[simp]
theorem Set.val_unitEquivUnitsInteger_apply_coe {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : (S.unit K)) :
((S.unitEquivUnitsInteger K) x) = x
def Set.unitEquivUnitsInteger {R : Type u} [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
(S.unit K) ≃* ((S.integer 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