English
If K1 and K2 have colimits and G preserves the two-variable colimit, then the uncurried whiskering construction has a colimit.
Русский
Если K1 и K2 имеют колимиты и G сохраняет двухпеременную колимиту, то укурри конструкция имеет колимит.
LaTeX
$$$[HasColimit K1] \\wedge [HasColimit K2] \\wedge [PreservesColimit₂ K1 K2 G] \\Rightarrow HasColimit (uncurry.obj (whiskeringLeft₂ C |>.obj K1 |>.obj K2 |>.obj G))$$$
Lean4
/-- Given a bifunctor `G : C₁ ⥤ C₂ ⥤ C`, diagrams `K₁ : J₁ ⥤ C₁` and `K₂ : J₂ ⥤ C₂`, and cocones
over these diagrams, `G.mapCocone₂ c₁ c₂` is the cocone over the diagram `J₁ × J₂ ⥤ C` obtained
by applying `G` to both `c₁` and `c₂`. -/
@[simps!]
def mapCocone₂ (G : C₁ ⥤ C₂ ⥤ C) {K₁ : J₁ ⥤ C₁} {K₂ : J₂ ⥤ C₂} (c₁ : Cocone K₁) (c₂ : Cocone K₂) :
Cocone <| uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G)
where
pt := (G.obj c₁.pt).obj c₂.pt
ι :=
{ app := fun ⟨j₁, j₂⟩ ↦ (G.map <| c₁.ι.app j₁).app _ ≫ (G.obj _).map (c₂.ι.app j₂)
naturality := by
rintro ⟨j₁, j₂⟩ ⟨k₁, k₂⟩ ⟨f₁, f₂⟩
dsimp
simp only [assoc, comp_id, NatTrans.naturality_assoc, ← Functor.map_comp, NatTrans.naturality, const_obj_map,
const_obj_obj, ← NatTrans.comp_app_assoc, c₁.w] }
