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} [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.

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) :

↑(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.

Instances For

@[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.

Instances For

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] [SeparatedSpace 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.

Instances For

theorem NormedAddGroupHom.extension_def {G : Type u_1} [SeminormedAddCommGroup G] {H : Type u_2} [SeminormedAddCommGroup H] [SeparatedSpace 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] [SeparatedSpace 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] [SeparatedSpace 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] [SeparatedSpace 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