mathlib3 documentation

analysis.normed.group.SemiNormedGroup.kernels

Kernels and cokernels in SemiNormedGroup₁ and SemiNormedGroup #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We show that SemiNormedGroup₁ has cokernels (for which of course the cokernel.π f maps are norm non-increasing), as well as the easier result that SemiNormedGroup has cokernels. We also show that SemiNormedGroup has kernels.

So far, I don't see a way to state nicely what we really want: SemiNormedGroup 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 SemiNormedGroup one can always take a cokernel and rescale its norm (and hence making cokernel.π f arbitrarily large in norm), obtaining another categorical cokernel.

source
noncomputable def SemiNormedGroup₁.cokernel_cocone {X Y : SemiNormedGroup₁} (f : X ⟶ Y) :
category_theory.limits.cofork f 0

Auxiliary definition for has_cokernels SemiNormedGroup₁.

Equations
source
noncomputable def SemiNormedGroup₁.cokernel_lift {X Y : SemiNormedGroup₁} (f : X ⟶ Y) (s : category_theory.limits.cokernel_cofork f) :
(SemiNormedGroup₁.cokernel_cocone f).X ⟶ s.X

Auxiliary definition for has_cokernels SemiNormedGroup₁.

Equations
source
@[protected, instance]
def SemiNormedGroup₁.category_theory.limits.has_cokernels  :
category_theory.limits.has_cokernels SemiNormedGroup₁
source
noncomputable def SemiNormedGroup.fork {V W : SemiNormedGroup} (f g : V ⟶ W) :
category_theory.limits.fork f g

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

Equations
source
@[protected, instance]
def SemiNormedGroup.has_limit_parallel_pair {V W : SemiNormedGroup} (f g : V ⟶ W) :
category_theory.limits.has_limit (category_theory.limits.parallel_pair f g)
source
@[protected, instance]
def SemiNormedGroup.category_theory.limits.has_equalizers  :
category_theory.limits.has_equalizers SemiNormedGroup
source
noncomputable def SemiNormedGroup.cokernel_cocone {X Y : SemiNormedGroup} (f : X ⟶ Y) :
category_theory.limits.cofork f 0

Auxiliary definition for has_cokernels SemiNormedGroup.

Equations
source
noncomputable def SemiNormedGroup.cokernel_lift {X Y : SemiNormedGroup} (f : X ⟶ Y) (s : category_theory.limits.cokernel_cofork f) :
(SemiNormedGroup.cokernel_cocone f).X ⟶ s.X

Auxiliary definition for has_cokernels SemiNormedGroup.

Equations
source
noncomputable def SemiNormedGroup.is_colimit_cokernel_cocone {X Y : SemiNormedGroup} (f : X ⟶ Y) :
category_theory.limits.is_colimit (SemiNormedGroup.cokernel_cocone f)

Auxiliary definition for has_cokernels SemiNormedGroup.

Equations
source
@[protected, instance]
def SemiNormedGroup.category_theory.limits.has_cokernels  :
category_theory.limits.has_cokernels SemiNormedGroup
source
noncomputable def SemiNormedGroup.explicit_cokernel {X Y : SemiNormedGroup} (f : X ⟶ Y) :
SemiNormedGroup

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

Equations
source
noncomputable def SemiNormedGroup.explicit_cokernel_desc {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) :
SemiNormedGroup.explicit_cokernel f ⟶ Z

Descend to the explicit cokernel.

Equations
source
noncomputable def SemiNormedGroup.explicit_cokernel_π {X Y : SemiNormedGroup} (f : X ⟶ Y) :
Y ⟶ SemiNormedGroup.explicit_cokernel f

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

