English
Let α and β be rings with uniform structures such that subtraction is uniformly continuous, and let f: α →+* β be a continuous ring homomorphism. Then there exists a unique ring homomorphism from the completion of α to the completion of β extending f.
Русский
Пусть α и β являются кольцами, оснащёнными униформной структурой так, что вычитание является однородно равномерно непрерывным, и дан гомоморфизм колец f: α →+* β, непрерывный. Тогда существует единственный гомоморфизм колец φ: завершение(α) →+* завершение(β), который является продолжением f.
LaTeX
$$$$ \exists! \phi \in \mathrm{RingHom}(\widehat{\alpha}, \widehat{\beta}) \quad (\phi \circ i_{\alpha}) = (i_{\beta} \circ f). $$$$
Lean4
/-- The completion map as a ring morphism. -/
def mapRingHom (hf : Continuous f) : Completion α →+* Completion β :=
extensionHom (coeRingHom.comp f) (continuous_coeRingHom.comp hf)
