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

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

theorem NormedAddGroupHom.completion_def {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] (f : NormedAddGroupHom G H) (x : UniformSpace.Completion G) : (NormedAddGroupHom.completion f) 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) : ⇑(NormedAddGroupHom.completion f) = 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) : (NormedAddGroupHom.completion f) (↑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 = NormedAddGroupHom.completion f

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 = { toZeroHom := { toFun := NormedAddGroupHom.completion, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem NormedAddGroupHom.completion_id {G : Type u_1} [SeminormedAddCommGroup G] : NormedAddGroupHom.completion (NormedAddGroupHom.id G) = 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) : NormedAddGroupHom.comp (NormedAddGroupHom.completion g) (NormedAddGroupHom.completion f) = NormedAddGroupHom.completion (NormedAddGroupHom.comp g f)

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

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

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

@[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) : NormedAddGroupHom.comp (NormedAddGroupHom.completion f) NormedAddCommGroup.toCompl = NormedAddGroupHom.comp NormedAddCommGroup.toCompl f

@[simp]

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

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

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

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

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

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) : (NormedAddGroupHom.extension f) (↑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) : (NormedAddGroupHom.extension f) (↑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) : ⇑(NormedAddGroupHom.extension f) = 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)) : NormedAddGroupHom.extension f = g