Kernels and cokernels in SemiNormedGrp₁ and SemiNormedGrp #
We show that SemiNormedGrp₁
has cokernels
(for which of course the cokernel.π f
maps are norm non-increasing),
as well as the easier result that SemiNormedGrp
has cokernels. We also show that
SemiNormedGrp
has kernels.
So far, I don't see a way to state nicely what we really want:
SemiNormedGrp
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 SemiNormedGrp
one can always take a cokernel and rescale its norm
(and hence making cokernel.π f
arbitrarily large in norm), obtaining another categorical cokernel.
Auxiliary definition for HasCokernels SemiNormedGrp₁
.
Equations
Instances For
Auxiliary definition for HasCokernels SemiNormedGrp₁
.
Equations
Instances For
Equations
Equations
Equations
The equalizer cone for a parallel pair of morphisms of seminormed groups.
Equations
Instances For
Auxiliary definition for HasCokernels SemiNormedGrp
.
Equations
Instances For
Auxiliary definition for HasCokernels SemiNormedGrp
.
Equations
Instances For
Auxiliary definition for HasCokernels SemiNormedGrp
.
Equations
Instances For
An explicit choice of cokernel, which has good properties with respect to the norm.
Instances For
Descend to the explicit cokernel.
Equations
Instances For
The projection from Y
to the explicit cokernel of X ⟶ Y
.
Equations
Instances For
The explicit cokernel is isomorphic to the usual cokernel.
Equations
Instances For
A special case of CategoryTheory.Limits.cokernel.map
adapted to explicitCokernel
.
Instances For
A special case of CategoryTheory.Limits.cokernel.map_desc
adapted to explicitCokernel
.