Commit 2021-07-27 19:34 2ea73d1cView on Github →
feat(analysis/normed_space/SemiNormedGroup): has_cokernels (#7628)
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,
SemiNormedGroup one can always take a cokernel and rescale its norm
(and hence making
cokernel.π f arbitrarily large in norm), obtaining another categorical cokernel.