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.

Equations

• TruncatedWittVector.zmodEquivTrunc p n = ZMod.ringEquiv (TruncatedWittVector p n (ZMod p)) ⋯

theorem TruncatedWittVector.zmodEquivTrunc_apply (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {x : ZMod (p ^ n)} : (TruncatedWittVector.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) : RingHom.comp (TruncatedWittVector.truncate hm) (RingEquiv.toRingHom (TruncatedWittVector.zmodEquivTrunc p m)) = RingHom.comp (RingEquiv.toRingHom (TruncatedWittVector.zmodEquivTrunc p n)) (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)) : (TruncatedWittVector.truncate hm) ((TruncatedWittVector.zmodEquivTrunc p m) x) = (TruncatedWittVector.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)) : (RingEquiv.symm (TruncatedWittVector.zmodEquivTrunc p n)) ((TruncatedWittVector.truncate hm) x) = (ZMod.castHom ⋯ (ZMod (p ^ n))) ((RingEquiv.symm (TruncatedWittVector.zmodEquivTrunc p m)) x)

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

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.

Equations

• WittVector.toZModPow p k = RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm (TruncatedWittVector.zmodEquivTrunc p k))) (WittVector.truncate k)

theorem WittVector.toZModPow_compat (p : ℕ) [hp : Fact (Nat.Prime p)] (m : ℕ) (n : ℕ) (h : m ≤ n) : RingHom.comp (ZMod.castHom ⋯ (ZMod (p ^ m))) (WittVector.toZModPow p n) = WittVector.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].

Equations

• WittVector.toPadicInt p = PadicInt.lift ⋯

theorem WittVector.zmodEquivTrunc_compat (p : ℕ) [hp : Fact (Nat.Prime p)] (k₁ : ℕ) (k₂ : ℕ) (hk : k₁ ≤ k₂) : RingHom.comp (TruncatedWittVector.truncate hk) (RingHom.comp (RingEquiv.toRingHom (TruncatedWittVector.zmodEquivTrunc p k₂)) (PadicInt.toZModPow k₂)) = RingHom.comp (RingEquiv.toRingHom (TruncatedWittVector.zmodEquivTrunc p k₁)) (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).

Equations

• WittVector.fromPadicInt p = WittVector.lift (fun (k : ℕ) => RingHom.comp (RingEquiv.toRingHom (TruncatedWittVector.zmodEquivTrunc p k)) (PadicInt.toZModPow k)) ⋯

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

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

theorem WittVector.fromPadicInt_comp_toPadicInt (p : ℕ) [hp : Fact (Nat.Prime p)] : RingHom.comp (WittVector.fromPadicInt p) (WittVector.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)) : (RingHom.comp (WittVector.fromPadicInt p) (WittVector.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.

Equations

• WittVector.equiv p = { toEquiv := { toFun := ⇑(WittVector.toPadicInt p), invFun := ⇑(WittVector.fromPadicInt p), left_inv := ⋯, right_inv := ⋯ }, map_mul' := ⋯, map_add' := ⋯ }