Completions of normed groups

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

Main definitions

• SemiNormedGrp.Completion : SemiNormedGrp ⥤ SemiNormedGrp : the completion of a seminormed group (defined as a functor on SemiNormedGrp to itself).
• SemiNormedGrp.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

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

noncomputable def SemiNormedGrp.completion : CategoryTheory.Functor SemiNormedGrp SemiNormedGrp

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

@[simp]

theorem SemiNormedGrp.completion_map {X✝ Y✝ : SemiNormedGrp} (f : X✝ ⟶ Y✝) : completion.map f = ofHom (Hom.hom f).completion

@[simp]

theorem SemiNormedGrp.completion_obj_str (V : SemiNormedGrp) : (completion.obj V).str = NormedAddCommGroup.toSeminormedAddCommGroup

@[simp]

theorem SemiNormedGrp.completion_obj_carrier (V : SemiNormedGrp) : (completion.obj V).carrier = UniformSpace.Completion V.carrier

instance SemiNormedGrp.completion_completeSpace {V : SemiNormedGrp} : CompleteSpace (completion.obj V).carrier

noncomputable def SemiNormedGrp.completion.incl {V : SemiNormedGrp} : V ⟶ completion.obj V

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

theorem SemiNormedGrp.completion.norm_incl_eq {V : SemiNormedGrp} {v : V.carrier} : ‖(CategoryTheory.ConcreteCategory.hom incl) v‖ = ‖v‖

theorem SemiNormedGrp.completion.map_normNoninc {V W : SemiNormedGrp} {f : V ⟶ W} (hf : (Hom.hom f).NormNoninc) : (Hom.hom (completion.map f)).NormNoninc

noncomputable def SemiNormedGrp.completion.mapHom (V W : SemiNormedGrp) : (V ⟶ W) →+ (completion.obj V ⟶ 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.

theorem SemiNormedGrp.completion.map_zero (V W : SemiNormedGrp) : completion.map 0 = 0

@[implicit_reducible]

noncomputable instance SemiNormedGrp.instPreadditive : CategoryTheory.Preadditive SemiNormedGrp

instance SemiNormedGrp.instAdditiveCompletion : completion.Additive

noncomputable def SemiNormedGrp.completion.lift {V W : SemiNormedGrp} [CompleteSpace W.carrier] [T0Space W.carrier] (f : V ⟶ W) : 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.

theorem SemiNormedGrp.completion.lift_comp_incl {V W : SemiNormedGrp} [CompleteSpace W.carrier] [T0Space W.carrier] (f : V ⟶ W) : CategoryTheory.CategoryStruct.comp incl (lift f) = f

theorem SemiNormedGrp.completion.lift_unique {V W : SemiNormedGrp} [CompleteSpace W.carrier] [T0Space W.carrier] (f : V ⟶ W) (g : completion.obj V ⟶ W) : CategoryTheory.CategoryStruct.comp incl g = f → g = lift f