English
For r ∈ R and n ∈ N, the difference between lift f_compat applied to r and the nth component f n r, taken as an integer in the p-adic ring, lies in the span of p^n. More precisely, lift f_compat r − (f n r).val ∈ span{ p^n }.
Русский
Для элемента r ∈ R и натурального числа n разность между значением lift f_compat на r и компонентой f n на r, взятая в ℤ_[p], принадлежит идеалу, порождённому p^n.
LaTeX
$$$\\text{lift} \\, f_{\\text{compat}}(r) - (f n r).\\text{val} \\in \\operatorname{span}\\{ (p : \\mathbb{Z}_{p})^{n} \\}$$$
Lean4
theorem lift_sub_val_mem_span (r : R) (n : ℕ) : lift f_compat r - (f n r).val ∈ (Ideal.span {(p : ℤ_[p]) ^ n}) :=
by
obtain ⟨k, hk⟩ :=
limNthHom_spec f_compat r _ (show (0 : ℝ) < (p : ℝ) ^ (-n : ℤ) from zpow_pos (mod_cast hp_prime.1.pos) _)
have := le_of_lt (hk (max n k) (le_max_right _ _))
rw [norm_le_pow_iff_mem_span_pow] at this
dsimp [lift]
rw [sub_eq_sub_add_sub (limNthHom f_compat r) _ ↑(nthHom f r (max n k))]
apply Ideal.add_mem _ _ this
rw [Ideal.mem_span_singleton]
convert map_dvd (Int.castRingHom ℤ_[p]) (pow_dvd_nthHom_sub f_compat r n (max n k) (le_max_left _ _))
· simp
· simp [nthHom]
