mathlib3 documentation

Kernels and cokernels in SemiNormedGroup₁ and SemiNormedGroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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. We also show that SemiNormedGroup has kernels.

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.

noncomputable def SemiNormedGroup.fork {V W : SemiNormedGroup} (f g : V W) :

The equalizer cone for a parallel pair of morphisms of seminormed groups.

noncomputable def SemiNormedGroup.explicit_cokernel {X Y : SemiNormedGroup} (f : X Y) :

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


The projection from Y to the explicit cokernel of X ⟶ Y.

Instances for SemiNormedGroup.explicit_cokernel_π
theorem SemiNormedGroup.explicit_cokernel_desc_comp_eq_zero {X Y Z W : SemiNormedGroup} {f : X Y} {g : Y Z} {h : Z W} (cond : f g = 0) (cond2 : g h = 0) :
noncomputable def {A B C D : SemiNormedGroup} {fab : A B} {fbd : B D} {fac : A C} {fcd : C D} (h : fab fbd = fac fcd) :

A special case of adapted to explicit_cokernel.

theorem SemiNormedGroup.explicit_coker.map_desc {A B C D B' D' : SemiNormedGroup} {fab : A B} {fbd : B D} {fac : A C} {fcd : C D} {h : fab fbd = fac fcd} {fbb' : B B'} {fdd' : D D'} {condb : fab fbb' = 0} {condd : fcd fdd' = 0} {g : B' D'} (h' : fbb' g = fbd fdd') :

A special case of category_theory.limits.cokernel.map_desc adapted to explicit_cokernel.