Kernels and cokernels in SemiNormedGroupCat₁ and SemiNormedGroupCat

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

So far, I don't see a way to state nicely what we really want: SemiNormedGroupCat 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 SemiNormedGroupCat one can always take a cokernel and rescale its norm (and hence making cokernel.π f arbitrarily large in norm), obtaining another categorical cokernel.

def SemiNormedGroupCat₁.cokernelCocone {X : SemiNormedGroupCat₁} {Y : SemiNormedGroupCat₁} (f : X ⟶ Y) : CategoryTheory.Limits.Cofork f 0

Auxiliary definition for HasCokernels SemiNormedGroupCat₁.

def SemiNormedGroupCat₁.cokernelLift {X : SemiNormedGroupCat₁} {Y : SemiNormedGroupCat₁} (f : X ⟶ Y) (s : CategoryTheory.Limits.CokernelCofork f) : (SemiNormedGroupCat₁.cokernelCocone f).pt ⟶ s.pt

Auxiliary definition for HasCokernels SemiNormedGroupCat₁.

instance SemiNormedGroupCat₁.instHasCokernelsSemiNormedGroupCat₁InstLargeCategorySemiNormedGroupCat₁InstHasZeroMorphismsSemiNormedGroupCat₁InstLargeCategorySemiNormedGroupCat₁ : CategoryTheory.Limits.HasCokernels SemiNormedGroupCat₁

instance SemiNormedGroupCat.instSubHomSemiNormedGroupCatToQuiverToCategoryStructInstSemiNormedGroupCatLargeCategory {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} : Sub (V ⟶ W)

noncomputable instance SemiNormedGroupCat.instNormHomSemiNormedGroupCatToQuiverToCategoryStructInstSemiNormedGroupCatLargeCategory {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} : Norm (V ⟶ W)

noncomputable instance SemiNormedGroupCat.instNNNormHomSemiNormedGroupCatToQuiverToCategoryStructInstSemiNormedGroupCatLargeCategory {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} : NNNorm (V ⟶ W)

def SemiNormedGroupCat.fork {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} (f : V ⟶ W) (g : V ⟶ W) : CategoryTheory.Limits.Fork f g

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

instance SemiNormedGroupCat.hasLimit_parallelPair {V : SemiNormedGroupCat} {W : SemiNormedGroupCat} (f : V ⟶ W) (g : V ⟶ W) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)

instance SemiNormedGroupCat.instHasEqualizersSemiNormedGroupCatInstSemiNormedGroupCatLargeCategory : CategoryTheory.Limits.HasEqualizers SemiNormedGroupCat

noncomputable def SemiNormedGroupCat.cokernelCocone {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : CategoryTheory.Limits.Cofork f 0

Auxiliary definition for HasCokernels SemiNormedGroupCat.

noncomputable def SemiNormedGroupCat.cokernelLift {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) (s : CategoryTheory.Limits.CokernelCofork f) : (SemiNormedGroupCat.cokernelCocone f).pt ⟶ s.pt

Auxiliary definition for HasCokernels SemiNormedGroupCat.

noncomputable def SemiNormedGroupCat.isColimitCokernelCocone {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : CategoryTheory.Limits.IsColimit (SemiNormedGroupCat.cokernelCocone f)

Auxiliary definition for HasCokernels SemiNormedGroupCat.

instance SemiNormedGroupCat.instHasCokernelsSemiNormedGroupCatInstSemiNormedGroupCatLargeCategoryInstHasZeroMorphismsSemiNormedGroupCatInstSemiNormedGroupCatLargeCategory : CategoryTheory.Limits.HasCokernels SemiNormedGroupCat

noncomputable def SemiNormedGroupCat.explicitCokernel {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : SemiNormedGroupCat

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

noncomputable def SemiNormedGroupCat.explicitCokernelDesc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) : SemiNormedGroupCat.explicitCokernel f ⟶ Z

Descend to the explicit cokernel.

noncomputable def SemiNormedGroupCat.explicitCokernelπ {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : Y ⟶ SemiNormedGroupCat.explicitCokernel f

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

theorem SemiNormedGroupCat.explicitCokernelπ_surjective {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {f : X ⟶ Y} : Function.Surjective ↑(SemiNormedGroupCat.explicitCokernelπ f)

@[simp]

theorem SemiNormedGroupCat.comp_explicitCokernelπ_assoc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) {Z : SemiNormedGroupCat} (h : SemiNormedGroupCat.explicitCokernel f ⟶ Z) : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) h) = CategoryTheory.CategoryStruct.comp 0 h

@[simp]

theorem SemiNormedGroupCat.comp_explicitCokernelπ {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp f (SemiNormedGroupCat.explicitCokernelπ f) = 0

@[simp]

theorem SemiNormedGroupCat.explicitCokernelπ_apply_dom_eq_zero {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {f : X ⟶ Y} (x : ↑X) : ↑(SemiNormedGroupCat.explicitCokernelπ f) (↑f x) = 0

theorem SemiNormedGroupCat.explicitCokernelπ_desc_assoc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) {Z : SemiNormedGroupCat} (h : Z ⟶ Z) : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) (CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelDesc w) h) = CategoryTheory.CategoryStruct.comp g h

@[simp]

theorem SemiNormedGroupCat.explicitCokernelπ_desc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) (SemiNormedGroupCat.explicitCokernelDesc w) = g

@[simp]

