Conditions for parallelPair to be initial #
In this file we give sufficient conditions on a category C and parallel morphisms f g : X ⟶ Y
in C so that parallelPair f g becomes an initial functor.
The conditions are that there is a morphism out of X to every object of C and that any two
parallel morphisms out of X factor through the parallel pair f, g
(h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z), ∃ (a : Y ⟶ Z), i = f ≫ a ∧ j = g ≫ a).
theorem
CategoryTheory.Limits.parallelPair_initial_mk'
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(h₁ : ∀ (Z : C), Nonempty (X ⟶ Z))
(h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
CategoryTheory.Zigzag (CategoryTheory.CostructuredArrow.mk i) (CategoryTheory.CostructuredArrow.mk j))
:
theorem
CategoryTheory.Limits.parallelPair_initial_mk
{C : Type u_1}
[CategoryTheory.Category.{u_2, u_1} C]
{X : C}
{Y : C}
(f : X ⟶ Y)
(g : X ⟶ Y)
(h₁ : ∀ (Z : C), Nonempty (X ⟶ Z))
(h₂ : ∀ ⦃Z : C⦄ (i j : X ⟶ Z),
∃ (a : Y ⟶ Z), i = CategoryTheory.CategoryStruct.comp f a ∧ j = CategoryTheory.CategoryStruct.comp g a)
: