Documentation

Mathlib.RingTheory.DedekindDomain.AdicValuation

Adic valuations on Dedekind domains #

Given a Dedekind domain R of Krull dimension 1 and a maximal ideal v of R, we define the v-adic valuation on R and its extension to the field of fractions K of R. We prove several properties of this valuation, including the existence of uniformizers.

We define the completion of K with respect to the v-adic valuation, denoted v.adicCompletion, and its ring of integers, denoted v.adicCompletionIntegers.

Main definitions #

Main results #

Implementation notes #

We are only interested in Dedekind domains with Krull dimension 1.

References #

Tags #

dedekind domain, dedekind ring, adic valuation

Adic valuations on the Dedekind domain R #

The additive v-adic valuation of r ∈ R is the exponent of v in the factorization of the ideal (r), if r is nonzero, or infinity, if r = 0. intValuationDef is the corresponding multiplicative valuation.

Equations
Instances For
    theorem IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r 0) :
    v.intValuationDef r = (Multiplicative.ofAdd (-((Associates.mk v.asIdeal).count (Associates.mk (Ideal.span {r})).factors)))
    theorem IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (hx : x 0) :
    v.intValuationDef x 0

    Nonzero elements have nonzero adic valuation.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero]

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero.


    Nonzero elements have nonzero adic valuation.

    Nonzero divisors have nonzero valuation.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero']

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_ne_zero'.


    Nonzero divisors have nonzero valuation.

    Nonzero divisors have valuation greater than zero.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le]

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_zero_le.


    Nonzero divisors have valuation greater than zero.

    The v-adic valuation on R is bounded above by 1.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_le_one]

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_le_one.


    The v-adic valuation on R is bounded above by 1.

    The v-adic valuation of r ∈ R is less than 1 if and only if v divides the ideal (r).

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd]

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd.


    The v-adic valuation of r ∈ R is less than 1 if and only if v divides the ideal (r).

    theorem IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (n : ) :
    v.intValuationDef r (Multiplicative.ofAdd (-n)) v.asIdeal ^ n Ideal.span {r}

    The v-adic valuation of r ∈ R is less than Multiplicative.ofAdd (-n) if and only if vⁿ divides the ideal (r).

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd]
    theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_le_pow_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) (n : ) :
    v.intValuationDef r (Multiplicative.ofAdd (-n)) v.asIdeal ^ n Ideal.span {r}

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd.


    The v-adic valuation of r ∈ R is less than Multiplicative.ofAdd (-n) if and only if vⁿ divides the ideal (r).

    The v-adic valuation of 0 : R equals 0.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero']

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_zero'.


    The v-adic valuation of 0 : R equals 0.

    The v-adic valuation of 1 : R equals 1.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_one']

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'.


    The v-adic valuation of 1 : R equals 1.

    theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (y : R) :
    v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y

    The v-adic valuation of a product equals the product of the valuations.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul']
    theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_mul' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (y : R) :
    v.intValuationDef (x * y) = v.intValuationDef x * v.intValuationDef y

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_mul'.


    The v-adic valuation of a product equals the product of the valuations.

    theorem IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le {a : } {b : } {c : } :
    Multiplicative.ofAdd (-c) max (Multiplicative.ofAdd (-a)) (Multiplicative.ofAdd (-b)) min a b c
    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le]
    theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.le_max_iff_min_le {a : } {b : } {c : } :
    Multiplicative.ofAdd (-c) max (Multiplicative.ofAdd (-a)) (Multiplicative.ofAdd (-b)) min a b c

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.le_max_iff_min_le.

    theorem IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (y : R) :
    v.intValuationDef (x + y) max (v.intValuationDef x) (v.intValuationDef y)

    The v-adic valuation of a sum is bounded above by the maximum of the valuations.

    @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max']
    theorem IsDedekindDomain.HeightOneSpectrum.IntValuation.map_add_le_max' {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (x : R) (y : R) :
    v.intValuationDef (x + y) max (v.intValuationDef x) (v.intValuationDef y)

    Alias of IsDedekindDomain.HeightOneSpectrum.intValuation.map_add_le_max'.


    The v-adic valuation of a sum is bounded above by the maximum of the valuations.

    @[simp]
    theorem IsDedekindDomain.HeightOneSpectrum.intValuation_toFun {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) :
    v.intValuation r = v.intValuationDef r

    The v-adic valuation on R.

    Equations
    • v.intValuation = { toFun := v.intValuationDef, map_zero' := , map_one' := , map_mul' := , map_add_le_max' := }
    Instances For
      theorem IsDedekindDomain.HeightOneSpectrum.intValuation_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {r : R} (v : IsDedekindDomain.HeightOneSpectrum R) :
      v.intValuation r = v.intValuationDef r
      theorem IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) :
      ∃ (π : R), v.intValuationDef π = (Multiplicative.ofAdd (-1))

      There exists π ∈ R with v-adic valuation Multiplicative.ofAdd (-1).

      @[deprecated IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer]
      theorem IsDedekindDomain.HeightOneSpectrum.int_valuation_exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) :
      ∃ (π : R), v.intValuationDef π = (Multiplicative.ofAdd (-1))

      Alias of IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer.


      There exists π ∈ R with v-adic valuation Multiplicative.ofAdd (-1).

      theorem IsDedekindDomain.HeightOneSpectrum.intValuation_singleton {R : Type u_1} [CommRing R] [IsDedekindDomain R] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} (hr : r 0) (hv : v.asIdeal = Ideal.span {r}) :
      v.intValuation r = (Multiplicative.ofAdd (-1))

      The I-adic valuation of a generator of I equals (-1 : ℤₘ₀)

      Adic valuations on the field of fractions K #

      The v-adic valuation of x ∈ K is the valuation of r divided by the valuation of s, where r and s are chosen so that x = r/s.

      Equations
      • v.valuation = v.intValuation.extendToLocalization K
      Instances For
        theorem IsDedekindDomain.HeightOneSpectrum.valuation_def {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (x : K) :
        v.valuation x = (v.intValuation.extendToLocalization K) x
        theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_mk' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {r : R} {s : (nonZeroDivisors R)} :
        v.valuation (IsLocalization.mk' K r s) = v.intValuation r / v.intValuation s

        The v-adic valuation of r/s ∈ K is the valuation of r divided by the valuation of s.

        theorem IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) :
        v.valuation ((algebraMap R K) r) = v.intValuation r

        The v-adic valuation on K extends the v-adic valuation on R.

        theorem IsDedekindDomain.HeightOneSpectrum.valuation_eq_intValuationDef {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) :
        v.valuation r = v.intValuationDef r

        The v-adic valuation on R is bounded above by 1.

        theorem IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) :
        v.valuation ((algebraMap R K) r) < 1 v.asIdeal Ideal.span {r}

        The v-adic valuation of r ∈ R is less than 1 if and only if v divides the ideal (r).

        theorem IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer {R : Type u_1} [CommRing R] [IsDedekindDomain R] (K : Type u_2) [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) :
        ∃ (π : K), v.valuation π = (Multiplicative.ofAdd (-1))

        There exists π ∈ K with v-adic valuation Multiplicative.ofAdd (-1).

        Completions with respect to adic valuations #

        Given a Dedekind domain R with field of fractions K and a maximal ideal v of R, we define the completion of K with respect to its v-adic valuation, denoted v.adicCompletion, and its ring of integers, denoted v.adicCompletionIntegers.

        K as a valued field with the v-adic valuation.

        Equations
        Instances For
          theorem IsDedekindDomain.HeightOneSpectrum.adicValued_apply {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {x : K} :
          Valued.v x = v.valuation x
          @[reducible, inline]

          The completion of K with respect to its v-adic valuation.

          Equations
          Instances For
            theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (r : R) :
            Valued.v r = v.valuation r

            The valuation on the completion agrees with the global valuation on elements of the integer ring.

            theorem IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation' {R : Type u_1} [CommRing R] [IsDedekindDomain R] {K : Type u_2} [Field K] [Algebra R K] [IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) (k : K) :
            Valued.v (K k) = v.valuation k

            The valuation on the completion agrees with the global valuation on elements of the field.