Documentation

Mathlib.RingTheory.WittVector.Compare

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 #

References #

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

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.

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

    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 (_ : p ^ n ∣ p ^ m) (ZMod (p ^ n))) x)

    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 : ℕ) :

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

    Instances For

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

      Instances For

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

        Instances For

          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.

          Instances For