Documentation

Mathlib.NumberTheory.Padics.HeightOneSpectrum

Isomorphisms between `adicCompletion ℚ` and `ℚ_[p]` #

Let R have field of fractions ℚ. If v : HeightOneSpectrum R, then v.adicCompletion ℚ is the uniform space completion of ℚ with respect to the v-adic valuation. On the other hand, ℚ_[p] is the p-adic numbers, defined as the completion of ℚ with respect to the p-adic norm using the completion of Cauchy sequences. This file constructs continuous ℚ-algebra isomorphisms between the two, as well as continuous ℤ-algebra isomorphisms for their respective rings of integers.

Isomorphisms are provided in both directions, allowing traversal of the following diagram:

HeightOneSpectrum R <----------->  Nat.Primes
          |                               |
          |                               |
          v                               v
v.adicCompletionIntegers ℚ  <------->   ℤ_[p]
          |                               |
          |                               |
          v                               v
v.adicCompletion ℚ  <--------------->   ℚ_[p]

Main definitions #

Rat.HeightOneSpectrum.primesEquiv : the equivalence between height-one prime ideals of R and prime numbers in ℕ.
Rat.HeightOneSpectrum.padicEquiv v : the continuous ℚ-algebra isomorphism v.adicCompletion ℚ ≃A[ℚ] ℚ_[primesEquiv v].
Padic.adicCompletionEquiv p : the continuous ℚ-algebra isomorphism ℚ_[p] ≃A[ℚ] (primesEquiv.symm p).adicCompletion ℚ.
Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv v : the continuous ℤ-algebra isomorphism v.adicCompletionIntegers ℚ ≃A[ℤ] ℤ_[natGenerator v].
PadicInt.adicCompletionIntegersEquiv p : the continuous ℤ-algebra isomorphism ℤ_[p] ≃A[ℤ] (primesEquiv.symm p).adicCompletionIntegers ℚ.

TODO : Abstract the isomorphisms in this file using a universal predicate on adic completions, along the lines of IsComplete + uniformity arises from a valuation + the valuations are equivalent. It is best to do this after Valued has been refactored, or at least after adicCompletion has IsValuativeTopology instance.

theorem instFactPrimeValNat (p : Nat.Primes) :

Fact (Nat.Prime ↑p)

theorem Rat.int_algebraMap_injective (R : Type u_1) [CommRing R] [Algebra R ℚ] :

Function.Injective ⇑(algebraMap ℤ R)

theorem Rat.int_algebraMap_surjective (R : Type u_1) [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsFractionRing R ℚ] :

Function.Surjective ⇑(algebraMap ℤ R)

noncomputable def Rat.IsIntegralClosure.intEquiv (R : Type u_1) [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] :

R ≃+* ℤ

If R has field of fractions ℚ and is the integral closure of ℤ in ℚ then it is isomorphic to ℤ.

Instances For

@[deprecated Rat.IsIntegralClosure.intEquiv (since := "2025-12-22")]

def Rat.intEquiv (R : Type u_1) [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] :

R ≃+* ℤ

Alias of Rat.IsIntegralClosure.intEquiv.

If R has field of fractions ℚ and is the integral closure of ℤ in ℚ then it is isomorphic to ℤ.

Instances For

@[simp]

theorem Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv (x : NumberField.RingOfIntegers ℚ) :

(intEquiv (NumberField.RingOfIntegers ℚ)) x = ringOfIntegersEquiv x

