English
For a Witt vector a ≠ 0 in 𝕎 k, there exist m and b with b.coeff 0 ≠ 0 such that a = p^m · b.
Русский
Для не нуля вектора Витта a в 𝕎 k существуют m и b с b.coeff 0 ≠ 0 такие, что a = p^m · b.
LaTeX
$$$\exists m\, \exists b\,\text{ with } b.\text{coeff } 0 \neq 0 \text{ and } a = (p : 𝕎 k)^m \ast b$$$
Lean4
theorem exists_eq_pow_p_mul (a : 𝕎 k) (ha : a ≠ 0) : ∃ (m : ℕ) (b : 𝕎 k), b.coeff 0 ≠ 0 ∧ a = (p : 𝕎 k) ^ m * b :=
by
obtain ⟨m, c, hc, hcm⟩ := WittVector.verschiebung_nonzero ha
obtain ⟨b, rfl⟩ := (frobenius_bijective p k).surjective.iterate m c
rw [WittVector.iterate_frobenius_coeff] at hc
have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b
simp only [Function.comp_apply] at this
rw [← this] at hcm
refine ⟨m, b, ?_, ?_⟩
· contrapose! hc
simp [hc, zero_pow <| pow_ne_zero _ hp.out.ne_zero]
· simp_rw [← mul_left_iterate (p : 𝕎 k) m]
convert hcm using 2
ext1 x
rw [mul_comm, ← WittVector.verschiebung_frobenius x]; rfl
