mathlib documentation

Completion of normed group homs #

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.

theorem normed_add_group_hom.completion_coe {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) (g : G) :

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.