# mathlibdocumentation

analysis.normed.group.hom_completion

# Completion of normed group homs #

Given two (semi) normed groups G and H and a normed group hom f : normed_group_hom G H, we build and study a normed group hom f.completion : normed_group_hom (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: #

• normed_group_hom.completion: see the discussion above.
• normed_group.to_compl : normed_group_hom G (completion G): the canonical map from G to its completion, as a normed group hom
• normed_group_hom.completion_to_compl: the above diagram indeed commutes.
• normed_group_hom.norm_completion: ∥f.completion∥ = ∥f∥
• normed_group_hom.ker_le_ker_completion: the kernel of f.completion contains the image of the kernel of f.
• normed_group_hom.ker_completion: the kernel of f.completion is the closure of the image of the kernel of f under an assumption that f is quantitatively surjective onto its image.
• normed_group_hom.extension : if H is complete, the extension of f : normed_group_hom G H to a normed_group_hom (completion G) H.
noncomputable def normed_group_hom.completion {G : Type u_1} {H : Type u_2} (f : H) :

The normed group hom induced between completions.

Equations
theorem normed_group_hom.completion_def {G : Type u_1} {H : Type u_2} (f : H) (x : uniform_space.completion G) :
@[simp]
theorem normed_group_hom.completion_coe_to_fun {G : Type u_1} {H : Type u_2} (f : H) :
@[simp]
theorem normed_group_hom.completion_coe {G : Type u_1} {H : Type u_2} (f : H) (g : G) :
noncomputable def normed_group_hom_completion_hom {G : Type u_1} {H : Type u_2}  :

Completion of normed group homs as a normed group hom.

Equations
@[simp]
theorem normed_group_hom_completion_hom_apply {G : Type u_1} {H : Type u_2} (f : H) :
@[simp]
theorem normed_group_hom.completion_id {G : Type u_1}  :
theorem normed_group_hom.completion_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} (f : H) (g : K) :
theorem normed_group_hom.completion_neg {G : Type u_1} {H : Type u_2} (f : H) :
theorem normed_group_hom.completion_add {G : Type u_1} {H : Type u_2} (f g : H) :
(f + g).completion =
theorem normed_group_hom.completion_sub {G : Type u_1} {H : Type u_2} (f g : H) :
(f - g).completion =
@[simp]
theorem normed_group_hom.zero_completion {G : Type u_1} {H : Type u_2}  :
def normed_group.to_compl {G : Type u_1}  :

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

Equations
theorem normed_group.norm_to_compl {G : Type u_1} (x : G) :
theorem normed_group.dense_range_to_compl {G : Type u_1}  :
@[simp]
theorem normed_group_hom.completion_to_compl {G : Type u_1} {H : Type u_2} (f : H) :
@[simp]
theorem normed_group_hom.norm_completion {G : Type u_1} {H : Type u_2} (f : H) :
theorem normed_group_hom.ker_le_ker_completion {G : Type u_1} {H : Type u_2} (f : H) :
theorem normed_group_hom.ker_completion {G : Type u_1} {H : Type u_2} {f : H} {C : } (h : C) :
noncomputable def normed_group_hom.extension {G : Type u_1} {H : Type u_2} (f : H) :

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

Equations
theorem normed_group_hom.extension_def {G : Type u_1} {H : Type u_2} (f : H) (v : G) :
@[simp]
theorem normed_group_hom.extension_coe {G : Type u_1} {H : Type u_2} (f : H) (v : G) :
theorem normed_group_hom.extension_coe_to_fun {G : Type u_1} {H : Type u_2} (f : H) :
theorem normed_group_hom.extension_unique {G : Type u_1} {H : Type u_2} (f : H) {g : H} (hg : ∀ (v : G), f v = g v) :