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₁.

Equations

• SemiNormedGroupCat₁.cokernelCocone f = CategoryTheory.Limits.Cofork.ofπ (SemiNormedGroupCat₁.mkHom (↑f).range.normedMk ⋯) ⋯

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₁.

Equations

• SemiNormedGroupCat₁.cokernelLift f s = ⟨NormedAddGroupHom.lift (↑f).range ↑(CategoryTheory.Limits.Cofork.π s) ⋯, ⋯⟩

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

Equations

• SemiNormedGroupCat₁.instHasCokernels = ⋯

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

Equations

• SemiNormedGroupCat.instSubHom = inferInstance

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

Equations

• SemiNormedGroupCat.instNormHom = inferInstance

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

Equations

• SemiNormedGroupCat.instNNNormHom = inferInstance

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.

Equations

• SemiNormedGroupCat.fork f g = CategoryTheory.Limits.Fork.ofι (NormedAddGroupHom.incl (NormedAddGroupHom.ker (f - g))) ⋯

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

Equations

• ⋯ = ⋯

instance SemiNormedGroupCat.instHasEqualizers : CategoryTheory.Limits.HasEqualizers SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instHasEqualizers = ⋯

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

Auxiliary definition for HasCokernels SemiNormedGroupCat.

Equations

• SemiNormedGroupCat.cokernelCocone f = CategoryTheory.Limits.Cofork.ofπ (NormedAddGroupHom.range f).normedMk ⋯

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.

Equations

• SemiNormedGroupCat.cokernelLift f s = NormedAddGroupHom.lift (NormedAddGroupHom.range f) (CategoryTheory.Limits.Cofork.π s) ⋯

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

Auxiliary definition for HasCokernels SemiNormedGroupCat.

Equations

• SemiNormedGroupCat.isColimitCokernelCocone f = CategoryTheory.Limits.isColimitAux (SemiNormedGroupCat.cokernelCocone f) (SemiNormedGroupCat.cokernelLift f) ⋯ ⋯

instance SemiNormedGroupCat.instHasCokernels : CategoryTheory.Limits.HasCokernels SemiNormedGroupCat

Equations

• SemiNormedGroupCat.instHasCokernels = ⋯

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.

Equations

• SemiNormedGroupCat.explicitCokernel f = (SemiNormedGroupCat.cokernelCocone f).pt

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.

Equations

• SemiNormedGroupCat.explicitCokernelDesc w = (SemiNormedGroupCat.isColimitCokernelCocone f).desc (CategoryTheory.Limits.Cofork.ofπ g ⋯)

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.

Equations

• SemiNormedGroupCat.explicitCokernelπ f = (SemiNormedGroupCat.cokernelCocone f).ι.app CategoryTheory.Limits.WalkingParallelPair.one

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 ⋯

@[simp]

theorem SemiNormedGroupCat.explicitCokernelDesc_zero {X : SemiNormedGroupCat} {Y : SemiNormedGroupCat} {Z : SemiNormedGroupCat} {f : X ⟶ Y} : SemiNormedGroupCat.explicitCokernelDesc ⋯ = 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)

Equations

• ⋯ = ⋯

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.

Equations

• One or more equations did not get rendered due to their size.

@[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.

Equations

• SemiNormedGroupCat.explicitCokernel.map h = SemiNormedGroupCat.explicitCokernelDesc ⋯

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.