English
Let p be a prime and n a natural number. In the Witt polynomial framework, a specific expansion for the product of p-adic coefficients yields an explicit combination of X-variables, renamed Witt polynomials, and a remainder term. This identity expresses how the p-adic structure of Witt vectors interacts with the polynomial representation of Witt multiplication.
Русский
Пусть p — простое число, а n — натуральное число. В рамках многочленов Witt приводится явное разложение произведения коэффициентов p-адической системы в виде комбинации переменных X, переименованных многочленов Witt и остатка. Эта тождесть описывает, как p-адическая структура Witt-векторов взаимодействует с полиномами Witt.
LaTeX
$$$(p^{n+1})\, wittMul_p(n+1) = -\bigl((p^{n+1})\, X(0,n+1)\bigr)\!\cdot\bigl((p^{n+1})\, X(1,n+1)\bigr) + (p^{n+1})\, X(0,n+1) \cdot rename(Prod.mk(1:Fin 2))(wittPolynomial p\;\mathbb{Z})(n+1) + (p^{n+1})\, X(1,n+1) \cdot rename(Prod.mk(0:Fin 2))(wittPolynomial p\;\mathbb{Z})(n+1) + (remainder\ p\ n - wittPolyProdRemainder p (n+1))$$$
Lean4
theorem mul_polyOfInterest_aux4 (n : ℕ) :
(p : 𝕄) ^ (n + 1) * wittMul p (n + 1) =
-((p : 𝕄) ^ (n + 1) * X (0, n + 1)) * ((p : 𝕄) ^ (n + 1) * X (1, n + 1)) +
(p : 𝕄) ^ (n + 1) * X (0, n + 1) * rename (Prod.mk (1 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
(p : 𝕄) ^ (n + 1) * X (1, n + 1) * rename (Prod.mk (0 : Fin 2)) (wittPolynomial p ℤ (n + 1)) +
(remainder p n - wittPolyProdRemainder p (n + 1)) :=
by
rw [← add_sub_assoc, eq_sub_iff_add_eq, mul_polyOfInterest_aux2]
exact mul_polyOfInterest_aux3 _ _
