English
One part of the universal property of ℤ_[p] as a projective limit: for every n, the composition (toZModPow n) ∘ (lift f_compat) equals f n.
Русский
Одна часть универсального свойства ℤ_[p] как проективного предела: для каждого n композиция (toZModPow n) ∘ (lift f_compat) равна f n.
LaTeX
$$$ (toZModPow\\, n) \\circ (lift\\, f_{\\text{compat}}) = f\\,n $$$
Lean4
/-- One part of the universal property of `ℤ_[p]` as a projective limit.
See also `PadicInt.lift_unique`.
-/
theorem lift_spec (n : ℕ) : (toZModPow n).comp (lift f_compat) = f n :=
by
ext r
rw [RingHom.comp_apply, ← ZMod.natCast_zmod_val (f n r), ← map_natCast <| toZModPow n, ← sub_eq_zero, ←
RingHom.map_sub, ← RingHom.mem_ker, ker_toZModPow]
apply lift_sub_val_mem_span
