mathlib documentation

analysis.normed.group.hom_completion

Completion of normed group homs #

Given two (semi) normed groups G and H and a normed group hom f : normed_group_hom G H, we build and study a normed group hom f.completion : normed_group_hom (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: #

The normed group hom induced between completions.

Equations
@[simp]
theorem normed_group_hom.completion_coe {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] (f : normed_group_hom G H) (g : G) :

Completion of normed group homs as a normed group hom.

Equations
theorem normed_group_hom.completion_comp {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] {K : Type u_3} [semi_normed_group K] (f : normed_group_hom G H) (g : normed_group_hom H K) :
theorem normed_group_hom.completion_neg {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] (f : normed_group_hom G H) :
theorem normed_group_hom.completion_add {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] (f g : normed_group_hom G H) :
theorem normed_group_hom.completion_sub {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] (f g : normed_group_hom G H) :
@[simp]
theorem normed_group_hom.zero_completion {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] :

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

Equations
@[simp]
theorem normed_group_hom.norm_completion {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] (f : normed_group_hom G H) :

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

Equations
@[simp]
theorem normed_group_hom.extension_coe {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] [separated_space H] [complete_space H] (f : normed_group_hom G H) (v : G) :
theorem normed_group_hom.extension_unique {G : Type u_1} [semi_normed_group G] {H : Type u_2} [semi_normed_group H] [separated_space H] [complete_space H] (f : normed_group_hom G H) {g : normed_group_hom (uniform_space.completion G) H} (hg : ∀ (v : G), f v = g v) :