English
Let x be a Witt vector over k. Then x lies in the principal ideal generated by p if and only if its zeroth coefficient is zero.
Русский
Пусть x — Witt‑вектор над k. Тогда x принадлежит порождающему идеалу p тогда и только тогда, когда его нулевой коэффициент равен нулю.
LaTeX
$$$x \\in \\operatorname{Ideal.span}\\{p\\} \\iff x_{0} = 0$$$
Lean4
/-- If `k` is a perfect ring of characteristic `p`, a Witt vector `x : 𝕎 k` falls in ideal generated by
`p` if and only if its zeroth coefficient is `0`.
-/
theorem mem_span_p_iff_coeff_zero_eq_zero (x : 𝕎 k) : x ∈ (Ideal.span {(p : 𝕎 k)}) ↔ x.coeff 0 = 0 :=
by
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]
refine ⟨fun ⟨u, hu⟩ ↦ ?_, fun h ↦ ?_⟩
· rw [hu, mul_charP_coeff_zero]
· use (frobeniusEquiv p k).symm (x.shift 1)
calc
_ = verschiebung (x.shift 1) := by simpa using eq_iterate_verschiebung (n := 1) (by simp [h])
_ = _ := by
rw [← verschiebung_frobenius, ← frobeniusEquiv_apply, RingEquiv.apply_symm_apply (frobeniusEquiv p k) _]
