English
If a linear map f is surjective, then the induced map on adic completions map I f is also surjective.
Русский
Если f сюрьективен, то и отображение map I f на адическом завершении сюрьективно.
LaTeX
$$$\text{Surjective}(f) \Rightarrow \text{Surjective}(\mathrm{map}\ I\ f)$$$
Lean4
/-- Adic completion preserves surjectivity -/
theorem map_surjective (hf : Function.Surjective f) : Function.Surjective (map I f) := fun y ↦
by
apply AdicCompletion.induction_on I N y (fun b ↦ ?_)
let a := mapPreimage hf b
refine ⟨AdicCompletion.mk I M (AdicCauchySequence.mk I M (fun n ↦ (a n : M)) ?_), ?_⟩
· refine fun n ↦ SModEq.symm ?_
simp only [SModEq, mapPreimage, Submodule.Quotient.mk_sub, sub_eq_self, Submodule.Quotient.mk_eq_zero,
SetLike.coe_mem, a]
· exact _root_.AdicCompletion.ext fun n ↦ congrArg _ ((a n).property)
