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
theorem TruncatedWittVector.charP_zmod (p : ) [hp : Fact (Nat.Prime p)] (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 : ) :
    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
    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₂) :

        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