SemiNormedGroupCat.explicitCokernelDesc_unique
theorem SemiNormedGroupCat.explicitCokernelDesc_unique :
∀ {X Y Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z} (w : CategoryTheory.CategoryStruct.comp f g = 0)
(e : SemiNormedGroupCat.explicitCokernel f ⟶ Z),
CategoryTheory.CategoryStruct.comp (SemiNormedGroupCat.explicitCokernelπ f) e = g →
e = SemiNormedGroupCat.explicitCokernelDesc w
The theorem `SemiNormedGroupCat.explicitCokernelDesc_unique` states that for all objects `X`, `Y`, and `Z` in the category of seminormed abelian groups, given morphisms `f: X ⟶ Y` and `g: Y ⟶ Z` such that their composition `f ≫ g` is the zero morphism, and another morphism `e: explicitCokernel f ⟶ Z`, if the composition of the projection from `Y` to the explicit cokernel of `f` with `e` equals to `g`, then `e` is equal to the morphism obtained by descending to the explicit cokernel. This essentially provides the uniqueness part of the universal property of the explicit cokernel in the category of seminormed abelian groups.
More concisely: Given morphisms `f: X ⟶ Y`, `g: Y ⟶ Z` in the category of seminormed abelian groups with `f ≫ g = 0`, and `e: explicitCokernel(f) ⟶ Z` such that `p∘e = g` for the projection `p: Y ⟶ explicitCokernel(f)`, then `e = desc(g ∘ i)` where `i: Y ⟶ explicitCokernel(f)` is the canonical injection.
|
SemiNormedGroupCat.explicitCokernelDesc.proof_1
theorem SemiNormedGroupCat.explicitCokernelDesc.proof_1 :
∀ {X Y Z : SemiNormedGroupCat} {f : X ⟶ Y} {g : Y ⟶ Z},
CategoryTheory.CategoryStruct.comp f g = 0 →
CategoryTheory.CategoryStruct.comp f g = CategoryTheory.CategoryStruct.comp 0 g
This theorem states that for any three objects X, Y, and Z in the category of seminormed abelian groups, and any two morphisms f : X ⟶ Y and g : Y ⟶ Z, if the composition of f and g (represented by `f ≫ g`) is zero, then it is equivalent to the composition of the zero morphism and g (represented by `0 ≫ g`).
More concisely: If for any seminormed abelian groups X, Y, Z and morphisms f : X ➔ Y and g : Y ➔ Z, the composition of f and g (f ≫ g) is zero then it is equivalent to the composition of the zero morphism and g (0 ≫ g).
|
SemiNormedGroupCat.explicitCokernelπ_desc
theorem SemiNormedGroupCat.explicitCokernelπ_desc :
∀ {X Y 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
The theorem `SemiNormedGroupCat.explicitCokernelπ_desc` states that for any three objects (X, Y, Z) in the category of seminormed abelian groups and any two morphisms f from X to Y and g from Y to Z, if the composition of f and g is zero, then the composition of the projection from Y to the explicit cokernel of f and the descent to the explicit cokernel is equal to g. In other words, for a sequence of morphisms in the category of seminormed abelian groups that becomes zero upon composition, the composition of the morphism's projection to its cokernel and the descent to the cokernel equals the original morphism. This theorem is part of the theory of cokernels in the context of category theory.
More concisely: If the composition of morphisms f : X → Y and g : Y → Z in the category of seminormed abelian groups is zero, then the composition of the projection of f's cokernel and the descent to that cokernel equals g.
|
SemiNormedGroupCat.ExplicitCoker.map_desc
theorem SemiNormedGroupCat.ExplicitCoker.map_desc :
∀ {A B C D B' 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'},
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)
This theorem is a special case of the `CategoryTheory.Limits.cokernel.map_desc`, adapted to the concept of `explicitCokernel` in the context of seminormed group categories. Given seminormed group categories A, B, C, D, B', and D'; morphisms `fab : A ⟶ B`, `fbd : B ⟶ D`, `fac : A ⟶ C`, `fcd : C ⟶ D`, `fbb' : B ⟶ B'`, `fdd' : D ⟶ D'`, and `g : B' ⟶ D'`; and conditions `h : CategoryTheory.CategoryStruct.comp fab fbd = CategoryTheory.CategoryStruct.comp fac fcd`, `condb : CategoryTheory.CategoryStruct.comp fab fbb' = 0`, and `condd : CategoryTheory.CategoryStruct.comp fcd fdd' = 0`. The theorem states that if the composition of `fbb'` and `g` equals the composition of `fbd` and `fdd'`, then the composition of `SemiNormedGroupCat.explicitCokernelDesc condb` and `g` equals the composition of `SemiNormedGroupCat.explicitCokernel.map h` and `SemiNormedGroupCat.explicitCokernelDesc condd`.
More concisely: Given seminormed group categories A, B, C, D, B', and D'; morphisms `fab`, `fbd`, `fac`, `fcd`, `fbb'`, `fdd'`, and `g`; and conditions `h`, `condb`, and `condd`, if `h` and `condb` imply `g = fbd * fdd'`, then `(SemiNormedGroupCat.explicitCokernelDesc condb) * g = (SemiNormedGroupCat.explicitCokernel.map h) * SemiNormedGroupCat.explicitCokernelDesc condd`.
|