PadicInverseLimit.lean

theorem exists_of_compatible_residues
    (a : ∀ n : ℕ, ZMod (p ^ n))
    (ha : ∀ n, ZMod.castHom (pow_dvd_pow p (Nat.le_succ n))
      (ZMod (p ^ n)) (a (n + 1)) = a n) :
    ∃ z : PadicInt p, ∀ n, toZModPow n z = a n

theorem continuous_toZModPow (n : ℕ) : Continuous (toZModPow n : PadicInt p → ZMod (p ^ n))

theorem continuous_of_continuous_toZModPow
    {X : Type u} [TopologicalSpace X] (f : X → PadicInt p)
    (hf : ∀ n, Continuous (fun x => toZModPow n (f x))) : Continuous f := by
  rw [continuous_iff_continuousAt]
  intro x
  rw [ContinuousAt, Metric.nhds_basis_closedBall.tendsto_right_iff]
  intro ε hε
  obtain ⟨n, hn⟩ := PadicInt.exists_pow_neg_lt p hε
  have hnb : {y | toZModPow n (f y) = toZModPow n (f x)} ∈ nhds x :=
    (isOpen_discrete ({toZModPow n (f x)} : Set (ZMod (p ^ n)))).preimage
      (hf n) |>.mem_nhds rfl
  apply Filter.mem_of_superset hnb
  intro y hy
  change f y ∈ Metric.closedBall (f x) ε
  rw [Metric.mem_closedBall, dist_eq_norm]
  apply le_trans _ hn.le
  rw [norm_le_pow_iff_mem_span_pow, ← ker_toZModPow n, RingHom.mem_ker, map_sub,
    sub_eq_zero]
  exact hy

theorem exists_continuous_of_compatible_residues
    {X : Type u} [TopologicalSpace X]
    (f : ∀ n : ℕ, X → ZMod (p ^ n))
    (hf : ∀ n, Continuous (f n))
    (hcompat : ∀ n x, ZMod.castHom (pow_dvd_pow p (Nat.le_succ n))
      (ZMod (p ^ n)) (f (n + 1) x) = f n x) :
    ∃ d : X → PadicInt p, Continuous d ∧ ∀ n x, toZModPow n (d x) = f n x