English
Symmetric version of commutes' for truncated Witt vectors and ZMod cast
Русский
Симметричная версия commutes' для усечённых Witt-векторов и ZMod cast
LaTeX
$$$$ (zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) = (ZMod.castHom (pow_dvd_pow p hm) _).comp (zmodEquivTrunc p m).symm.toRingHom. $$$$
Lean4
/-- The following diagram commutes:
```text
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`.
-/
theorem commutes_symm {m : ℕ} (hm : n ≤ m) :
(zmodEquivTrunc p n).symm.toRingHom.comp (truncate hm) =
(ZMod.castHom (pow_dvd_pow p hm) _).comp (zmodEquivTrunc p m).symm.toRingHom :=
by ext; apply commutes_symm'
