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 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.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem Set.coe_integer {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :
    (S.integer K) = {x : K | vS, v.valuation x 1}

    S-units #

    The subgroup of S-units of .

    Equations
    Instances For
      @[simp]
      theorem Set.coe_unit {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] :
      (S.unit K) = {x : Kˣ | vS, v.valuation x = 1}
      theorem Set.unit_valuation_eq_one {R : Type u} [CommRing R] [IsDedekindDomain R] (S : Set (IsDedekindDomain.HeightOneSpectrum R)) (K : Type v) [Field K] [Algebra R K] [IsFractionRing R K] (x : (S.unit K)) {v : IsDedekindDomain.HeightOneSpectrum R} (hv : vS) :
      v.valuation x = 1

      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