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 : SemiNormedGrp₁} {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 : SemiNormedGrp₁} {Y : SemiNormedGrp₁} (f : X ⟶ Y) (s : CategoryTheory.Limits.CokernelCofork f) : (SemiNormedGrp₁.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₁

Equations

• SemiNormedGrp₁.instHasCokernels = ⋯

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

Equations

• SemiNormedGrp.instSubHom = inferInstance

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

Equations

• SemiNormedGrp.instNormHom = inferInstance

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

Equations

• SemiNormedGrp.instNNNormHom = inferInstance

def SemiNormedGrp.fork {V : SemiNormedGrp} {W : SemiNormedGrp} (f : V ⟶ W) (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 : SemiNormedGrp} {W : SemiNormedGrp} (f : V ⟶ W) (g : V ⟶ W) : CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)

Equations

• ⋯ = ⋯

instance SemiNormedGrp.instHasEqualizers : CategoryTheory.Limits.HasEqualizers SemiNormedGrp

Equations

• SemiNormedGrp.instHasEqualizers = ⋯

noncomputable def SemiNormedGrp.cokernelCocone {X : SemiNormedGrp} {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 : SemiNormedGrp} {Y : SemiNormedGrp} (f : X ⟶ Y) (s : CategoryTheory.Limits.CokernelCofork f) : (SemiNormedGrp.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 : SemiNormedGrp} {Y : SemiNormedGrp} (f : X ⟶ Y) : CategoryTheory.Limits.IsColimit (SemiNormedGrp.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

Equations

• SemiNormedGrp.instHasCokernels = ⋯

noncomputable def SemiNormedGrp.explicitCokernel {X : SemiNormedGrp} {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 : SemiNormedGrp} {Y : SemiNormedGrp} {Z : SemiNormedGrp} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0) : SemiNormedGrp.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 : SemiNormedGrp} {Y : SemiNormedGrp} (f : X ⟶ Y) : Y ⟶ SemiNormedGrp.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 : SemiNormedGrp} {Y : SemiNormedGrp} {f : X ⟶ Y} : Function.Surjective ⇑(SemiNormedGrp.explicitCokernelπ f)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

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

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

Equations

• ⋯ = ⋯

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

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

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

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

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

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

noncomputable def SemiNormedGrp.explicitCokernelIso {X : SemiNormedGrp} {Y : SemiNormedGrp} (f : X ⟶ Y) : SemiNormedGrp.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 : SemiNormedGrp} {Y : SemiNormedGrp} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) (SemiNormedGrp.explicitCokernelIso f).hom = CategoryTheory.Limits.cokernel.π f

@[simp]

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

@[simp]

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

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

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