Completion of normed group homs #
Given two (semi) normed groups
H and a normed group hom
f : NormedAddGroupHom G H,
we build and study a normed group hom
f.completion : NormedAddGroupHom (completion G) (completion H) such that the diagram
f G -----------> H | | | | | | V V completion G -----------> completion H f.completion
commutes. The map itself comes from the general theory of completion of uniform spaces, but here we want a normed group hom, study its operator norm and kernel.
The vertical maps in the above diagrams are also normed group homs constructed in this file.
Main definitions and results: #
NormedAddGroupHom.completion: see the discussion above.
NormedAddCommGroup.toCompl : NormedAddGroupHom G (completion G): the canonical map from
Gto its completion, as a normed group hom
NormedAddGroupHom.completion_toCompl: the above diagram indeed commutes.
‖f.completion‖ = ‖f‖
NormedAddGroupHom.ker_le_ker_completion: the kernel of
f.completioncontains the image of the kernel of
NormedAddGroupHom.ker_completion: the kernel of
f.completionis the closure of the image of the kernel of
funder an assumption that
fis quantitatively surjective onto its image.
His complete, the extension of
f : NormedAddGroupHom G Hto a
NormedAddGroupHom (completion G) H.