fromPadicInt — Mathlib

English

The Witt vector ring over ZMod p is isomorphic to the p-adic integers; the equivalence is given by toPadicInt with inverse fromPadicInt.

Русский

Кольцо Witt над ZMod p изоморфно p-адическим целым; эквивалентность задаётся через toPadicInt с обратным fromPadicInt.

LaTeX

$$$$ \mathbb{W}_p(\mathbb{Z}/p\mathbb{Z}) \cong^+_* \mathbb{Z}_{(p)}. $$$$

Lean4

/-- `fromPadicInt` uses `WittVector.lift` to lift `TruncatedWittVector.zmodEquivTrunc`
composed with `PadicInt.toZModPow` to a ring hom `ℤ_[p] →+* 𝕎 (ZMod p)`.
-/
def fromPadicInt : ℤ_[p] →+* 𝕎 (ZMod p) :=
  (WittVector.lift fun k => (zmodEquivTrunc p k).toRingHom.comp (PadicInt.toZModPow k)) <| zmodEquivTrunc_compat _

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