English
For n ≤ m, the following diagram commutes: truncation, zmodEquivTrunc, and ZMod.castHom connect ZMod(p^n) and ZMod(p^m) with TruncatedWittVector p n (ZMod p) and p m.
Русский
Пусть n ≤ m: диаграмма между ZMod(p^n), ZMod(p^m) и TruncatedWittVector p n, p m с учетом zmodEquivTrunc, truncation и castHom коммутирует.
LaTeX
$$$$ (\text{truncate}(hm)).toRingHom \circ (zmodEquivTrunc\ p\ m).toRingHom = (zmodEquivTrunc\ p\ n).toRingHom \circ (ZMod.castHom (pow\_dvd\_pow\ p\ hm) \_). $$$$
Lean4
/-- 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`.
-/
theorem commutes {m : ℕ} (hm : n ≤ m) :
(truncate hm).comp (zmodEquivTrunc p m).toRingHom =
(zmodEquivTrunc p n).toRingHom.comp (ZMod.castHom (pow_dvd_pow p hm) _) :=
RingHom.ext_zmod _ _
