# mathlib3documentation

ring_theory.witt_vector.compare

# Comparison isomorphism between witt_vector p (zmod p) and ℤ_[p]#

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

theorem truncated_witt_vector.eq_of_le_of_cast_pow_eq_zero (p : ) [hp : fact (nat.prime p)] (n : ) (R : Type u_1) [comm_ring R] [ p] (i : ) (hin : i n) (hpi : p ^ i = 0) :
i = n
theorem truncated_witt_vector.card_zmod (p : ) [hp : fact (nat.prime p)] (n : ) :
fintype.card (zmod p)) = p ^ n
theorem truncated_witt_vector.char_p_zmod (p : ) [hp : fact (nat.prime p)] (n : ) :
char_p (zmod p)) (p ^ n)
noncomputable def truncated_witt_vector.zmod_equiv_trunc (p : ) [hp : fact (nat.prime p)] (n : ) :
zmod (p ^ n) ≃+* (zmod p)

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
theorem truncated_witt_vector.zmod_equiv_trunc_apply (p : ) [hp : fact (nat.prime p)] (n : ) {x : zmod (p ^ n)} :
= (zmod p))) x
theorem truncated_witt_vector.commutes (p : ) [hp : fact (nat.prime p)] (n : ) {m : } (hm : n m) :

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.

theorem truncated_witt_vector.commutes' (p : ) [hp : fact (nat.prime p)] (n : ) {m : } (hm : n m) (x : zmod (p ^ m)) :
= ( (zmod (p ^ n))) x)
theorem truncated_witt_vector.commutes_symm' (p : ) [hp : fact (nat.prime p)] (n : ) {m : } (hm : n m) (x : (zmod p)) :
= (zmod (p ^ n))) x)
theorem truncated_witt_vector.commutes_symm (p : ) [hp : fact (nat.prime p)] (n : ) {m : } (hm : n m) :

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.

noncomputable def witt_vector.to_zmod_pow (p : ) [hp : fact (nat.prime p)] (k : ) :
(zmod p) →+* zmod (p ^ k)

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
theorem witt_vector.to_zmod_pow_compat (p : ) [hp : fact (nat.prime p)] (m n : ) (h : m n) :
(zmod (p ^ m))).comp =
noncomputable def witt_vector.to_padic_int (p : ) [hp : fact (nat.prime p)] :

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
theorem witt_vector.zmod_equiv_trunc_compat (p : ) [hp : fact (nat.prime p)] (k₁ k₂ : ) (hk : k₁ k₂) :
noncomputable def witt_vector.from_padic_int (p : ) [hp : fact (nat.prime p)] :

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
noncomputable def witt_vector.equiv (p : ) [hp : fact (nat.prime p)] :

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