mathlib3 documentation

analysis.normed.group.hom_completion

Completion of normed group homs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

normed_add_group_hom.completion: see the discussion above.
normed_add_comm_group.to_compl : normed_add_group_hom G (completion G): the canonical map from G to its completion, as a normed group hom
normed_add_group_hom.completion_to_compl: the above diagram indeed commutes.
normed_add_group_hom.norm_completion: ‖f.completion‖ = ‖f‖
normed_add_group_hom.ker_le_ker_completion: the kernel of f.completion contains the image of the kernel of f.
normed_add_group_hom.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.
normed_add_group_hom.extension : if H is complete, the extension of f : normed_add_group_hom G H to a normed_add_group_hom (completion G) H.

noncomputable def normed_add_group_hom.completion {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

normed_add_group_hom (uniform_space.completion G) (uniform_space.completion H)

The normed group hom induced between completions.

Equations

f.completion = {to_fun := (f.to_add_monoid_hom.completion _).to_fun, map_add' := _, bound' := _}

theorem normed_add_group_hom.completion_def {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) (x : uniform_space.completion G) :

⇑(f.completion) x = uniform_space.completion.map ⇑f x

@[simp]

theorem normed_add_group_hom.completion_coe_to_fun {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

⇑(f.completion) = uniform_space.completion.map ⇑f

@[simp]

theorem normed_add_group_hom.completion_coe {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) (g : G) :

⇑(f.completion) ↑g = ↑(⇑f g)

@[simp]

theorem normed_add_group_hom_completion_hom_apply {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

⇑normed_add_group_hom_completion_hom f = f.completion

noncomputable def normed_add_group_hom_completion_hom {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] :

normed_add_group_hom G H →+ normed_add_group_hom (uniform_space.completion G) (uniform_space.completion H)

Completion of normed group homs as a normed group hom.

Equations

normed_add_group_hom_completion_hom = {to_fun := normed_add_group_hom.completion _inst_2, map_zero' := _, map_add' := _}

@[simp]

theorem normed_add_group_hom.completion_id {G : Type u_1} [seminormed_add_comm_group G] :

(normed_add_group_hom.id G).completion = normed_add_group_hom.id (uniform_space.completion G)

theorem normed_add_group_hom.completion_comp {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] {K : Type u_3} [seminormed_add_comm_group K] (f : normed_add_group_hom G H) (g : normed_add_group_hom H K) :

g.completion.comp f.completion = (g.comp f).completion

theorem normed_add_group_hom.completion_neg {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

(-f).completion = -f.completion

theorem normed_add_group_hom.completion_add {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f g : normed_add_group_hom G H) :

(f + g).completion = f.completion + g.completion

theorem normed_add_group_hom.completion_sub {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f g : normed_add_group_hom G H) :

(f - g).completion = f.completion - g.completion

@[simp]

theorem normed_add_group_hom.zero_completion {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] :

0.completion = 0

def normed_add_comm_group.to_compl {G : Type u_1} [seminormed_add_comm_group G] :

normed_add_group_hom G (uniform_space.completion G)

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

Equations

normed_add_comm_group.to_compl = {to_fun := coe coe_to_lift, map_add' := _, bound' := _}

theorem normed_add_comm_group.norm_to_compl {G : Type u_1} [seminormed_add_comm_group G] (x : G) :

‖⇑normed_add_comm_group.to_compl x‖ = ‖x‖

theorem normed_add_comm_group.dense_range_to_compl {G : Type u_1} [seminormed_add_comm_group G] :

dense_range ⇑normed_add_comm_group.to_compl

@[simp]

theorem normed_add_group_hom.completion_to_compl {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

f.completion.comp normed_add_comm_group.to_compl = normed_add_comm_group.to_compl.comp f

@[simp]

theorem normed_add_group_hom.norm_completion {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

‖f.completion ‖ = ‖f‖

theorem normed_add_group_hom.ker_le_ker_completion {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] (f : normed_add_group_hom G H) :

(normed_add_comm_group.to_compl.comp (normed_add_group_hom.incl f.ker)).range ≤ f.completion.ker

theorem normed_add_group_hom.ker_completion {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] {f : normed_add_group_hom G H} {C : ℝ} (h : f.surjective_on_with f.range C) :

↑(f.completion.ker) = closure ↑((normed_add_comm_group.to_compl.comp (normed_add_group_hom.incl f.ker)).range)

noncomputable def normed_add_group_hom.extension {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] [separated_space H] [complete_space H] (f : normed_add_group_hom G H) :

normed_add_group_hom (uniform_space.completion G) H

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

Equations

f.extension = {to_fun := (f.to_add_monoid_hom.extension _).to_fun, map_add' := _, bound' := _}

theorem normed_add_group_hom.extension_def {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] [separated_space H] [complete_space H] (f : normed_add_group_hom G H) (v : G) :

⇑(f.extension) ↑v = uniform_space.completion.extension ⇑f ↑v

@[simp]

theorem normed_add_group_hom.extension_coe {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] [separated_space H] [complete_space H] (f : normed_add_group_hom G H) (v : G) :

⇑(f.extension) ↑v = ⇑f v

theorem normed_add_group_hom.extension_coe_to_fun {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] [separated_space H] [complete_space H] (f : normed_add_group_hom G H) :

⇑(f.extension) = uniform_space.completion.extension ⇑f

theorem normed_add_group_hom.extension_unique {G : Type u_1} [seminormed_add_comm_group G] {H : Type u_2} [seminormed_add_comm_group H] [separated_space H] [complete_space H] (f : normed_add_group_hom G H) {g : normed_add_group_hom (uniform_space.completion G) H} (hg : ∀ (v : G), ⇑f v = ⇑g ↑v) :

f.extension = g