mathlib3 documentation

Completion of normed group homs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

Given two (semi) normed groups G and H and a normed group hom f : normed_add_group_hom G H, we build and study a normed group hom f.completion : normed_add_group_hom (completion G) (completion H) such that the diagram

     G       ----------->     H

     |                        |
     |                        |
     |                        |
     V                        V

completion G -----------> completion H

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: #

The normed group hom induced between completions.


The map from a normed group to its completion, as a normed group hom.


If H is complete, the extension of f : normed_add_group_hom G H to a normed_add_group_hom (completion G) H.