English
The effect of applying bind₁ with verschiebungPoly to a WittPolynomial: it yields 0 when n=0, otherwise p times the WittPolynomial at n−1.
Русский
Применение bind₁ к verschiebungPoly и WittPolynomial даёт 0 при n=0, иначе p умножает на WittPolynomial(p, ℤ, n−1).
LaTeX
$$$$ \\operatorname{bind}_1(\\\\text{verschiebungPoly})(wittPolynomial(p,\\mathbb{Z},n)) = \\begin{cases}0, & n=0 \\\\ p \\cdot wittPolynomial(p,\\mathbb{Z},n-1), & n>0.\\end{cases} $$$$
Lean4
@[simp]
theorem bind₁_verschiebungPoly_wittPolynomial (n : ℕ) :
bind₁ verschiebungPoly (wittPolynomial p ℤ n) = if n = 0 then 0 else p * wittPolynomial p ℤ (n - 1) :=
by
apply MvPolynomial.funext
intro x
split_ifs with hn
· simp only [hn, wittPolynomial_zero, bind₁_X_right, verschiebungPoly_zero, map_zero]
· obtain ⟨n, rfl⟩ := Nat.exists_eq_succ_of_ne_zero hn
rw [Nat.succ_eq_add_one, add_tsub_cancel_right]
simp only [map_mul]
rw [map_natCast, hom_bind₁]
calc
_ = ghostComponent (n + 1) (verschiebung <| mk p x) :=
by
apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
funext k
simp only [← aeval_verschiebungPoly]
exact eval₂Hom_congr (RingHom.ext_int _ _) rfl rfl
_ = _ := by rw [ghostComponent_verschiebung]; rfl
