Action of bifunctors on cokernels

Let c₁ (resp. c₂) be a cokernel cofork for a morphism f₁ : X₁ ⟶ Y₁ in a category C₁ (resp. f₂ : X₂ ⟶ Y₂ in C₂). Given a bifunctor F : C₁ ⥤ C₂ ⥤ C, we construct a cokernel cofork with point (F.obj c₁.pt).obj c₂.pt for the obvious morphism (F.obj X₁).obj Y₂ ⨿ (F.obj Y₁).obj X₂ ⟶ (F.obj Y₁).obj Y₂, and show that it is a colimit when both coforks are colimit, the cokernel of f₁ is preserved by F.obj c₁.pt and the cokernel of f₂ is preserved by F.flip.obj X₁ and F.flip.obj Y₁.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.CokernelCofork.mapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C] [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} (c₁ : CokernelCofork f₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} (c₂ : CokernelCofork f₂) (F : Functor C₁ (Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))

Let c₁ (resp. c₂) be a cokernel cofork for a morphism f₁ : X₁ ⟶ Y₁ in a category C₁ (resp. f₂ : X₂ ⟶ Y₂ in C₂). Given a bifunctor F : C₁ ⥤ C₂ ⥤ C, this is the cokernel cofork with point (F.obj c₁.pt).obj c₂.pt for the obvious morphism (F.obj X₁).obj Y₂ ⨿ (F.obj Y₁).obj X₂ ⟶ (F.obj Y₁).obj Y₂.

Equations

• One or more equations did not get rendered due to their size.

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

theorem CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor.exists_desc {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C] [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CokernelCofork f₁} (hc₁ : IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CokernelCofork f₂} (hc₂ : IsColimit c₂) (F : Functor C₁ (Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)] [PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)] [HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] [PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)] (s : CokernelCofork (coprod.desc ((F.map f₁).app Y₂) ((F.obj Y₁).map f₂))) : ∃ (l : (F.obj c₁.pt).obj c₂.pt ⟶ s.pt), CategoryStruct.comp ((F.map (Cofork.π c₁)).app Y₂) (CategoryStruct.comp ((F.obj c₁.pt).map (Cofork.π c₂)) l) = Cofork.π s

noncomputable def CategoryTheory.Limits.CokernelCofork.isColimitMapBifunctor {C₁ : Type u_1} {C₂ : Type u_2} {C : Type u_3} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C] [HasZeroMorphisms C₁] [HasZeroMorphisms C₂] [HasZeroMorphisms C] {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁} {c₁ : CokernelCofork f₁} (hc₁ : IsColimit c₁) {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {c₂ : CokernelCofork f₂} (hc₂ : IsColimit c₂) (F : Functor C₁ (Functor C₂ C)) [(F.obj c₁.pt).PreservesZeroMorphisms] [F.PreservesZeroMorphisms] [PreservesColimit (parallelPair f₂ 0) (F.obj c₁.pt)] [PreservesColimit (parallelPair f₁ 0) (F.flip.obj Y₂)] [HasBinaryCoproduct ((F.obj X₁).obj Y₂) ((F.obj Y₁).obj X₂)] [PreservesColimit (parallelPair f₁ 0) (F.flip.obj X₂)] : IsColimit (c₁.mapBifunctor c₂ F)

Let c₁ (resp. c₂) be a colimit cokernel cofork for a morphism f₁ : X₁ ⟶ Y₁ in a category C₁ (resp. f₂ : X₂ ⟶ Y₂ in C₂). If F : C₁ ⥤ C₂ ⥤ C is a bifunctor, then (F.obj c₁.pt).obj c₂.pt identifies to the cokernel of the morphism (F.obj X₁).obj Y₂ ⨿ (F.obj Y₁).obj X₂ ⟶ (F.obj Y₁).obj Y₂ when the cokernel of f₁ is preserved by F.obj c₁.pt and the cokernel of f₂ is preserved by F.flip.obj X₁ and F.flip.obj Y₁.

Equations

• One or more equations did not get rendered due to their size.