Documentation

Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels

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 ⋯) ⋯

Instances For

def SemiNormedGrp₁.cokernelLift {X 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) ⋯, ⋯⟩

Instances For

instance SemiNormedGrp₁.instHasCokernels :

CategoryTheory.Limits.HasCokernels SemiNormedGrp₁

Equations

SemiNormedGrp₁.instHasCokernels = ⋯

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))) ⋯

Instances For

instance SemiNormedGrp.hasLimit_parallelPair {V W : SemiNormedGrp} (f 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 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 ⋯

Instances For

noncomputable def SemiNormedGrp.cokernelLift {X 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) ⋯

Instances For

noncomputable def SemiNormedGrp.isColimitCokernelCocone {X 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) ⋯ ⋯

Instances For

instance SemiNormedGrp.instHasCokernels :

CategoryTheory.Limits.HasCokernels SemiNormedGrp

Equations

SemiNormedGrp.instHasCokernels = ⋯

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

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

Equations

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

Instances For

noncomputable def SemiNormedGrp.explicitCokernelDesc {X Y 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 ⋯)

Instances For

noncomputable def SemiNormedGrp.explicitCokernelπ {X 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

Instances For

theorem SemiNormedGrp.explicitCokernelπ_surjective {X Y : SemiNormedGrp} {f : X ⟶ Y} :

Function.Surjective ⇑(SemiNormedGrp.explicitCokernelπ f)

@[simp]

theorem SemiNormedGrp.comp_explicitCokernelπ {X Y : SemiNormedGrp} (f : X ⟶ Y) :

CategoryTheory.CategoryStruct.comp f (SemiNormedGrp.explicitCokernelπ f) = 0

@[simp]

theorem SemiNormedGrp.comp_explicitCokernelπ_assoc {X 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 Y : SemiNormedGrp} {f : X ⟶ Y} (x : ↑X) :

(SemiNormedGrp.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 (SemiNormedGrp.explicitCokernelπ f) (SemiNormedGrp.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 (SemiNormedGrp.explicitCokernelπ f) (CategoryTheory.CategoryStruct.comp (SemiNormedGrp.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) :

(SemiNormedGrp.explicitCokernelDesc cond) ((SemiNormedGrp.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 : SemiNormedGrp.explicitCokernel f ⟶ Z) (he : CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) e = g) :

e = SemiNormedGrp.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 (SemiNormedGrp.explicitCokernelDesc cond') h = SemiNormedGrp.explicitCokernelDesc ⋯

@[simp]

theorem SemiNormedGrp.explicitCokernelDesc_zero {X Y Z : SemiNormedGrp} {f : X ⟶ Y} :

SemiNormedGrp.explicitCokernelDesc ⋯ = 0

theorem SemiNormedGrp.explicitCokernel_hom_ext {X Y Z : SemiNormedGrp} {f : X ⟶ Y} (e₁ 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 Y : SemiNormedGrp} {f : X ⟶ Y} :

CategoryTheory.Epi (SemiNormedGrp.explicitCokernelπ f)

Equations

⋯ = ⋯

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

NormedAddGroupHom.IsQuotient (SemiNormedGrp.explicitCokernelπ f)

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

NormedAddGroupHom.NormNoninc (SemiNormedGrp.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) :

‖SemiNormedGrp.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 (SemiNormedGrp.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 (SemiNormedGrp.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) :

‖SemiNormedGrp.explicitCokernelDesc w‖ ≤ ‖g‖

noncomputable def SemiNormedGrp.explicitCokernelIso {X 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))

Instances For

@[simp]

theorem SemiNormedGrp.explicitCokernelIso_hom_π {X 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 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 Y 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 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) :

SemiNormedGrp.explicitCokernel fab ⟶ SemiNormedGrp.explicitCokernel fcd

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

Equations

SemiNormedGrp.explicitCokernel.map h = SemiNormedGrp.explicitCokernelDesc ⋯

Instances For

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