CategoryTheory.IsSplitCoequalizer.condition
theorem CategoryTheory.IsSplitCoequalizer.condition :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z},
CategoryTheory.IsSplitCoequalizer f g π →
CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π
This theorem, `CategoryTheory.IsSplitCoequalizer.condition`, in the field of Category Theory, states that for any category `C` with objects `X`, `Y`, and `Z`, and morphisms `f`, `g` from `X` to `Y`, and `π` from `Y` to `Z`, if `π` is a split coequalizer of `f` and `g`, then the composition of `π` with `f` is equal to the composition of `π` with `g`. This essentially means that `π` can 'uniformly' map the results of `f` and `g` from `X` to `Y` to object `Z` in the category.
More concisely: If `π:` `Y` `→` `Z` is a split coequalizer of `f:` `X` `→` `Y` and `g:` `X` `→` `Y` in a category `C`, then `π ∘ f = π ∘ g`.
|
CategoryTheory.IsSplitCoequalizer.leftSection_top
theorem CategoryTheory.IsSplitCoequalizer.leftSection_top :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
(self : CategoryTheory.IsSplitCoequalizer f g π),
CategoryTheory.CategoryStruct.comp self.leftSection f = CategoryTheory.CategoryStruct.comp π self.rightSection
In the context of category theory, the theorem `CategoryTheory.IsSplitCoequalizer.leftSection_top` states that for any category `C` with objects `X`, `Y`, and `Z`, and morphisms `f` and `g` from `X` to `Y`, and a morphism `π` from `Y` to `Z`, if `π` is a split coequalizer of `f` and `g`, then the composition of `leftSection` and `f` is equal to the composition of `π` and `rightSection`. Here, `leftSection` and `rightSection` are morphisms associated with the split coequalizer. In category theory, a split coequalizer is a coequalizer together with a specified morphism making the diagram commute.
More concisely: For any category `C` and morphisms `f: X -> Y`, `g: X -> Y`, `π: Y -> Z`, if `π` is a split coequalizer of `f` and `g`, then `π ∘ rightSection = leftSection ∘ f`.
|
CategoryTheory.IsSplitCoequalizer.leftSection_bottom
theorem CategoryTheory.IsSplitCoequalizer.leftSection_bottom :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
(self : CategoryTheory.IsSplitCoequalizer f g π),
CategoryTheory.CategoryStruct.comp self.leftSection g = CategoryTheory.CategoryStruct.id Y
The theorem `CategoryTheory.IsSplitCoequalizer.leftSection_bottom` states that for any category `C` with objects `X`, `Y`, and `Z`, and morphisms `f` and `g` from `X` to `Y`, and `π` from `Y` to `Z`, if `π` is a split coequalizer of `f` and `g`, then the composition of the left section of the split coequalizer and `g` is the identity morphism on object `Y`. In other words, the left section of the split coequalizer splits the morphism `g`.
More concisely: If `π : Y → Z` is a split coequalizer of `f, g : X → Y` in a category `C`, then the left section of `π`, denoted `s := π∘λx.π⁻¹(f x)`, satisfies `s ∘ g = id_Y`.
|
CategoryTheory.IsSplitCoequalizer.rightSection_π
theorem CategoryTheory.IsSplitCoequalizer.rightSection_π :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z}
(self : CategoryTheory.IsSplitCoequalizer f g π),
CategoryTheory.CategoryStruct.comp self.rightSection π = CategoryTheory.CategoryStruct.id Z
The theorem `CategoryTheory.IsSplitCoequalizer.rightSection_π` states that for any category `C` with objects `X`, `Y`, `Z`, and morphisms `f`, `g` from `X` to `Y`, and `π` from `Y` to `Z`, if `π` is a split coequalizer of `f` and `g`, then the composition of the right section of the split coequalizer with `π` results in the identity morphism on `Z`. In mathematical terms, if `π` is a split coequalizer, then `rightSection(π)∘π` is equal to `id(Z)`.
More concisely: If `π:` `Y` `→` `Z` is a split coequalizer of `f:` `X` `→` `Y` and `g:` `X` `→` `Y` in a category `C`, then `rightSection(π) ∘ π = id(Z)`.
|
CategoryTheory.HasSplitCoequalizer.splittable
theorem CategoryTheory.HasSplitCoequalizer.splittable :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y}
[self : CategoryTheory.HasSplitCoequalizer f g], ∃ Z h, Nonempty (CategoryTheory.IsSplitCoequalizer f g h)
This theorem states that in any category `C`, for any two objects `X` and `Y` and morphisms `f` and `g` from `X` to `Y`, if there is a split coequalizer of `f` and `g`, then there exists an object `Z` and a morphism `h` such that `h` is a split coequalizer of `f` and `g`. In categorical terms, a split coequalizer is a coequalizer together with a morphism in the opposite direction that splits it, that is, makes it isomorphic to the direct sum of its components.
More concisely: In any category, given two objects and morphisms with a split coequalizer, there exists an object and a split morphism making it the split coequalizer of the given morphisms.
|