Theorems · Definition · number theory

Rat.HeightOneSpectrum.withValEquiv

{R : Type u_2} →
  [inst : CommRing R] →
    [inst_1 : Algebra R ℚ] →
      [inst_2 : IsIntegralClosure R ℤ ℚ] →
        [inst_3 : IsDedekindDomain R] →
          [inst_4 : IsFractionRing R ℚ] →
            (v : IsDedekindDomain.HeightOneSpectrum R) →
              WithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v) ≃ᵤ
                WithVal (Rat.padicValuation ↑(Rat.HeightOneSpectrum.primesEquiv v))

The uniform space isomorphism ℚ ≃ᵤ ℚ, where the LHS has the uniformity from HeightOneSpectrum.valuation ℚ v and the RHS has uniformity from Rat.padicValuation (natGenerator v), for a height-one prime ideal v : HeightOneSpectrum R.

Defined in

Mathlib.NumberTheory.Padics.HeightOneSpectrum

Cited by

0 results in Mathlib

Foundations

Depth 169 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingAlgebraIsIntegralClosureIsDedekindDomainIsFractionRing