Completions of normed groups

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

Main definitions

• SemiNormedGroupCat.Completion : SemiNormedGroupCat ⥤ SemiNormedGroupCat : the completion of a seminormed group (defined as a functor on SemiNormedGroupCat to itself).
• SemiNormedGroupCat.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 CompleteSemiNormedGroupCat and promote the Completion functor below to a functor landing in this category.
2. Prove that the functor Completion : SemiNormedGroupCat ⥤ CompleteSemiNormedGroupCat is left adjoint to the forgetful functor.

@[simp]

theorem SemiNormedGroupCat.completion_obj (V : SemiNormedGroupCat) : SemiNormedGroupCat.completion.obj V = SemiNormedGroupCat.of (UniformSpace.Completion ↑V)

@[simp]

theorem SemiNormedGroupCat.completion_map : ∀ {X Y : SemiNormedGroupCat} (f : X ⟶ Y), SemiNormedGroupCat.completion.map f = NormedAddGroupHom.completion f

def SemiNormedGroupCat.completion : CategoryTheory.Functor SemiNormedGroupCat SemiNormedGroupCat

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

Equations

• One or more equations did not get rendered due to their size.

instance SemiNormedGroupCat.completion_completeSpace {V : SemiNormedGroupCat} : CompleteSpace ↑(SemiNormedGroupCat.completion.obj V)

Equations

• ⋯ = ⋯

@[simp]

theorem SemiNormedGroupCat.completion.incl_apply {V : SemiNormedGroupCat} (v : ↑V) : SemiNormedGroupCat.completion.incl v = ↑↑V v

def SemiNormedGroupCat.completion.incl {V : SemiNormedGroupCat} : V ⟶ SemiNormedGroupCat.completion.obj V

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

Equations

• SemiNormedGroupCat.completion.incl = { toFun := fun (v : ↑V) => ↑↑V v, map_add' := ⋯, bound' := ⋯ }

theorem SemiNormedGroupCat.completion.norm_incl_eq {V : SemiNormedGroupCat} {v : ↑V} : ‖SemiNormedGroupCat.completion.incl v‖ = ‖v‖

theorem SemiNormedGroupCat.completion.map_normNoninc {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} {f : V ⟶ W} (hf : NormedAddGroupHom.NormNoninc f) : NormedAddGroupHom.NormNoninc (SemiNormedGroupCat.completion.map f)

def SemiNormedGroupCat.completion.mapHom (V : SemiNormedGroupCat) (W : SemiNormedGroupCat) : let_fun this := fun (V W : SemiNormedGroupCat) => inferInstanceAs (AddGroup (NormedAddGroupHom ↑V ↑W)); (V ⟶ W) →+ (SemiNormedGroupCat.completion.obj V ⟶ SemiNormedGroupCat.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

• SemiNormedGroupCat.completion.mapHom V W = AddMonoidHom.mk' SemiNormedGroupCat.completion.map ⋯

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

instance SemiNormedGroupCat.instPreadditive : CategoryTheory.Preadditive SemiNormedGroupCat

Equations

• One or more equations did not get rendered due to their size.

instance SemiNormedGroupCat.instAdditiveCompletion : SemiNormedGroupCat.completion.Additive

Equations

• SemiNormedGroupCat.instAdditiveCompletion = ⋯

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

• SemiNormedGroupCat.completion.lift f = { toFun := ⇑(NormedAddGroupHom.extension f), map_add' := ⋯, bound' := ⋯ }

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

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