English
There exists a bilinear form f on truncated Witt vectors that computes the (n+1)th coefficient of the product x*y after truncation. This provides a universal expression for the (n+1)th coefficient in terms of truncated inputs.
Русский
Существует билинейная форма f на усеченных Witt-векторах, вычисляющая (n+1)-й коэффициент произведения x*y после усечения. Это универсальное выражение для коэффициента n+1.
LaTeX
$$$\\exists f:\\operatorname{TruncatedWittVector}(p,n+1)\\to\\operatorname{TruncatedWittVector}(p,n+1)\\to k,\\ \\forall x,y:\\mathbb{W}^k,\\ f(\\operatorname{truncateFun}(n+1,x),\\operatorname{truncateFun}(n+1,y)) = (x*y)_{n+1} - y_{n+1} x_0^p^{n+1} - x_{n+1} y_0^p^{n+1}$$$
Lean4
theorem nth_mul_coeff' (n : ℕ) :
∃ f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k,
∀ x y : 𝕎 k,
f (truncateFun (n + 1) x) (truncateFun (n + 1) y) =
(x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) -
x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1) :=
by
simp only [← peval_polyOfInterest']
obtain ⟨f₀, hf₀⟩ := exists_restrict_to_vars k (polyOfInterest_vars p n)
have : ∀ (a : Multiset (Fin 2)) (b : Multiset ℕ), a ×ˢ b = a.product b := fun a b => rfl
let f : TruncatedWittVector p (n + 1) k → TruncatedWittVector p (n + 1) k → k :=
by
intro x y
apply f₀
rintro ⟨a, ha⟩
apply Function.uncurry ![x, y]
simp_rw [product_val, this, range_val, Multiset.range_succ] at ha
let S : Set (Fin 2 × ℕ) := (fun a => a.2 = n ∨ a.2 < n)
have ha' : a ∈ S := by
convert ha
dsimp [S]
congr!
simp
refine ⟨a.fst, ⟨a.snd, ?_⟩⟩
obtain ⟨ha, ha⟩ := ha' <;> omega
use f
intro x y
dsimp [f, peval]
rw [← hf₀]
congr
ext a
obtain ⟨a, ha⟩ := a
obtain ⟨i, m⟩ := a
fin_cases i <;>
rfl -- surely this case split is not necessary
