English
Let p be a prime. The map that sends every Witt vector to the constant Witt vector of value 1 is a polynomial function in the Witt coordinates.
Русский
Пусть p — простое число. отображение, которое каждому вектору Witt сопоставляет константный вектор Witt, все координаты которого равны 1, задаётся полиномиальной функцией по координатам Witt.
LaTeX
$$$\exists\text{ a family of polynomials } (f_i)_{i\ge 0} \subset \mathbb{Z}[X_j]\text{ such that }(f_0(w), f_1(w), f_2(w), \dots)=(1,1,1,\dots) \text{ for every Witt vector } w \text{ over any commutative ring } R.$$$
Lean4
/-- The function that is constantly one on Witt vectors is a polynomial function. -/
instance oneIsPoly [Fact p.Prime] : IsPoly p fun _ _ _ => 1 :=
⟨⟨onePoly, by
intros; funext n; cases n
· simp only [one_coeff_zero, onePoly, ite_true, map_one]
· simp only [Nat.succ_pos', one_coeff_eq_of_pos, onePoly, Nat.succ_ne_zero, ite_false, map_zero]⟩⟩
