English
The inverse of the canonical isomorphism between the two ways of mapping via composed bifunctors is given by the corresponding universal property mapping obtained from the colimit cocone.
Русский
Обратный к каноническому изоморфизму между двумя способами отображения через композицию бифункторов задаётся соответствующим отображением, получаемым из универсального свойства кокона диаграммы сопряжённости с пределом.
LaTeX
$$$$ιMapBifunctor₁₂BifunctorMapObj F G ρ X_1 X_2 X_3 i_1 i_2 i_3 j h \; \circ \; (\mathrm{mapBifunctorComp}_{12}\mathrm{MapObjIso} F G ρ X_1 X_2 X_3).\mathrm{inv} \; j = ιMapTrifunctorMapObj(\mathrm{bifunctorComp}_{12} F G) r X_1 X_2 X_3 i_1 i_2 i_3 j h.$$$
Lean4
@[reassoc (attr := simp)]
theorem ι_mapBifunctorComp₁₂MapObjIso_inv (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
(mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).inv j =
ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h :=
CofanMapObjFun.inj_iso_hom (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j) _ h
