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 #

source
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
source
theorem truncated_witt_vector.card_zmod (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :
fintype.card (truncated_witt_vector p n (zmod p)) = p ^ n
source
theorem truncated_witt_vector.char_p_zmod (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :
char_p (truncated_witt_vector p n (zmod p)) (p ^ n)
source
noncomputable def truncated_witt_vector.zmod_equiv_trunc (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) :
zmod (p ^ n) ≃+* truncated_witt_vector 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
source
theorem truncated_witt_vector.zmod_equiv_trunc_apply (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) {x : zmod (p ^ n)} :
⇑(truncated_witt_vector.zmod_equiv_trunc p n) x = ⇑(zmod.cast_hom _ (truncated_witt_vector p n (zmod p))) x
source
theorem truncated_witt_vector.commutes (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) :
(truncated_witt_vector.truncate hm).comp (truncated_witt_vector.zmod_equiv_trunc p m).to_ring_hom = (truncated_witt_vector.zmod_equiv_trunc p n).to_ring_hom.comp (zmod.cast_hom _ (zmod (p ^ n)))

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.

source
theorem truncated_witt_vector.commutes' (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) (x : zmod (p ^ m)) :
⇑(truncated_witt_vector.truncate hm) (⇑(truncated_witt_vector.zmod_equiv_trunc p m) x) = ⇑(truncated_witt_vector.zmod_equiv_trunc p n) (⇑(zmod.cast_hom _ (zmod (p ^ n))) x)
source
theorem truncated_witt_vector.commutes_symm' (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) (x : truncated_witt_vector p m (zmod p)) :
⇑((truncated_witt_vector.zmod_equiv_trunc p n).symm) (⇑(truncated_witt_vector.truncate hm) x) = ⇑(zmod.cast_hom _ (zmod (p ^ n))) (⇑((truncated_witt_vector.zmod_equiv_trunc p m).symm) x)
source
theorem truncated_witt_vector.commutes_symm (p : ℕ) [hp : fact (nat.prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) :
(truncated_witt_vector.zmod_equiv_trunc p n).symm.to_ring_hom.comp (truncated_witt_vector.truncate hm) = (zmod.cast_hom _ (zmod (p ^ n))).comp (truncated_witt_vector.zmod_equiv_trunc p m).symm.to_ring_hom

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.

source
noncomputable def witt_vector.to_zmod_pow (p : ℕ) [hp : fact (nat.prime p)] (k : ℕ) :
witt_vector p (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
source
theorem witt_vector.to_zmod_pow_compat (p : ℕ) [hp : fact (nat.prime p)] (m n : ℕ) (h : m ≤ n) :
(zmod.cast_hom _ (zmod (p ^ m))).comp (witt_vector.to_zmod_pow p n) = witt_vector.to_zmod_pow p m
source
noncomputable def witt_vector.to_padic_int (p : ℕ) [hp : fact (nat.prime p)] :
witt_vector p (zmod p) →+* ℤ_[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
source
theorem witt_vector.zmod_equiv_trunc_compat (p : ℕ) [hp : fact (nat.prime p)] (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂) :
(truncated_witt_vector.truncate hk).comp ((truncated_witt_vector.zmod_equiv_trunc p k₂).to_ring_hom.comp (padic_int.to_zmod_pow k₂)) = (truncated_witt_vector.zmod_equiv_trunc p k₁).to_ring_hom.comp (padic_int.to_zmod_pow k₁)
source
noncomputable def witt_vector.from_padic_int (p : ℕ) [hp : fact (nat.prime p)] :
ℤ_[p] →+* witt_vector p (zmod 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
source
theorem witt_vector.to_padic_int_comp_from_padic_int (p : ℕ) [hp : fact (nat.prime p)] :
(witt_vector.to_padic_int p).comp (witt_vector.from_padic_int p) = ring_hom.id ℤ_[p]
source
theorem witt_vector.to_padic_int_comp_from_padic_int_ext (p : ℕ) [hp : fact (nat.prime p)] (x : ℤ_[p]) :
⇑((witt_vector.to_padic_int p).comp (witt_vector.from_padic_int p)) x = ⇑(ring_hom.id ℤ_[p]) x
source
theorem witt_vector.from_padic_int_comp_to_padic_int (p : ℕ) [hp : fact (nat.prime p)] :
(witt_vector.from_padic_int p).comp (witt_vector.to_padic_int p) = ring_hom.id (witt_vector p (zmod p))
source
theorem witt_vector.from_padic_int_comp_to_padic_int_ext (p : ℕ) [hp : fact (nat.prime p)] (x : witt_vector p (zmod p)) :
⇑((witt_vector.from_padic_int p).comp (witt_vector.to_padic_int p)) x = ⇑(ring_hom.id (witt_vector p (zmod p))) x
source
noncomputable def witt_vector.equiv (p : ℕ) [hp : fact (nat.prime p)] :
witt_vector p (zmod p) ≃+* ℤ_[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