Theorems · Theorem · number theory

TruncatedWittVector.commutes

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

The following diagram commutes: ``text 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`.

Defined in

Mathlib.RingTheory.WittVector.Compare

Cited by

2 results in Mathlib

Foundations

Depth 148 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Fact