# Documentation

Mathlib.Analysis.Normed.Group.HomCompletion

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

Instances For
theorem NormedAddGroupHom.completion_def {G : Type u_1} {H : Type u_2} (f : ) (x : ) :
=
@[simp]
theorem NormedAddGroupHom.completion_coe_to_fun {G : Type u_1} {H : Type u_2} (f : ) :
theorem NormedAddGroupHom.completion_coe {G : Type u_1} {H : Type u_2} (f : ) (g : G) :
↑() (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.

Instances For
@[simp]
theorem NormedAddGroupHom.completion_comp {G : Type u_1} {H : Type u_2} {K : Type u_3} (f : ) (g : ) :
theorem NormedAddGroupHom.completion_neg {G : Type u_1} {H : Type u_2} (f : ) :
theorem NormedAddGroupHom.completion_add {G : Type u_1} {H : Type u_2} (f : ) (g : ) :
theorem NormedAddGroupHom.completion_sub {G : Type u_1} {H : Type u_2} (f : ) (g : ) :
@[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.

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 : ) :
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 : } :
If H is complete, the extension of f : NormedAddGroupHom G H to a NormedAddGroupHom (completion G) H.