Documentation

Mathlib.CategoryTheory.Limits.Final.ParallelPair

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) :