mathlib3 documentation

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 #

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] [char_p R p] (i : ) (hin : i n) (hpi : p ^ i = 0) :
i = n
theorem truncated_witt_vector.char_p_zmod (p : ) [hp : fact (nat.prime p)] (n : ) :
noncomputable def truncated_witt_vector.zmod_equiv_trunc (p : ) [hp : fact (nat.prime p)] (n : ) :

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

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.

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