mathlib documentation


Cokernels in SemiNormedGroup₁ and SemiNormedGroup #

We show that SemiNormedGroup₁ has cokernels (for which of course the cokernel.π f maps are norm non-increasing), as well as the easier result that SemiNormedGroup has cokernels.

So far, I don't see a way to state nicely what we really want: SemiNormedGroup has cokernels, and cokernel.π f is norm non-increasing. The problem is that the limits API doesn't promise you any particular model of the cokernel, and in SemiNormedGroup one can always take a cokernel and rescale its norm (and hence making cokernel.π f arbitrarily large in norm), obtaining another categorical cokernel.

An explicit choice of cokernel, which has good properties with respect to the norm.