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 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 definitions #

Main statements #

References #

Tags #

S integer, S-integer, S unit, S-unit

S-integers #

The R-subalgebra of S-integers of K.

Instances For

    S-units #

    The subgroup of S-units of .

    Instances For
      theorem Set.unitEquivUnitsInteger_symm_apply_coe {R : Type u} [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (x : { x // x Set.integer S K }ˣ) :
      ↑(↑(MulEquiv.symm (Set.unitEquivUnitsInteger S K)) x) = Units.mk0 x (_ : x = 0False)
      theorem Set.val_unitEquivUnitsInteger_apply_coe {R : Type u} [CommRing R] [IsDomain R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (x : { x // x Set.unit S K }) :
      ↑(↑(Set.unitEquivUnitsInteger S K) x) = x

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

      Instances For