English
Let x be a Witt vector over k. Then x lies in the ideal generated by p^n if and only if its first n coefficients vanish: x_m = 0 for all m < n.
Русский
Пусть x — Witt‑вектор над k. Тогда x принадлежит IDE p^n тогда и только тогда, когда первые n коэффициентов равны нулю: x_m = 0 для всех m < n.
LaTeX
$$$x \\in \\operatorname{Ideal.span}\\{p^{n}\\} \\iff \\forall m < n,\\ x_{m} = 0$$$
Lean4
/-- If `k` is a perfect ring of characteristic `p`, a Witt vector `x : 𝕎 k` falls in ideal generated by
`p ^ n` if and only if its initial `n` coefficients are `0`.
-/
theorem mem_span_p_pow_iff_le_coeff_eq_zero (x : 𝕎 k) (n : ℕ) :
x ∈ (Ideal.span {(p ^ n : 𝕎 k)}) ↔ ∀ m, m < n → x.coeff m = 0 :=
by
simp_rw [Ideal.mem_span_singleton, dvd_def, mul_comm]
refine ⟨fun ⟨u, hu⟩ m hm ↦ ?_, fun h ↦ ?_⟩
· rw [hu, mul_pow_charP_coeff_zero _ hm]
· use (frobeniusEquiv p k).symm^[n] (x.shift n)
rw [← iterate_verschiebung_iterate_frobenius]
calc
_ = verschiebung^[n] (x.shift n) := by simpa using eq_iterate_verschiebung (x := x) (n := n) h
_ = _ := by
congr
rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
· rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
simp
· rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]
