English
For complete spaces β, the extension Hom agrees with f on the embedded α.
Русский
Для заполненных пространств β продолжение гомоморфизма совпадает с f на вложении α.
LaTeX
$$$\\mathrm{extensionHom\\;}(f, hf, a) = f(a)$$$
Lean4
/-- The completion extension as a ring morphism. -/
def extensionHom [CompleteSpace β] [T0Space β] : Completion α →+* β :=
have hf' : Continuous (f : α →+ β) := hf
have hf : UniformContinuous f := uniformContinuous_addMonoidHom_of_continuous hf'
{ toFun := Completion.extension f
map_zero' := by simp_rw [← coe_zero, extension_coe hf, f.map_zero]
map_add' := fun a b =>
Completion.induction_on₂ a b
(isClosed_eq (continuous_extension.comp continuous_add)
((continuous_extension.comp continuous_fst).add (continuous_extension.comp continuous_snd)))
fun a b => by simp_rw [← coe_add, extension_coe hf, f.map_add]
map_one' := by rw [← coe_one, extension_coe hf, f.map_one]
map_mul' := fun a b =>
Completion.induction_on₂ a b
(isClosed_eq (continuous_extension.comp continuous_mul)
((continuous_extension.comp continuous_fst).mul (continuous_extension.comp continuous_snd)))
fun a b => by simp_rw [← coe_mul, extension_coe hf, f.map_mul] }
