Comparison isomorphism between witt_vector p (zmod p)
and ℤ_[p]
#
We construct a ring isomorphism between witt_vector p (zmod p)
and ℤ_[p]
.
This isomorphism follows from the fact that both satisfy the universal property
of the inverse limit of zmod (p^n)
.
Main declarations #
witt_vector.to_zmod_pow
: a family of compatible ring homs𝕎 (zmod p) → zmod (p^k)
witt_vector.equiv
: the isomorphism
References #
The unique isomorphism between zmod p^n
and truncated_witt_vector p n (zmod p)
.
This isomorphism exists, because truncated_witt_vector p n (zmod p)
is a finite ring
with characteristic and cardinality p^n
.
Equations
- truncated_witt_vector.zmod_equiv_trunc p n = zmod.ring_equiv (truncated_witt_vector p n (zmod p)) _
The following diagram commutes:
zmod (p^n) ----------------------------> zmod (p^m)
| |
| |
v v
truncated_witt_vector p n (zmod p) ----> truncated_witt_vector p m (zmod p)
Here the vertical arrows are truncated_witt_vector.zmod_equiv_trunc
,
the horizontal arrow at the top is zmod.cast_hom
,
and the horizontal arrow at the bottom is truncated_witt_vector.truncate
.
The following diagram commutes:
truncated_witt_vector p n (zmod p) ----> truncated_witt_vector p m (zmod p)
| |
| |
v v
zmod (p^n) ----------------------------> zmod (p^m)
Here the vertical arrows are (truncated_witt_vector.zmod_equiv_trunc p _).symm
,
the horizontal arrow at the top is zmod.cast_hom
,
and the horizontal arrow at the bottom is truncated_witt_vector.truncate
.
to_zmod_pow
is a family of compatible ring homs. We get this family by composing
truncated_witt_vector.zmod_equiv_trunc
(in right-to-left direction)
with witt_vector.truncate
.
Equations
to_padic_int
lifts to_zmod_pow : 𝕎 (zmod p) →+* zmod (p ^ k)
to a ring hom to ℤ_[p]
using padic_int.lift
, the universal property of ℤ_[p]
.
Equations
from_padic_int
uses witt_vector.lift
to lift truncated_witt_vector.zmod_equiv_trunc
composed with padic_int.to_zmod_pow
to a ring hom ℤ_[p] →+* 𝕎 (zmod p)
.
Equations
- witt_vector.from_padic_int p = witt_vector.lift (λ (k : ℕ), (truncated_witt_vector.zmod_equiv_trunc p k).to_ring_hom.comp (padic_int.to_zmod_pow k)) _
The ring of Witt vectors over zmod p
is isomorphic to the ring of p
-adic integers. This
equivalence is witnessed by witt_vector.to_padic_int
with inverse witt_vector.from_padic_int
.
Equations
- witt_vector.equiv p = {to_fun := ⇑(witt_vector.to_padic_int p), inv_fun := ⇑(witt_vector.from_padic_int p), left_inv := _, right_inv := _, map_mul' := _, map_add' := _}