Completion of topological groups: #
This files endows the completion of a topological abelian group with a group structure.
More precisely the instance
UniformSpace.Completion.addGroup builds an abelian group structure
on the completion of an abelian group endowed with a compatible uniform structure.
Then the instance
UniformSpace.Completion.uniformAddGroup proves this group structure is
compatible with the completed uniform structure. The compatibility condition is
Main declarations: #
Beyond the instances explained above (that don't have to be explicitly invoked), the main constructions deal with continuous group morphisms.
Extension to the completion of a continuous group hom.
Completion of a continuous group hom, as a group hom.