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.

Equations
Instances For
    theorem TruncatedWittVector.commutes (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {m : ℕ} (hm : n ≤ m) :

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

    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
    Instances For
      theorem WittVector.toZModPow_compat (p : ℕ) [hp : Fact (Nat.Prime p)] (m : ℕ) (n : ℕ) (h : m ≤ n) :

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

      Equations
      Instances For
        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₁)

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

        Equations
        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.

          Equations
          Instances For