English
The shifting map verschiebungFun moves Witt coordinates up by one: the 0th coefficient becomes 0, and the i-th coefficient becomes the previous coefficient x.coeff(i−1). This is the underlying function of the additive monoid hom verschiebung.
Русский
Перемещающее отображение verschiebungFun сдвигает коэффициенты Виттового вектора вверх на одну позицию: коэффициент нулевой позиции становится 0, а i-й коэффициент становится предыдущим коэффициентом x.coeff(i−1). Это смысловая функция односоставного гомоморфизма verschiebung.
LaTeX
$$$$ (\\\\text{verschiebungFun}(x))_n = \\begin{cases}0, & n=0 \\\\ x_{n-1}, & n>0\\end{cases} $$$$
Lean4
/-- `verschiebungFun x` shifts the coefficients of `x` up by one,
by inserting 0 as the 0th coefficient.
`x.coeff i` then becomes `(verschiebungFun x).coeff (i + 1)`.
`verschiebungFun` is the underlying function of the additive monoid hom `WittVector.verschiebung`.
-/
def verschiebungFun (x : 𝕎 R) : 𝕎 R :=
@mk' p _ fun n => if n = 0 then 0 else x.coeff (n - 1)
