English
For x in PreTilt(O, p) and m ≤ n, the p^m-th power divides the difference between x.untiltAux m and x.untiltAux n.
Русский
Для x в PreTilt(O, p) и m ≤ n, p^m делит разность x.untiltAux m и x.untiltAux n.
LaTeX
$$$(p : O)^{m} \mid x.untiltAux m - x.untiltAux n$ for m ≤ n$$
Lean4
theorem pow_dvd_untiltAux_sub_untiltAux (x : PreTilt O p) {m n : ℕ} (h : m ≤ n) :
(p : O) ^ m ∣ x.untiltAux m - x.untiltAux n := by
cases m with
| zero => simp [untiltAux]
| succ m =>
let n' := n.pred
have : n = n' + 1 := by simp [n', Nat.sub_add_cancel (n := n) (m := 1) (by linarith)]
simp only [this, add_le_add_iff_right, untiltAux] at h ⊢
rw [← Nat.sub_add_cancel h, pow_add _ _ m, pow_mul]
refine (dvd_sub_pow_of_dvd_sub ?_ m)
rw [← mem_span_singleton, ← Ideal.Quotient.eq]
simp only [Ideal.Quotient.mk_out, map_pow, Nat.sub_add_cancel h]
calc
_ = (coeff (ModP O p) p (n' - (n' - m))) x := by simp [Nat.sub_sub_self h]
_ = (coeff (ModP O p) p n') (((frobenius (Ring.Perfection (ModP O p) p) p))^[n' - m] x) :=
(coeff_iterate_frobenius' x n' (n' - m) (Nat.sub_le n' m)).symm
_ = _ := by simp [iterate_frobenius]
