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} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : NormedAddGroupHom (UniformSpace.Completion G) (UniformSpace.Completion H)

The normed group hom induced between completions.

Equations

• f.completion = NormedAddGroupHom.ofLipschitz (f.toAddMonoidHom.completion ⋯) ⋯

theorem NormedAddGroupHom.completion_def {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (x : UniformSpace.Completion G) : f.completion x = UniformSpace.Completion.map (⇑f) x

@[simp]

theorem NormedAddGroupHom.completion_coe_to_fun {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : ⇑f.completion = UniformSpace.Completion.map ⇑f

theorem NormedAddGroupHom.completion_coe {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (g : G) : f.completion (↑G g) = ↑H (f g)

@[simp]

theorem NormedAddGroupHom.completion_coe' {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (g : G) : UniformSpace.Completion.map (⇑f) (↑G g) = ↑H (f g)

@[simp]

theorem normedAddGroupHomCompletionHom_apply {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : normedAddGroupHomCompletionHom f = f.completion

def normedAddGroupHomCompletionHom {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] : NormedAddGroupHom G H →+ NormedAddGroupHom (UniformSpace.Completion G) (UniformSpace.Completion H)

Completion of normed group homs as a normed group hom.

Equations

• normedAddGroupHomCompletionHom = { toFun := NormedAddGroupHom.completion, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem NormedAddGroupHom.completion_id {G : Type u_1} [SeminormedAddCommGroup G] : (NormedAddGroupHom.id G).completion = NormedAddGroupHom.id (UniformSpace.Completion G)

theorem NormedAddGroupHom.completion_comp {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] {K : Type u_3} [SeminormedAddCommGroup K] (f : NormedAddGroupHom G H) (g : NormedAddGroupHom H K) : g.completion.comp f.completion = (g.comp f).completion

theorem NormedAddGroupHom.completion_neg {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : (-f).completion = -f.completion

theorem NormedAddGroupHom.completion_add {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (g : NormedAddGroupHom G H) : (f + g).completion = f.completion + g.completion

theorem NormedAddGroupHom.completion_sub {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (g : NormedAddGroupHom G H) : (f - g).completion = f.completion - g.completion

@[simp]

theorem NormedAddGroupHom.zero_completion {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] : NormedAddGroupHom.completion 0 = 0

@[simp]

theorem NormedAddCommGroup.toCompl_apply {G : Type u_1} [SeminormedAddCommGroup G] : ∀ (a : G), NormedAddCommGroup.toCompl a = ↑G a

def NormedAddCommGroup.toCompl {G : Type u_1} [SeminormedAddCommGroup G] : NormedAddGroupHom G (UniformSpace.Completion G)

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

Equations

• NormedAddCommGroup.toCompl = { toFun := ↑G, map_add' := ⋯, bound' := ⋯ }

theorem NormedAddCommGroup.norm_toCompl {G : Type u_1} [SeminormedAddCommGroup G] (x : G) : ‖NormedAddCommGroup.toCompl x‖ = ‖x‖

theorem NormedAddCommGroup.denseRange_toCompl {G : Type u_1} [SeminormedAddCommGroup G] : DenseRange ⇑NormedAddCommGroup.toCompl

@[simp]

theorem NormedAddGroupHom.completion_toCompl {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : f.completion.comp NormedAddCommGroup.toCompl = NormedAddCommGroup.toCompl.comp f

@[simp]

theorem NormedAddGroupHom.norm_completion {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : ‖f.completion‖ = ‖f‖

theorem NormedAddGroupHom.ker_le_ker_completion {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) : (NormedAddCommGroup.toCompl.comp (NormedAddGroupHom.incl f.ker)).range ≤ f.completion.ker

theorem NormedAddGroupHom.ker_completion {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] {f : NormedAddGroupHom G H} {C : ℝ} (h : f.SurjectiveOnWith f.range C) : ↑f.completion.ker = closure ↑(NormedAddCommGroup.toCompl.comp (NormedAddGroupHom.incl f.ker)).range

def NormedAddGroupHom.extension {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] [T0Space H] [CompleteSpace H] (f : NormedAddGroupHom G H) : NormedAddGroupHom (UniformSpace.Completion G) H

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

Equations

• f.extension = NormedAddGroupHom.ofLipschitz (f.toAddMonoidHom.extension ⋯) ⋯

theorem NormedAddGroupHom.extension_def {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] [T0Space H] [CompleteSpace H] (f : NormedAddGroupHom G H) (v : G) : f.extension (↑G v) = UniformSpace.Completion.extension (⇑f) (↑G v)

@[simp]

theorem NormedAddGroupHom.extension_coe {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] [T0Space H] [CompleteSpace H] (f : NormedAddGroupHom G H) (v : G) : f.extension (↑G v) = f v

theorem NormedAddGroupHom.extension_coe_to_fun {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] [T0Space H] [CompleteSpace H] (f : NormedAddGroupHom G H) : ⇑f.extension = UniformSpace.Completion.extension ⇑f

theorem NormedAddGroupHom.extension_unique {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] [T0Space H] [CompleteSpace H] (f : NormedAddGroupHom G H) {g : NormedAddGroupHom (UniformSpace.Completion G) H} (hg : ∀ (v : G), f v = g (↑G v)) : f.extension = g