English
Every element of the I-adic completion of M is represented by a Cauchy sequence; i.e., the canonical map mk from the Cauchy sequences to the adic completion is surjective.
Русский
Каждый элемент I-адического завершения пространства M изображается последовательностью Коши; тождество mk: AdicCauchySequence I M → AdicCompletion I M является сюрьективным.
LaTeX
$$$\forall x:\\mathrm{AdicCompletion}(I,M),\ \exists f:\mathrm{AdicCauchySequence}(I,M),\mk I M f = x$$$
Lean4
/-- Every element in the adic completion is represented by a Cauchy sequence. -/
theorem mk_surjective : Function.Surjective (mk I M) := by
intro x
choose a ha using fun n ↦ Submodule.Quotient.mk_surjective _ (x.val n)
refine ⟨⟨a, ?_⟩, ?_⟩
· intro m n hmn
rw [SModEq.def, ha m, ← mkQ_apply, ← factor_mk (Submodule.smul_mono_left (Ideal.pow_le_pow_right hmn)) (a n),
mkQ_apply, ha n, x.property hmn]
· ext n
simp [ha n]
