Contributions to mathlib from LTE about normed groups
When the Liquid Tensor Experiment started, in December 2020, mathlib already had a decent theory of normed spaces. With this post I want to show how mathlib can benefit from projects like LTE, showing what we added to the theory of normed spaces in almost one year of work (this is only a small part of what has been added to mathlib from LTE, for a more complete list, see the history of for_mathlib folder).
Besides several small missing lemmas, we added the following notions.

normed_group_hom
: we already had the operator norm, but no bundled hom between normed groups. We introducednormed_group_hom G H
, that it is itself a normed group. We also introduced kernels and images of a normed groups hom. 
semi_normed_group
: a seminorm generalizes a norm by allowing nonzero vectors of zero (semi)norm. This notion is needed in LTE, and we introduced it in mathlib (providing a reasonable API). Sincenormed_group
depends onmetric_space
that in turn depends onemetric_space
, we had first of all introduced (extended) pseudo metric spaces. We also introducedsemi_normed_space
and similar related notions. 
normed_group_quotient
: the theory of quotients of (semi) normed groups was completely missing. We now have a good API for it. 
normed_group_hom.completion
: similarly tonormed_group_quotient
, mathlib did not know completions of normed groups. Using the already existing theory for topological groups, we added an API for completions of normed groups. 
nnnorm
: sometimes it is useful to consider the norm as taking values in the nonnegative reals. We introduced the classhas_nnnorm
, with the obvious instances, and wrote an API for it. 
SemiNormedGroup
: we introducedSemiNormedGroup
, the category of semi normed groups, as a preadditive category with kernels and cokernels. We promotednormed_group_hom.completion
to a functor, showing its universal property. Working with cokernels, an interesting problem arose: iff : X → Y
is a normed groups hom, one usually consider the cokernelcoker(f) = Y/Im(f)
, with the quotient norm and it is obvious that the projectionπ : Y → coker(f)
satisfies∥π∥ ≤ 1
. This is often needed in computations, but the category theory API doesn't promise any particular model of the cokernel, so one can for example scale the quotient norm by any positive factor, ending up with another cokernel, whose natural projection has norm bigger than1
. Iff
itself has norm less or equal than1
, one can work withSemiNormedGroup₁
, the category of seminormed groups and norm nonincreasing morphisms (that we proved has cokernels), but in general we ended up providingexplicit_cokernel f
, an explicit choice of cokernel, which has good properties with respect to the norm. This was enough for LTE, but still not completely satisfying, since one cannot directly use the category theory API forexplicit_cokernel
.