English
Uniqueness in the universal property: if g: R → ℤ_[p] satisfies (toZModPow n) ∘ g = f n for all n, then lift f_compat = g.
Русский
Уникальность в универсальном свойстве: если g: R → ℤ_[p] удовлетворяет (toZModPow n) ∘ g = f n для всех n, то lift f_compat = g.
LaTeX
$$$\\forall g:\\, R \\to+* \\mathbb{Z}_{p},\\ (\\forall n, (toZModPow\\, n) \\circ g = f\\, n) \\Rightarrow \\text{lift} \\, f_{\\text{compat}} = g$$$
Lean4
/-- One part of the universal property of `ℤ_[p]` as a projective limit.
See also `PadicInt.lift_spec`.
-/
theorem lift_unique (g : R →+* ℤ_[p]) (hg : ∀ n, (toZModPow n).comp g = f n) : lift f_compat = g :=
by
ext1 r
apply eq_of_forall_dist_le
intro ε hε
obtain ⟨n, hn⟩ := exists_pow_neg_lt p hε
apply le_trans _ (le_of_lt hn)
rw [dist_eq_norm, norm_le_pow_iff_mem_span_pow, ← ker_toZModPow, RingHom.mem_ker, RingHom.map_sub, ←
RingHom.comp_apply, ← RingHom.comp_apply, lift_spec, hg, sub_self]