Equations
Instances for SemiNormedGroup.explicit_cokernel_π
source
theorem SemiNormedGroup.explicit_cokernel_π_surjective {X Y : SemiNormedGroup} {f : X ⟶ Y} :
function.surjective ⇑(SemiNormedGroup.explicit_cokernel_π f)
source
@[simp]
theorem SemiNormedGroup.comp_explicit_cokernel_π_assoc {X Y : SemiNormedGroup} (f : X ⟶ Y) {X' : SemiNormedGroup} (f' : SemiNormedGroup.explicit_cokernel f ⟶ X') :
f ≫ SemiNormedGroup.explicit_cokernel_π f ≫ f' = 0 ≫ f'
source
@[simp]
theorem SemiNormedGroup.comp_explicit_cokernel_π {X Y : SemiNormedGroup} (f : X ⟶ Y) :
f ≫ SemiNormedGroup.explicit_cokernel_π f = 0
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_π_apply_dom_eq_zero {X Y : SemiNormedGroup} {f : X ⟶ Y} (x : ↥X) :
⇑(SemiNormedGroup.explicit_cokernel_π f) (⇑f x) = 0
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_π_desc {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) :
SemiNormedGroup.explicit_cokernel_π f ≫ SemiNormedGroup.explicit_cokernel_desc w = g
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_π_desc_assoc {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) {X' : SemiNormedGroup} (f' : Z ⟶ X') :
SemiNormedGroup.explicit_cokernel_π f ≫ SemiNormedGroup.explicit_cokernel_desc w ≫ f' = g ≫ f'
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_π_desc_apply {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : f ≫ g = 0} (x : ↥Y) :
⇑(SemiNormedGroup.explicit_cokernel_desc cond) (⇑(SemiNormedGroup.explicit_cokernel_π f) x) = ⇑g x
source
theorem SemiNormedGroup.explicit_cokernel_desc_unique {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) (e : SemiNormedGroup.explicit_cokernel f ⟶ Z) (he : SemiNormedGroup.explicit_cokernel_π f ≫ e = g) :
e = SemiNormedGroup.explicit_cokernel_desc w
source
theorem SemiNormedGroup.explicit_cokernel_desc_comp_eq_desc {X Y Z W : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} {cond : f ≫ g = 0} :
SemiNormedGroup.explicit_cokernel_desc cond ≫ h = SemiNormedGroup.explicit_cokernel_desc _
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_desc_zero {X Y Z : SemiNormedGroup} {f : X ⟶ Y} :
SemiNormedGroup.explicit_cokernel_desc _ = 0
source
@[ext]
theorem SemiNormedGroup.explicit_cokernel_hom_ext {X Y Z : SemiNormedGroup} {f : X ⟶ Y} (e₁ e₂ : SemiNormedGroup.explicit_cokernel f ⟶ Z) (h : SemiNormedGroup.explicit_cokernel_π f ≫ e₁ = SemiNormedGroup.explicit_cokernel_π f ≫ e₂) :
e₁ = e₂
source
@[protected, instance]
def SemiNormedGroup.explicit_cokernel_π.epi {X Y : SemiNormedGroup} {f : X ⟶ Y} :
category_theory.epi (SemiNormedGroup.explicit_cokernel_π f)
source
theorem SemiNormedGroup.is_quotient_explicit_cokernel_π {X Y : SemiNormedGroup} (f : X ⟶ Y) :
normed_add_group_hom.is_quotient (SemiNormedGroup.explicit_cokernel_π f)
source
theorem SemiNormedGroup.norm_noninc_explicit_cokernel_π {X Y : SemiNormedGroup} (f : X ⟶ Y) :
normed_add_group_hom.norm_noninc (SemiNormedGroup.explicit_cokernel_π f)
source
theorem SemiNormedGroup.explicit_cokernel_desc_norm_le_of_norm_le {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) (c : nnreal) (h : ‖g‖ ≤ ↑c) :
‖SemiNormedGroup.explicit_cokernel_desc w‖ ≤ ↑c
source
theorem SemiNormedGroup.explicit_cokernel_desc_norm_noninc {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} {cond : f ≫ g = 0} (hg : normed_add_group_hom.norm_noninc g) :
normed_add_group_hom.norm_noninc (SemiNormedGroup.explicit_cokernel_desc cond)
source
theorem SemiNormedGroup.explicit_cokernel_desc_comp_eq_zero {X Y Z W : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} {h : Z ⟶ W} (cond : f ≫ g = 0) (cond2 : g ≫ h = 0) :
SemiNormedGroup.explicit_cokernel_desc cond ≫ h = 0
source
theorem SemiNormedGroup.explicit_cokernel_desc_norm_le {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) :
‖SemiNormedGroup.explicit_cokernel_desc w‖ ≤ ‖g‖
source
noncomputable def SemiNormedGroup.explicit_cokernel_iso {X Y : SemiNormedGroup} (f : X ⟶ Y) :
SemiNormedGroup.explicit_cokernel f ≅ category_theory.limits.cokernel f

The explicit cokernel is isomorphic to the usual cokernel.

Equations
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_iso_hom_π {X Y : SemiNormedGroup} (f : X ⟶ Y) :
SemiNormedGroup.explicit_cokernel_π f ≫ (SemiNormedGroup.explicit_cokernel_iso f).hom = category_theory.limits.cokernel.π f
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_iso_inv_π {X Y : SemiNormedGroup} (f : X ⟶ Y) :
category_theory.limits.cokernel.π f ≫ (SemiNormedGroup.explicit_cokernel_iso f).inv = SemiNormedGroup.explicit_cokernel_π f
source
@[simp]
theorem SemiNormedGroup.explicit_cokernel_iso_hom_desc {X Y Z : SemiNormedGroup} {f : X ⟶ Y} {g : Y ⟶ Z} (w : f ≫ g = 0) :
(SemiNormedGroup.explicit_cokernel_iso f).hom ≫ category_theory.limits.cokernel.desc f g w = SemiNormedGroup.explicit_cokernel_desc w
source
noncomputable def SemiNormedGroup.explicit_cokernel.map {A B C D : SemiNormedGroup} {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D} (h : fab ≫ fbd = fac ≫ fcd) :
SemiNormedGroup.explicit_cokernel fab ⟶ SemiNormedGroup.explicit_cokernel fcd

A special case of category_theory.limits.cokernel.map adapted to explicit_cokernel.

Equations
source
theorem SemiNormedGroup.explicit_coker.map_desc {A B C D B' D' : SemiNormedGroup} {fab : A ⟶ B} {fbd : B ⟶ D} {fac : A ⟶ C} {fcd : C ⟶ D} {h : fab ≫ fbd = fac ≫ fcd} {fbb' : B ⟶ B'} {fdd' : D ⟶ D'} {condb : fab ≫ fbb' = 0} {condd : fcd ≫ fdd' = 0} {g : B' ⟶ D'} (h' : fbb' ≫ g = fbd ≫ fdd') :
SemiNormedGroup.explicit_cokernel_desc condb ≫ g = SemiNormedGroup.explicit_cokernel.map h ≫ SemiNormedGroup.explicit_cokernel_desc condd

A special case of category_theory.limits.cokernel.map_desc adapted to explicit_cokernel.