English
There is a canonical isomorphism between the colimit of the uncurry construction and the iterated application of G to the colimits of K1 and K2.
Русский
Существует каноническое изоморфизм между колимитом конструкции uncurry и повторным применением G к колимитам K1 и K2.
LaTeX
$$$\\mathrm{colimit}(\\text{uncurry}(\\dots)) \\cong G(\\mathrm{colimit}(K1)) \\otimes \\mathrm{colimit}(K2)$$$
Lean4
/-- Given a bifunctor `G : C₁ ⥤ C₂ ⥤ C`, diagrams `K₁ : J₁ ⥤ C₁` and `K₂ : J₂ ⥤ C₂`, and cones
over these diagrams, `G.mapCone₂ c₁ c₂` is the cone over the diagram `J₁ × J₂ ⥤ C` obtained
by applying `G` to both `c₁` and `c₂`. -/
@[simps!]
def mapCone₂ (G : C₁ ⥤ C₂ ⥤ C) {K₁ : J₁ ⥤ C₁} {K₂ : J₂ ⥤ C₂} (c₁ : Cone K₁) (c₂ : Cone K₂) :
Cone <| 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, id_comp, NatTrans.naturality_assoc, ← Functor.map_comp, ← NatTrans.comp_app_assoc, c₁.w,
c₂.w] }
