# Documentation

Mathlib.RingTheory.DedekindDomain.SInteger

# 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] [] :
↑() = {x | ∀ (v : ), ¬v S}
def Set.integer {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] :

The R-subalgebra of S-integers of K.

Instances For
theorem Set.integer_eq {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
= ⨅ (v : ) (_ : ¬v S),
theorem Set.integer_valuation_le_one {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : { x // x }) (hv : ¬v S) :

## S-units #

@[simp]
theorem Set.unit_coe {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
↑(Set.unit S K) = {x | ∀ (v : ), ¬v S}
def Set.unit {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] :

The subgroup of S-units of Kˣ.

Instances For
theorem Set.unit_eq {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
Set.unit S K =
theorem Set.unit_valuation_eq_one {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : { x // x Set.unit S K }) (hv : ¬v S) :
@[simp]
theorem Set.unitEquivUnitsInteger_symm_apply_coe {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : { x // x }ˣ) :
↑(↑() x) = Units.mk0 x (_ : x = 0False)
@[simp]
theorem Set.val_unitEquivUnitsInteger_apply_coe {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] (x : { x // x Set.unit S K }) :
↑(↑() x) = x
def Set.unitEquivUnitsInteger {R : Type u} [] [] [] (S : ) (K : Type v) [] [Algebra R K] [] :
{ x // x Set.unit S K } ≃* { x // x }ˣ

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

Instances For