noncomputable def Rat.HeightOneSpectrum.natGenerator {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

ℕ

If v : HeightOneSpectrum R then natGenerator v is the generator in ℕ of the corresponding ideal in ℤ.

Instances For

theorem Rat.HeightOneSpectrum.span_natGenerator {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

Ideal.span {↑(natGenerator v)} = Ideal.map (IsIntegralClosure.intEquiv R) v.asIdeal

theorem Rat.HeightOneSpectrum.natGenerator_dvd_iff {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) {n : ℕ} :

natGenerator v ∣ n ↔ ↑n ∈ Ideal.map (IsIntegralClosure.intEquiv R) v.asIdeal

theorem Rat.HeightOneSpectrum.prime_natGenerator {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

Nat.Prime (natGenerator v)

noncomputable def Rat.HeightOneSpectrum.primesEquiv {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] :

IsDedekindDomain.HeightOneSpectrum R ≃ Nat.Primes

The equivalence between height-one prime ideals of R and primes in ℕ.

Instances For

theorem Rat.HeightOneSpectrum.valuation_equiv_padicValuation {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

(IsDedekindDomain.HeightOneSpectrum.valuation ℚ v).IsEquiv (padicValuation ↑(primesEquiv v))

noncomputable def Rat.HeightOneSpectrum.withValEquiv {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

WithVal (IsDedekindDomain.HeightOneSpectrum.valuation ℚ v) ≃ᵤ WithVal (padicValuation ↑(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.

Instances For

noncomputable def Rat.HeightOneSpectrum.adicCompletion.padicEquiv {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ v ≃A[ℚ] ℚ_[↑(primesEquiv v)]

The continuous ℚ-algebra isomorphism between v.adicCompletion ℚ and ℚ_[primesEquiv v].

Instances For

noncomputable def Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v) ≃A[ℤ] ℤ_[↑(primesEquiv v)]

The continuous ℤ-algebra isomorphism between v.adicCompletionIntegers ℚ and ℤ_[primesEquiv v].

Instances For

theorem Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v)) :

↑((padicIntEquiv v) x) = (adicCompletion.padicEquiv v) ↑x

The diagram

v.adicCompletionIntegers ℚ  ----->  ℤ_[primesEquiv v]
      |                               |
      |                               |
      v                               v
v.adicCompletion ℚ  ------------->  ℚ_[primesEquiv v]

commutes.

theorem Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) (x : ℤ_[↑(primesEquiv v)]) :

↑((padicIntEquiv v).symm x) = (adicCompletion.padicEquiv v).symm ↑x

The diagram

v.adicCompletionIntegers ℚ  <-----  ℤ_[primesEquiv v]
      |                               |
      |                               |
      v                               v
v.adicCompletion ℚ  <-------------  ℚ_[primesEquiv v]

commutes.

theorem Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn {R : Type u_2} [CommRing R] [Algebra R ℚ] [IsIntegralClosure R ℤ ℚ] [IsDedekindDomain R] [IsFractionRing R ℚ] (v : IsDedekindDomain.HeightOneSpectrum R) :

Set.BijOn ⇑(padicEquiv v) ↑(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ v) ↑(PadicInt.subring ↑(primesEquiv v))

noncomputable def Padic.adicCompletionEquiv (R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra R ℚ] [IsFractionRing R ℚ] [IsIntegralClosure R ℤ ℚ] (p : Nat.Primes) :

ℚ_[↑p] ≃A[ℚ] IsDedekindDomain.HeightOneSpectrum.adicCompletion ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p)

The continuous ℚ-algebra isomorphism between ℚ_[p] and (primesEquiv.symm p).adicCompletion ℚ.

Instances For

noncomputable def PadicInt.adicCompletionIntegersEquiv (R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra R ℚ] [IsFractionRing R ℚ] [IsIntegralClosure R ℤ ℚ] (p : Nat.Primes) :

ℤ_[↑p] ≃A[ℤ] ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p))

The continuous ℤ-algebra isomorphism between ℤ_[p] and (primesEquiv.symm p).adicCompletionIntegers ℚ.

Instances For

theorem PadicInt.coe_adicCompletionIntegersEquiv_apply (R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra R ℚ] [IsFractionRing R ℚ] [IsIntegralClosure R ℤ ℚ] (p : Nat.Primes) (x : ℤ_[↑p]) :

↑((adicCompletionIntegersEquiv R p) x) = (Padic.adicCompletionEquiv R p) ↑x

The diagram

ℤ_[p]  -------->  (primesEquiv.symm p).adicCompletionIntegers ℚ
   |                          |
   |                          |
   v                          v
ℚ_[p]  -------->  (primesEquiv.symm p).adicCompletion ℚ

commutes.

theorem PadicInt.coe_adicCompletionIntegersEquiv_symm_apply (R : Type u_2) [CommRing R] [IsDedekindDomain R] [Algebra R ℚ] [IsFractionRing R ℚ] [IsIntegralClosure R ℤ ℚ] (p : Nat.Primes) (x : ↥(IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers ℚ (Rat.HeightOneSpectrum.primesEquiv.symm p))) :

↑((adicCompletionIntegersEquiv R p).symm x) = (Padic.adicCompletionEquiv R p).symm ↑x

The diagram

ℤ_[p]  <--------  (primesEquiv.symm p).adicCompletionIntegers ℚ
   |                          |
   |                          |
   v                          v
ℚ_[p]  <--------  (primesEquiv.symm p).adicCompletion ℚ

commutes.