# mathlib3documentation

ring_theory.dedekind_domain.S_integer

# 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 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 , where K can be specialised to the case of a number field or a function field separately.

## Main statements #

• set.unit_equiv_units_integer: 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.

## 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] (K : Type v) [field K] [ K] [ K] :
(S.integer K).carrier = (( (v : (H : v S), v.valuation.valuation_subring.to_subring).copy {x : K | (v : , v S (v.valuation) x 1} _).carrier
def set.integer {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] :
K

The R-subalgebra of S-integers of K.

Equations
theorem set.integer_eq {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] :
theorem set.integer_valuation_le_one {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] (x : (S.integer K)) (hv : v S) :

## S-units #

@[simp]
theorem set.unit_coe {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] :
(S.unit K) = {x : Kˣ | (v : , v S (v.valuation) x = 1}
noncomputable def set.unit {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] :

The subgroup of S-units of .

Equations
theorem set.unit_eq {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] :
theorem set.unit_valuation_eq_one {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] (x : (S.unit K)) (hv : v S) :
@[simp]
theorem set.unit_equiv_units_integer_symm_apply_coe {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] (x : ((S.integer K))ˣ) :
@[simp]
theorem set.coe_unit_equiv_units_integer_apply_coe {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ 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] (K : Type v) [field K] [ K] [ K] (x : (S.unit K)) :
noncomputable def set.unit_equiv_units_integer {R : Type u} [comm_ring R] [is_domain R] (K : Type v) [field K] [ K] [ K] :
(S.unit K) ≃* ((S.integer K))ˣ

The group of S-units is the group of units of the ring of S-integers.

Equations