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 ℚ-algebraisomorphisms 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 ℤ.

Equations

• Rat.IsIntegralClosure.intEquiv R = (NumberField.RingOfIntegers.equiv R).symm.trans Rat.ringOfIntegersEquiv

@[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 ℤ.

Equations

• Rat.intEquiv = Rat.IsIntegralClosure.intEquiv

@[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 ℤ.

Equations

• Rat.HeightOneSpectrum.natGenerator v = (Submodule.IsPrincipal.generator (Ideal.map (Rat.IsIntegralClosure.intEquiv R) v.asIdeal)).natAbs

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

Equations

• One or more equations did not get rendered due to their size.

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.

Equations

• Rat.HeightOneSpectrum.withValEquiv v = Valuation.IsEquiv.uniformEquiv ⋯ ⋯ ⋯

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• Padic.adicCompletionEquiv R p = (ContinuousAlgEquiv.cast ⋯).trans (Rat.HeightOneSpectrum.adicCompletion.padicEquiv (Rat.HeightOneSpectrum.primesEquiv.symm p)).symm

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

Equations

• PadicInt.adicCompletionIntegersEquiv R p = (ContinuousAlgEquiv.cast ⋯).trans (Rat.HeightOneSpectrum.adicCompletionIntegers.padicIntEquiv (Rat.HeightOneSpectrum.primesEquiv.symm p)).symm

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.