Comparison isomorphism between WittVector p (ZMod p) and ℤ_[p]

We construct a ring isomorphism between WittVector 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

• WittVector.toZModPow: a family of compatible ring homs 𝕎 (ZMod p) → ZMod (p^k)
• WittVector.equiv: the isomorphism

References

• [Hazewinkel, Witt Vectors][Haze09]

• [Commelin and Lewis, Formalizing the Ring of Witt Vectors][CL21]

theorem TruncatedWittVector.eq_of_le_of_cast_pow_eq_zero (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) (R : Type u_1) [CommRing R] [CharP R p] (i : ℕ) (hin : i ≤ n) (hpi : ↑p ^ i = 0) : i = n

theorem TruncatedWittVector.card_zmod (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : Fintype.card (TruncatedWittVector p n (ZMod p)) = p ^ n

theorem TruncatedWittVector.charP_zmod (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : CharP (TruncatedWittVector p n (ZMod p)) (p ^ n)

def TruncatedWittVector.zmodEquivTrunc (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) : ZMod (p ^ n) ≃+* TruncatedWittVector p n (ZMod p)

The unique isomorphism between ZMod p^n and TruncatedWittVector p n (ZMod p).

This isomorphism exists, because TruncatedWittVector p n (ZMod p) is a finite ring with characteristic and cardinality p^n.

theorem TruncatedWittVector.zmodEquivTrunc_apply (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {x : ZMod (p ^ n)} : (zmodEquivTrunc p n) x = (ZMod.castHom ⋯ (TruncatedWittVector p n (ZMod p))) x

theorem TruncatedWittVector.commutes (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) : (truncate hm).comp (zmodEquivTrunc p m).toRingHom = (zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ n)))

The following diagram commutes:

          ZMod (p^n) ----------------------------> ZMod (p^m)
            |                                        |
            |                                        |
            v                                        v
TruncatedWittVector p n (ZMod p) ----> TruncatedWittVector p m (ZMod p)

Here the vertical arrows are TruncatedWittVector.zmodEquivTrunc, the horizontal arrow at the top is ZMod.castHom, and the horizontal arrow at the bottom is TruncatedWittVector.truncate.

theorem TruncatedWittVector.commutes' (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) (x : ZMod (p ^ m)) : (truncate hm) ((zmodEquivTrunc p m) x) = (zmodEquivTrunc p n) ((ZMod.castHom ⋯ (ZMod (p ^ n))) x)

theorem TruncatedWittVector.commutes_symm' (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) (x : TruncatedWittVector p m (ZMod p)) : (zmodEquivTrunc p n).symm ((truncate hm) x) = (ZMod.castHom ⋯ (ZMod (p ^ n))) ((zmodEquivTrunc p m).symm x)

theorem TruncatedWittVector.commutes_symm (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) : (zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) = (ZMod.castHom ⋯ (ZMod (p ^ n))).comp (zmodEquivTrunc p m).symm.toRingHom

The following diagram commutes:

TruncatedWittVector p n (ZMod p) ----> TruncatedWittVector p m (ZMod p)
            |                                        |
            |                                        |
            v                                        v
          ZMod (p^n) ----------------------------> ZMod (p^m)

Here the vertical arrows are (TruncatedWittVector.zmodEquivTrunc p _).symm, the horizontal arrow at the top is ZMod.castHom, and the horizontal arrow at the bottom is TruncatedWittVector.truncate.

def WittVector.toZModPow (p : ℕ) [hp : Fact (Nat.Prime p)] (k : ℕ) : WittVector p (ZMod p) →+* ZMod (p ^ k)

toZModPow is a family of compatible ring homs. We get this family by composing TruncatedWittVector.zmodEquivTrunc (in right-to-left direction) with WittVector.truncate.

theorem WittVector.toZModPow_compat (p : ℕ) [hp : Fact (Nat.Prime p)] (m n : ℕ) (h : m ≤ n) : (ZMod.castHom ⋯ (ZMod (p ^ m))).comp (toZModPow p n) = toZModPow p m

def WittVector.toPadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : WittVector p (ZMod p) →+* ℤ_[p]

toPadicInt lifts toZModPow : 𝕎 (ZMod p) →+* ZMod (p ^ k) to a ring hom to ℤ_[p] using PadicInt.lift, the universal property of ℤ_[p].

theorem WittVector.zmodEquivTrunc_compat (p : ℕ) [hp : Fact (Nat.Prime p)] (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂) : (TruncatedWittVector.truncate hk).comp ((TruncatedWittVector.zmodEquivTrunc p k₂).toRingHom.comp (PadicInt.toZModPow k₂)) = (TruncatedWittVector.zmodEquivTrunc p k₁).toRingHom.comp (PadicInt.toZModPow k₁)

def WittVector.fromPadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : ℤ_[p] →+* WittVector p (ZMod p)

fromPadicInt uses WittVector.lift to lift TruncatedWittVector.zmodEquivTrunc composed with PadicInt.toZModPow to a ring hom ℤ_[p] →+* 𝕎 (ZMod p).

theorem WittVector.toPadicInt_comp_fromPadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : (toPadicInt p).comp (fromPadicInt p) = RingHom.id ℤ_[p]

theorem WittVector.toPadicInt_comp_fromPadicInt_ext (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ℤ_[p]) : ((toPadicInt p).comp (fromPadicInt p)) x = (RingHom.id ℤ_[p]) x

theorem WittVector.fromPadicInt_comp_toPadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : (fromPadicInt p).comp (toPadicInt p) = RingHom.id (WittVector p (ZMod p))

theorem WittVector.fromPadicInt_comp_toPadicInt_ext (p : ℕ) [hp : Fact (Nat.Prime p)] (x : WittVector p (ZMod p)) : ((fromPadicInt p).comp (toPadicInt p)) x = (RingHom.id (WittVector p (ZMod p))) x

def WittVector.equiv (p : ℕ) [hp : Fact (Nat.Prime p)] : WittVector 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 WittVector.toPadicInt with inverse WittVector.fromPadicInt.