Completions of normed groups #

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

This file contains an API for completions of seminormed groups (basic facts about objects and morphisms).

Main definitions #

SemiNormedGroup.Completion : SemiNormedGroup ⥤ SemiNormedGroup : the completion of a seminormed group (defined as a functor on SemiNormedGroup to itself).
SemiNormedGroup.Completion.lift (f : V ⟶ W) : (Completion.obj V ⟶ W) : a normed group hom from V to complete W extends ("lifts") to a seminormed group hom from the completion of V to W.

Projects #

Construct the category of complete seminormed groups, say CompleteSemiNormedGroup and promote the Completion functor below to a functor landing in this category.
Prove that the functor Completion : SemiNormedGroup ⥤ CompleteSemiNormedGroup is left adjoint to the forgetful functor.

source

noncomputable def SemiNormedGroup.Completion :

SemiNormedGroup ⥤ SemiNormedGroup

The completion of a seminormed group, as an endofunctor on SemiNormedGroup.

Equations

SemiNormedGroup.Completion = {obj := λ (V : SemiNormedGroup), SemiNormedGroup.of (uniform_space.completion ↥V), map := λ (V W : SemiNormedGroup) (f : V ⟶ W), normed_add_group_hom.completion f, map_id' := SemiNormedGroup.Completion._proof_1, map_comp' := SemiNormedGroup.Completion._proof_2}

Instances for SemiNormedGroup.Completion

SemiNormedGroup.Completion.category_theory.functor.additive

source

@[simp]

theorem SemiNormedGroup.Completion_map (V W : SemiNormedGroup) (f : V ⟶ W) :

SemiNormedGroup.Completion.map f = normed_add_group_hom.completion f

source

@[simp]

theorem SemiNormedGroup.Completion_obj (V : SemiNormedGroup) :

SemiNormedGroup.Completion.obj V = SemiNormedGroup.of (uniform_space.completion ↥V)

source

@[protected, instance]

def SemiNormedGroup.Completion_complete_space {V : SemiNormedGroup} :

complete_space ↥(SemiNormedGroup.Completion.obj V)

source

@[simp]

theorem SemiNormedGroup.Completion.incl_apply {V : SemiNormedGroup} (v : ↥V) :

⇑SemiNormedGroup.Completion.incl v = ↑v

source

def SemiNormedGroup.Completion.incl {V : SemiNormedGroup} :

V ⟶ SemiNormedGroup.Completion.obj V

The canonical morphism from a seminormed group V to its completion.

Equations

SemiNormedGroup.Completion.incl = {to_fun := λ (v : ↥V), ↑v, map_add' := _, bound' := _}

source

theorem SemiNormedGroup.Completion.norm_incl_eq {V : SemiNormedGroup} {v : ↥V} :

‖⇑SemiNormedGroup.Completion.incl v‖ = ‖v‖

source

theorem SemiNormedGroup.Completion.map_norm_noninc {V W : SemiNormedGroup} {f : V ⟶ W} (hf : normed_add_group_hom.norm_noninc f) :

normed_add_group_hom.norm_noninc (SemiNormedGroup.Completion.map f)

source

noncomputable def SemiNormedGroup.Completion.map_hom (V W : SemiNormedGroup) :

(V ⟶ W) →+ (SemiNormedGroup.Completion.obj V ⟶ SemiNormedGroup.Completion.obj W)

Given a normed group hom V ⟶ W, this defines the associated morphism from the completion of V to the completion of W. The difference from the definition obtained from the functoriality of completion is in that the map sending a morphism f to the associated morphism of completions is itself additive.

Equations

SemiNormedGroup.Completion.map_hom V W = add_monoid_hom.mk' SemiNormedGroup.Completion.map _

source

@[simp]

theorem SemiNormedGroup.Completion.map_zero (V W : SemiNormedGroup) :

SemiNormedGroup.Completion.map 0 = 0

source

@[protected, instance]

noncomputable def SemiNormedGroup.category_theory.preadditive :

category_theory.preadditive SemiNormedGroup

Equations

SemiNormedGroup.category_theory.preadditive = {hom_group := λ (P Q : SemiNormedGroup), infer_instance, add_comp' := SemiNormedGroup.category_theory.preadditive._proof_1, comp_add' := SemiNormedGroup.category_theory.preadditive._proof_2}

source

@[protected, instance]

def SemiNormedGroup.Completion.category_theory.functor.additive :

SemiNormedGroup.Completion.additive

source

noncomputable def SemiNormedGroup.Completion.lift {V W : SemiNormedGroup} [complete_space ↥W] [separated_space ↥W] (f : V ⟶ W) :

SemiNormedGroup.Completion.obj V ⟶ W

Given a normed group hom f : V → W with W complete, this provides a lift of f to the completion of V. The lemmas lift_unique and lift_comp_incl provide the api for the universal property of the completion.

Equations

SemiNormedGroup.Completion.lift f = {to_fun := ⇑(normed_add_group_hom.extension f), map_add' := _, bound' := _}

source

theorem SemiNormedGroup.Completion.lift_comp_incl {V W : SemiNormedGroup} [complete_space ↥W] [separated_space ↥W] (f : V ⟶ W) :

SemiNormedGroup.Completion.incl ≫ SemiNormedGroup.Completion.lift f = f

source

theorem SemiNormedGroup.Completion.lift_unique {V W : SemiNormedGroup} [complete_space ↥W] [separated_space ↥W] (f : V ⟶ W) (g : SemiNormedGroup.Completion.obj V ⟶ W) :

SemiNormedGroup.Completion.incl ≫ g = f → g = SemiNormedGroup.Completion.lift f