English
There exists a unique extension of a continuous group hom f: α →+ β to a homomorphism on the completion, i.e., an extension hat f: Completion α →+ Completion β with hat f ∘ toCompl = f.
Русский
Существует единственное расширение непрерывного гомоморфизма группы f: α →+ β на дополнение, то есть hat f: Completion α →+ Completion β такое, что hat f ∘ toCompl = f.
LaTeX
$$$\\exists!\\hat f : \\mathrm{Completion}(\\alpha) \\to+ \\mathrm{Completion}(\\beta),\\ \\hat f \\circ \\mathrm{toCompl} = f$$$
Lean4
/-- Extension to the completion of a continuous group hom. -/
def extension [CompleteSpace β] [T0Space β] (f : α →+ β) (hf : Continuous f) : Completion α →+ β :=
have hf : UniformContinuous f := uniformContinuous_addMonoidHom_of_continuous hf
{ toFun := Completion.extension f
map_zero' := by 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 ↦
show Completion.extension f _ = Completion.extension f _ + Completion.extension f _ by
rw_mod_cast [extension_coe hf, extension_coe hf, extension_coe hf, f.map_add] }
