withValRingEquiv — Mathlib

English

There is a RingEquiv between the completion of Rat.padicValuation p and the p-adic integers ℤ_p.

Русский

Существует кольцеподобное эквивалентное отображение между замкнутой степенью Rat.padicValuation p и p-адическими целыми ℤ_p.

LaTeX

$$\$\\text{Padic.withValRingEquiv} : (\\text{Rat.padicValuation}(p)).\\mathrm{Completion} \\simeq_+^* \\mathbb{Z}_p\$$$

Lean4

/-- The `p`-adic numbers are isomorphic as a field to the completion of the rationals at
the `p`-adic valuation. -/
noncomputable def withValRingEquiv : (Rat.padicValuation p).Completion ≃+* ℚ_[p]
    where
  toFun :=
    (extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)
      Padic.isUniformInducing_cast_withVal.uniformContinuous.continuous)
  invFun := Padic.isDenseInducing_cast_withVal.extend coe'
  left_inv
    y := by
    induction y using induction_on
    · generalize_proofs _ _ _ H
      refine isClosed_eq ?_ continuous_id
      exact
        (uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal (Padic.denseRange_ratCast p)
              (uniformContinuous_coe _)).continuous.comp
          (continuous_extension)
    · rw [extensionHom_coe]
      apply IsDenseInducing.extend_eq
      exact continuous_coe _
  right_inv
    y := by
    induction y using isClosed_property (Padic.denseRange_ratCast p)
    · refine isClosed_eq ?_ continuous_id
      refine continuous_extension.comp ?_
      exact
        (uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal (Padic.denseRange_ratCast p)
            (uniformContinuous_coe _)).continuous
    · have :
        ∀ q : ℚ,
          Padic.isDenseInducing_cast_withVal.extend coe' q = coe' ((WithVal.equiv (Rat.padicValuation p)).symm q) :=
        by
        intro q
        apply IsDenseInducing.extend_eq
        exact continuous_coe _
      rw [this, extensionHom_coe]
      simp
  map_mul' := map_mul _
  map_add' := map_add _

Похожие утверждения