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

@[simp]

theorem Padic.withValUniformEquiv_cast_apply {p : ℕ} [Fact (Nat.Prime p)] (x : WithVal (Rat.padicValuation p)) : withValUniformEquiv ↑x = ↑((WithVal.equiv (Rat.padicValuation p)) x)

theorem Padic.norm_rat_le_one_iff_padicValuation_le_one (p : ℕ) [Fact (Nat.Prime p)] {x : ℚ} : ‖↑x‖ ≤ 1 ↔ (Rat.padicValuation p) x ≤ 1

theorem Padic.withValUniformEquiv_norm_le_one_iff {p : ℕ} [Fact (Nat.Prime p)] (x : (Rat.padicValuation p).Completion) : ‖withValUniformEquiv x‖ ≤ 1 ↔ Valued.v x ≤ 1

noncomputable def PadicInt.withValIntegersRingEquiv {p : ℕ} [Fact (Nat.Prime p)] : ↥(Valued.integer (Rat.padicValuation p).Completion) ≃+* ℤ_[p]

The p-adic integers are ring isomorphic to the integers of the uniform completion of the rationals at the p-adic valuation.

Equations

• PadicInt.withValIntegersRingEquiv = Padic.withValRingEquiv.restrict (Valued.integer (Rat.padicValuation p).Completion) (PadicInt.subring p) ⋯

noncomputable def PadicInt.withValIntegersUniformEquiv {p : ℕ} [Fact (Nat.Prime p)] : ↥(Valued.integer (Rat.padicValuation p).Completion) ≃ᵤ ℤ_[p]

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

Equations

• PadicInt.withValIntegersUniformEquiv = Padic.withValUniformEquiv.subtype ⋯