CategoryTheory.Factorisation.Hom.ext
theorem CategoryTheory.Factorisation.Hom.ext :
∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} {f : X ⟶ Y}
{d e : CategoryTheory.Factorisation f} (x y : d.Hom e), x.h = y.h → x = y
This theorem states that in the context of a category theory, given a category 'C' with objects 'X' and 'Y' and a morphism 'f' from 'X' to 'Y', for any two factorisations 'd' and 'e' of 'f', if we have two morphisms 'x' and 'y' from 'd' to 'e', then if the hom-set of 'x' equals the hom-set of 'y', 'x' and 'y' are themselves equal. This is essentially a statement of the uniqueness of such a morphism under these conditions.
More concisely: In a category, if two morphisms between factorizations of a given morphism have equal hom-sets, then they are equal.
|
CategoryTheory.Factorisation.Hom.ι_h
theorem CategoryTheory.Factorisation.Hom.ι_h :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{d e : CategoryTheory.Factorisation f} (self : d.Hom e), CategoryTheory.CategoryStruct.comp d.ι self.h = e.ι
This theorem, called `CategoryTheory.Factorisation.Hom.ι_h`, states that for any category `C` with objects `X` and `Y`, and a morphism `f` from `X` to `Y`, any two factorisations `d` and `e` of `f`, and any morphism `self` from `d` to `e`, the composition of the morphism `d.ι` with `self.h` is equal to the morphism `e.ι`. In other words, in the context of category theory, this theorem checks that the left triangle in the diagram that represents the factorisation of a morphism commutes.
More concisely: Given any category `C`, morphisms `f: X → Y`, factorizations `d → f → e`, and their connecting morphisms `self: d → e`, the composite `d.ι ∘ self.h` equals `e.ι`.
|
CategoryTheory.Factorisation.Hom.h_π
theorem CategoryTheory.Factorisation.Hom.h_π :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
{d e : CategoryTheory.Factorisation f} (self : d.Hom e), CategoryTheory.CategoryStruct.comp self.h e.π = d.π
This theorem, named `CategoryTheory.Factorisation.Hom.h_π`, states that for any category `C` with objects `X` and `Y`, and a morphism `f` from `X` to `Y`, given two factorisations `d` and `e` of `f`, if `self` is a morphism from `d` to `e`, then the composition of `self.h` and `e.π` (represented as `self.h ≫ e.π` in category theory notation) is equal to `d.π`. In other words, this theorem establishes the right commuting triangle property of the factorization's morphism in a category.
More concisely: Given a category `C` and morphisms `d �ṛ arr e` and `self : d ⟶ e` in `C` such that `f = d.π = e.π`, then `self.h ∘ e.π = d.π`.
|
CategoryTheory.Factorisation.ι_π
theorem CategoryTheory.Factorisation.ι_π :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
(self : CategoryTheory.Factorisation f), CategoryTheory.CategoryStruct.comp self.ι self.π = f
The theorem `CategoryTheory.Factorisation.ι_π` states that for any category `C` and any morphisms `f` from `X` to `Y` in `C`, any factorization of `f` must satisfy the factorization condition. Specifically, if we have a factorisation `self` of `f`, then the composition of the factorisation's two morphisms (`self.ι` and `self.π`) equals `f`. This is integral to the concept of factorization in category theory, where we attempt to "break down" a given morphism into a sequence of simpler ones.
More concisely: For any category `C` and morphism `f` in `C`, any factorization `self` of `f` satisfies `self.ι ∘ self.π = f`.
|