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.

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

Auxiliary definition for HasCokernels SemiNormedGrp₁.

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

Auxiliary definition for HasCokernels SemiNormedGrp₁.

instance SemiNormedGrp₁.instHasCokernels : CategoryTheory.Limits.HasCokernels SemiNormedGrp₁

noncomputable instance SemiNormedGrp.instNormHom {V W : SemiNormedGrp} : Norm (V ⟶ W)

noncomputable instance SemiNormedGrp.instNNNormHom {V W : SemiNormedGrp} : NNNorm (V ⟶ W)

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

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

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

instance SemiNormedGrp.instHasEqualizers : CategoryTheory.Limits.HasEqualizers SemiNormedGrp

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

Auxiliary definition for HasCokernels SemiNormedGrp.

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

Auxiliary definition for HasCokernels SemiNormedGrp.

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

Auxiliary definition for HasCokernels SemiNormedGrp.

instance SemiNormedGrp.instHasCokernels : CategoryTheory.Limits.HasCokernels SemiNormedGrp

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

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

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

Descend to the explicit cokernel.

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

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

theorem SemiNormedGrp.explicitCokernelπ_surjective {X Y : SemiNormedGrp} {f : X ⟶ Y} : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (explicitCokernelπ f))

@[simp]

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

@[simp]

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

@[simp]

theorem SemiNormedGrp.explicitCokernelπ_apply_dom_eq_zero {X Y : SemiNormedGrp} {f : X ⟶ Y} (x : X.carrier) : (CategoryTheory.ConcreteCategory.hom (explicitCokernelπ f)) ((CategoryTheory.ConcreteCategory.hom f) x) = 0

@[simp]

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

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

@[simp]

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

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

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

@[simp]

theorem SemiNormedGrp.explicitCokernelDesc_zero {X Y Z : SemiNormedGrp} {f : X ⟶ Y} : explicitCokernelDesc ⋯ = 0

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

theorem SemiNormedGrp.explicitCokernel_hom_ext_iff {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {e₁ e₂ : explicitCokernel f ⟶ Z} : e₁ = e₂ ↔ CategoryTheory.CategoryStruct.comp (explicitCokernelπ f) e₁ = CategoryTheory.CategoryStruct.comp (explicitCokernelπ f) e₂

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

theorem SemiNormedGrp.isQuotient_explicitCokernelπ {X Y : SemiNormedGrp} (f : X ⟶ Y) : (Hom.hom (explicitCokernelπ f)).IsQuotient

theorem SemiNormedGrp.normNoninc_explicitCokernelπ {X Y : SemiNormedGrp} (f : X ⟶ Y) : (Hom.hom (explicitCokernelπ f)).NormNoninc

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

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

theorem SemiNormedGrp.explicitCokernelDesc_comp_eq_zero {X Y Z W : SemiNormedGrp} {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 (explicitCokernelDesc cond) h = 0

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

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

The explicit cokernel is isomorphic to the usual cokernel.

@[simp]

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

@[simp]

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

@[simp]

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

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

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

theorem SemiNormedGrp.ExplicitCoker.map_desc {A B C D B' D' : SemiNormedGrp} {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 (explicitCokernelDesc condb) g = CategoryTheory.CategoryStruct.comp (explicitCokernel.map h) (explicitCokernelDesc condd)

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