theorem SemiNormedGroupCat.explicitCokernelπ_desc_apply {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : CategoryTheory.CategoryStruct.comp f g = 0} (x : ↑Y) : ↑(SemiNormedGroupCat.explicitCokernelDesc cond) (↑(SemiNormedGroupCat.explicitCokernelπ f) x) = ↑g x

theorem SemiNormedGroupCat.explicitCokernelDesc_unique {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) (e : SemiNormedGroupCat.explicitCokernel f ⟶ Z) (he : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) e = g) : e = SemiNormedGroupCat.explicitCokernelDesc w

theorem SemiNormedGroupCat.explicitCokernelDesc_comp_eq_desc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {W : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} {cond' : CategoryTheory.CategoryStruct.comp f g = 0} : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelDesc cond') h = SemiNormedGroupCat.explicitCokernelDesc (_ : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h) = 0)

@[simp]

theorem SemiNormedGroupCat.explicitCokernelDesc_zero {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} : SemiNormedGroupCat.explicitCokernelDesc (_ : CategoryTheory.CategoryStruct.comp f 0 = 0) = 0

theorem SemiNormedGroupCat.explicitCokernel_hom_ext {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} (e₁ : SemiNormedGroupCat.explicitCokernel f ⟶ Z) (e₂ : SemiNormedGroupCat.explicitCokernel f ⟶ Z) (h : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) e₁ = CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) e₂) : e₁ = e₂

instance SemiNormedGroupCat.explicitCokernelπ.epi {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {f : X ⟶ Y} : CategoryTheory.Epi (SemiNormedGroupCat.explicitCokernelπ f)

theorem SemiNormedGroupCat.isQuotient_explicitCokernelπ {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : NormedAddGroupHom.IsQuotient (SemiNormedGroupCat.explicitCokernelπ f)

theorem SemiNormedGroupCat.normNoninc_explicitCokernelπ {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : NormedAddGroupHom.NormNoninc (SemiNormedGroupCat.explicitCokernelπ f)

theorem SemiNormedGroupCat.explicitCokernelDesc_norm_le_of_norm_le {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) (c : NNReal) (h : ‖g‖ ≤ ↑c) : ‖SemiNormedGroupCat.explicitCokernelDesc w‖ ≤ ↑c

theorem SemiNormedGroupCat.explicitCokernelDesc_normNoninc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : CategoryTheory.CategoryStruct.comp f g = 0} (hg : NormedAddGroupHom.NormNoninc g) : NormedAddGroupHom.NormNoninc (SemiNormedGroupCat.explicitCokernelDesc cond)

theorem SemiNormedGroupCat.explicitCokernelDesc_comp_eq_zero {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {W : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} (cond : CategoryTheory.CategoryStruct.comp f g = 0) (cond2 : CategoryTheory.CategoryStruct.comp g h = 0) : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelDesc cond) h = 0

theorem SemiNormedGroupCat.explicitCokernelDesc_norm_le {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) : ‖SemiNormedGroupCat.explicitCokernelDesc w‖ ≤ ‖g‖

noncomputable def SemiNormedGroupCat.explicitCokernelIso {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : SemiNormedGroupCat.explicitCokernel f ≅ CategoryTheory.Limits.cokernel f

The explicit cokernel is isomorphic to the usual cokernel.

@[simp]

theorem SemiNormedGroupCat.explicitCokernelIso_hom_π {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) (SemiNormedGroupCat.explicitCokernelIso f).hom = CategoryTheory.Limits.cokernel.π f

@[simp]

theorem SemiNormedGroupCat.explicitCokernelIso_inv_π {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π f) (SemiNormedGroupCat.explicitCokernelIso f).inv = SemiNormedGroupCat.explicitCokernelπ f

@[simp]

theorem SemiNormedGroupCat.explicitCokernelIso_hom_desc {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelIso f).hom (CategoryTheory.Limits.cokernel.desc f g w) = SemiNormedGroupCat.explicitCokernelDesc w

noncomputable def SemiNormedGroupCat.explicitCokernel.map {A : SemiNormedGroupCat} {B : SemiNormedGroupCat} {C : SemiNormedGroupCat} {D : SemiNormedGroupCat} {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D} (h : CategoryTheory.CategoryStruct.comp fab fbd = CategoryTheory.CategoryStruct.comp fac fcd) : SemiNormedGroupCat.explicitCokernel fab ⟶ SemiNormedGroupCat.explicitCokernel fcd

A special case of CategoryTheory.Limits.cokernel.map adapted to explicitCokernel.

theorem SemiNormedGroupCat.ExplicitCoker.map_desc {A : SemiNormedGroupCat} {B : SemiNormedGroupCat} {C : SemiNormedGroupCat} {D : SemiNormedGroupCat} {B' : SemiNormedGroupCat} {D' : SemiNormedGroupCat} {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D} {h : CategoryTheory.CategoryStruct.comp fab fbd = CategoryTheory.CategoryStruct.comp fac fcd} {fbb' : B ⟶ B'} {fdd' : D ⟶ D'} {condb : CategoryTheory.CategoryStruct.comp fab fbb' = 0} {condd : CategoryTheory.CategoryStruct.comp fcd fdd' = 0} {g : B' ⟶ D'} (h' : CategoryTheory.CategoryStruct.comp fbb' g = CategoryTheory.CategoryStruct.comp fbd fdd') : CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelDesc condb) g = CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernel.map h) (SemiNormedGroupCat.explicitCokernelDesc condd)

A special case of CategoryTheory.Limits.cokernel.map_desc adapted to explicitCokernel.