English
A polynomial two-argument operation on Witt vectors remains polynomial after applying a ring homomorphism to both arguments.
Русский
Полиномиальная операция из двух аргументов над Witt-векторами сохраняется после применения кольцевого гомоморфа к обоим аргументам.
LaTeX
$$$\forall f\; (IsPoly₂ p f)\; \forall g:\text{RingHom } R\, S,\; \forall x,y:\mathbb{W}_p(R):\; map\ g\ (f\ x\ y) = f\ (map\ g\ x) (map\ g\ y).$$$
Lean4
theorem map [Fact p.Prime] {f} (hf : IsPoly₂ p f) (g : R →+* S) (x y : 𝕎 R) : map g (f x y) = f (map g x) (map g y) :=
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
obtain ⟨φ, hf⟩ := hf
ext n
simp +unfoldPartialApp only [map_coeff, hf, map_aeval, peval, uncurry]
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
ext ⟨i, k⟩
fin_cases i <;> simp
