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

- Construct the category of complete seminormed groups, say
`CompleteSemiNormedGrp`

and promote the`Completion`

functor below to a functor landing in this category. - Prove that the functor
`Completion : SemiNormedGrp ⥤ CompleteSemiNormedGrp`

is left adjoint to the forgetful functor.

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

.

## Equations

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

## Instances For

## Equations

- ⋯ = ⋯

The canonical morphism from a seminormed group `V`

to its completion.

## Equations

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

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

## Equations

## Instances For

## Equations

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

## Equations

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

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