Theorems · Theorem · category theory

CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.hom_ext

∀ {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {c₁ : CategoryTheory.Limits.CokernelCofork f₁} (hc₁ : CategoryTheory.Limits.IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂}
  {c₂ : CategoryTheory.Limits.CokernelCofork f₂} (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms]
  [F.PreservesZeroMorphisms]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₂ 0) (F.obj c₁.pt)]
  [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f₁ 0) (F.flip.obj Y₂)] {T : C}
  {f g : (F.obj c₁.pt).obj c₂.pt ⟶ T},
  CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂)
        (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) f) =
      CategoryTheory.CategoryStruct.comp ((F.map (CategoryTheory.Limits.Cofork.π c₁)).app Y₂)
        (CategoryTheory.CategoryStruct.comp ((F.obj c₁.pt).map (CategoryTheory.Limits.Cofork.π c₂)) g) →
    f = g

Defined in

Mathlib.CategoryTheory.Limits.Preserves.BifunctorCokernel

Cited by

0 results in Mathlib

Foundations

Depth 38 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Limits.HasZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Functor.PreservesZeroMorphismsCategoryTheory.Limits.PreservesColimitCategoryTheory.Limits.PreservesColimit