# Documentation

Mathlib.Analysis.Normed.Group.SemiNormedGroupCat.Completion

# Completions of normed groups #

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 #

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

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

Instances For
@[simp]
theorem SemiNormedGroupCat.completion.incl_apply {V : SemiNormedGroupCat} (v : V) :
SemiNormedGroupCat.completion.incl v = V v

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

Instances For
theorem SemiNormedGroupCat.completion.norm_incl_eq {V : SemiNormedGroupCat} {v : V} :
SemiNormedGroupCat.completion.incl v = v

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.

Instances For

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.

Instances For
theorem SemiNormedGroupCat.completion.lift_unique {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} [] [] (f : V W) (g : ) :
CategoryTheory.CategoryStruct.comp SemiNormedGroupCat.completion.incl g = f