English
Alternative formulation of uniqueness: if g satisfies (toZModPow n) ∘ g = f n for all n, then lift f_compat = g.
Русский
Альтернативная формулировка уникальности: если g удовлетворяет (toZModPow n) ∘ g = f n для всех n, то lift f_compat = g.
LaTeX
$$$\\forall g,\\ (\\forall n, (toZModPow n) \\circ g = f n) \\Rightarrow \\text{lift} \\ f_{\\text{compat}} = g$$$
Lean4
theorem toZModPow_ofIntSeq_of_pow_dvd_sub (f : ℕ → ℤ) (p : ℕ) [Fact p.Prime] (hi : ∀ i, (p : ℤ) ^ i ∣ f (i + 1) - f i)
(n : ℕ) : (PadicInt.ofIntSeq _ (isCauSeq_padicNorm_of_pow_dvd_sub f p hi)).toZModPow n = f n :=
by
set x := PadicInt.ofIntSeq _ (isCauSeq_padicNorm_of_pow_dvd_sub f p hi)
let s : PadicSeq p := ⟨(f ·), isCauSeq_padicNorm_of_pow_dvd_sub f p hi⟩
have hs : x = Padic.mk s := rfl
obtain ⟨e, he⟩ := Ideal.mem_span_singleton.mp (PadicInt.appr_spec n x)
rw [sub_eq_iff_eq_add] at he
obtain ⟨N, hN⟩ :=
padicNormE.defn s (ε := p ^ (-n : ℤ))
(by simp only [zpow_neg, zpow_natCast, inv_pos]; exact_mod_cast Nat.pos_of_neZero _)
replace hN := hN (N + n) (Nat.le_add_right N n)
rw [← hs, he, ← Rat.cast_lt (K := ℝ)] at hN
push_cast at hN
simp only [← add_sub, s, Rat.cast_intCast, padicNormE.is_norm, ← Int.cast_natCast (R := ℚ_[p]) (x.appr n),
← Int.cast_sub] at hN
have : ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ ≤ ↑p ^ (-n : ℤ) :=
by
by_contra! H
have H' : ‖(p ^ n * e : ℚ_[p])‖ < ‖(((x.appr n) - f (N + n) : ℤ) : ℚ_[p])‖ :=
by
refine LE.le.trans_lt ?_ H
simpa using mul_le_mul_of_nonneg le_rfl e.2 (show 0 ≤ (↑p ^ n)⁻¹ by simp) zero_le_one
rw [Padic.add_eq_max_of_ne H'.ne, sup_eq_right.mpr H'.le] at hN
exact lt_asymm hN H
rw [Padic.norm_int_le_pow_iff_dvd, ← Nat.cast_pow, ← ZMod.intCast_eq_intCast_iff_dvd_sub, Int.cast_natCast] at this
refine this.symm.trans ?_
clear * - hi
induction N with
| zero => simp
| succ N IH =>
rw [← IH, eq_comm, add_right_comm, ZMod.intCast_eq_intCast_iff_dvd_sub]
exact .trans ⟨p ^ N, by simp [pow_add, mul_comm]⟩ (hi _)
