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.

noncomputable 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 ⋯) ⋯

Instances For

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 = ↑(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 = ↑(f g)

noncomputable 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' := ⋯ }

Instances For

@[simp]

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

normedAddGroupHomCompletionHom f = f.completion

@[simp]

theorem NormedAddGroupHom.completion_id {G : Type u_1} [SeminormedAddCommGroup G] :

(id G).completion = 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 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 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] :

completion 0 = 0

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 := UniformSpace.Completion.coe', map_add' := ⋯, bound' := ⋯ }

Instances For

@[simp]

theorem NormedAddCommGroup.toCompl_apply {G : Type u_1} [SeminormedAddCommGroup G] (a✝ : G) :

toCompl a✝ = ↑a✝

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

‖toCompl x‖ = ‖x‖

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

DenseRange ⇑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 (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 (incl f.ker)).range

noncomputable 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 ⋯) ⋯

Instances For

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 ↑v = UniformSpace.Completion.extension ⇑f ↑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 ↑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 ↑v) :

f.extension = g