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

Equations

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

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

Auxiliary definition for HasCokernels SemiNormedGrp₁.

Equations

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

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

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

Equations

• SemiNormedGrp.instSubHom = inferInstance

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

Equations

• SemiNormedGrp.instNormHom = inferInstance

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

Equations

• SemiNormedGrp.instNNNormHom = inferInstance

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.

Equations

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

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.

Equations

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

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.

Equations

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

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

Auxiliary definition for HasCokernels SemiNormedGrp.

Equations

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

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.

Equations

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

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.

Equations

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

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

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

Equations

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

theorem SemiNormedGrp.explicitCokernelπ_surjective {X Y : SemiNormedGrp} {f : X ⟶ Y} : Function.Surjective ⇑(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) : (explicitCokernelπ f) (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) : (explicitCokernelDesc cond) ((explicitCokernelπ f) x) = 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₂

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

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

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

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 : NormedAddGroupHom.NormNoninc g) : NormedAddGroupHom.NormNoninc (explicitCokernelDesc cond)

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.

Equations

• SemiNormedGrp.explicitCokernelIso f = (SemiNormedGrp.isColimitCokernelCocone f).coconePointUniqueUpToIso (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Limits.parallelPair f 0))

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

Equations

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

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.