English
A polynomial map on Witt vectors commutes with Ring homomorphisms: applying the map before or after a ring homomorphism yields the same result.
Русский
Полиномиальное отображение на Witt-векторах сохраняет совместимость с отображениями колец: применение отображения до или после кольцевого гомоморфа даёт одинаковый результат.
LaTeX
$$$\forall \text{hf: IsPoly p f}, \forall g: R\to\to S, \forall x:\mathbb{W}_p(R):\; map\; g\ (f\ x) = f\ (map\ g\ x).$$$
Lean4
theorem map [Fact p.Prime] {f} (hf : IsPoly p f) (g : R →+* S) (x : 𝕎 R) : map g (f x) = f (map g x) := by
-- this could be turned into a tactic “macro” (taking `hf` as parameter)
-- so that applications do not have to worry about the universe issue
-- see `IsPoly₂.map` for a slightly more general proof strategy
obtain ⟨φ, hf⟩ := hf
ext n
simp_rw [map_coeff, hf, map_aeval, funext (map_coeff g _), RingHom.ext_int _ (algebraMap ℤ S), aeval_eq_eval₂Hom]
