# Completion of normed group homs #

Given two (semi) normed groups G and 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 G to its completion, as a normed group hom
• NormedAddGroupHom.completion_toCompl: the above diagram indeed commutes.
• NormedAddGroupHom.norm_completion: ‖f.completion‖ = ‖f‖
• NormedAddGroupHom.ker_le_ker_completion: the kernel of f.completion contains the image of the kernel of f.
• NormedAddGroupHom.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.
• NormedAddGroupHom.extension : if H is complete, the extension of f : NormedAddGroupHom G H to a NormedAddGroupHom (completion G) H.
def NormedAddGroupHom.completion {G : Type u_1} {H : Type u_2} (f : ) :

The normed group hom induced between completions.

Equations
Instances For
theorem NormedAddGroupHom.completion_def {G : Type u_1} {H : Type u_2} (f : ) (x : ) :
f.completion x =
@[simp]
theorem NormedAddGroupHom.completion_coe_to_fun {G : Type u_1} {H : Type u_2} (f : ) :
f.completion =
theorem NormedAddGroupHom.completion_coe {G : Type u_1} {H : Type u_2} (f : ) (g : G) :
f.completion (G g) = H (f g)
@[simp]
theorem NormedAddGroupHom.completion_coe' {G : Type u_1} {H : Type u_2} (f : ) (g : G) :
UniformSpace.Completion.map (f) (G g) = H (f g)
@[simp]
theorem normedAddGroupHomCompletionHom_apply {G : Type u_1} {H : Type u_2} (f : ) :
def normedAddGroupHomCompletionHom {G : Type u_1} {H : Type u_2} :

Completion of normed group homs as a normed group hom.

Equations
Instances For
@[simp]
theorem NormedAddGroupHom.completion_id {G : Type u_1} :
.completion =
theorem NormedAddGroupHom.completion_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} (f : ) (g : ) :
g.completion.comp f.completion = (g.comp f).completion
theorem NormedAddGroupHom.completion_neg {G : Type u_1} {H : Type u_2} (f : ) :
(-f).completion = -f.completion
theorem NormedAddGroupHom.completion_add {G : Type u_1} {H : Type u_2} (f : ) (g : ) :
(f + g).completion = f.completion + g.completion
theorem NormedAddGroupHom.completion_sub {G : Type u_1} {H : Type u_2} (f : ) (g : ) :
(f - g).completion = f.completion - g.completion
@[simp]
theorem NormedAddGroupHom.zero_completion {G : Type u_1} {H : Type u_2} :
@[simp]
theorem NormedAddCommGroup.toCompl_apply {G : Type u_1} :
∀ (a : G), NormedAddCommGroup.toCompl a = G a

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

Equations
• NormedAddCommGroup.toCompl = { toFun := G, map_add' := , bound' := }
Instances For
theorem NormedAddCommGroup.norm_toCompl {G : Type u_1} (x : G) :
theorem NormedAddCommGroup.denseRange_toCompl {G : Type u_1} :
@[simp]
theorem NormedAddGroupHom.completion_toCompl {G : Type u_1} {H : Type u_2} (f : ) :
@[simp]
theorem NormedAddGroupHom.norm_completion {G : Type u_1} {H : Type u_2} (f : ) :
f.completion = f
theorem NormedAddGroupHom.ker_le_ker_completion {G : Type u_1} {H : Type u_2} (f : ) :
theorem NormedAddGroupHom.ker_completion {G : Type u_1} {H : Type u_2} {f : } {C : } (h : f.SurjectiveOnWith f.range C) :
def NormedAddGroupHom.extension {G : Type u_1} {H : Type u_2} [] [] (f : ) :

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

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