Equivalence between ℚ_[p] and (Rat.padicValuation p).Completion

The p-adic numbers are isomorphic as a field to the completion of the rationals at the p-adic valuation. This is implemented via Valuation.Completion using Rat.padicValuation, which is shorthand for UniformSpace.Completion (WithVal (Rat.padicValuation p)).

Main definitions

• Padic.withValRingEquiv: the field isomorphism between (Rat.padicValuation p).Completion and ℚ_[p]
• Padic.withValUniformEquiv: the uniform space isomorphism between (Rat.padicValuation p).Completion and ℚ_[p]

theorem Padic.isUniformInducing_cast_withVal {p : ℕ} [Fact (Nat.Prime p)] : IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

theorem Padic.isDenseInducing_cast_withVal {p : ℕ} [Fact (Nat.Prime p)] : IsDenseInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

noncomputable def Padic.withValRingEquiv {p : ℕ} [Fact (Nat.Prime p)] : (Rat.padicValuation p).Completion ≃+* ℚ_[p]

The p-adic numbers are isomorphic as a field to the completion of the rationals at the p-adic valuation.

Equations

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

@[simp]

theorem Padic.coe_withValRingEquiv {p : ℕ} [Fact (Nat.Prime p)] : ⇑withValRingEquiv = UniformSpace.Completion.extension (Rat.cast ∘ ⇑(WithVal.equiv (Rat.padicValuation p)))

@[simp]

theorem Padic.coe_withValRingEquiv_symm {p : ℕ} [Fact (Nat.Prime p)] : ⇑withValRingEquiv.symm = ⋯.extend UniformSpace.Completion.coe'

noncomputable def Padic.withValUniformEquiv {p : ℕ} [Fact (Nat.Prime p)] : (Rat.padicValuation p).Completion ≃ᵤ ℚ_[p]

The p-adic numbers are isomophic as uniform spaces to the completion of the rationals at the p-adic valuation.

Equations

• Padic.withValUniformEquiv = (Padic.withValRingEquiv.symm.toUniformEquivOfIsUniformInducing ⋯).symm

@[simp]

theorem Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv {p : ℕ} [Fact (Nat.Prime p)] : ↑withValUniformEquiv = ↑withValRingEquiv