# 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 #

- 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.

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

.

## Instances For

The canonical morphism from a seminormed group `V`

to its completion.

## Instances For

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.