English
Let p be prime and R a commutative ring. For any Witt vector x ∈ W_p(R) and any natural k, if the first k+1 coefficients of x vanish (i.e., x.coeff i = 0 for all i < k+1), then applying Verschiebung to the (k+1)-shift of x gives the same Witt vector as shifting x by k.
Русский
Пусть p — простое число, R — коммутативное кольцо. Для любого Witt-вектора x ∈ W_p(R) и любого натурального k, если первые k+1 коэффициентов x равны нулю (то есть x.coeff i = 0 при всех i < k+1), то Verschiebung применённый к x.shift(k+1) равен x.shift(k).
LaTeX
$$$\forall x \in \mathbb{W}_p(R), \; \forall k \in \mathbb{N}, \; (\forall i < k+1,\; x_i = 0) \Rightarrow \ operatorname{verschiebung}(x.shift(k+1)) = x.shift(k).$$$
Lean4
theorem verschiebung_shift (x : 𝕎 R) (k : ℕ) (h : ∀ i < k + 1, x.coeff i = 0) :
verschiebung (x.shift k.succ) = x.shift k := by
ext ⟨j⟩
· rw [verschiebung_coeff_zero, shift_coeff, h]
apply Nat.lt_succ_self
· simp only [verschiebung_coeff_succ, shift]
congr 1
rw [Nat.add_succ, add_comm, Nat.add_succ, add_comm]
