English
There is a canonical morphism between the two ways of mapping graded objects via the composition of bifunctors, and its composite with the iso hom component coincides with the direct action built from the two-step mapping.
Русский
Существует каноническое отображение между двумя способами отображения градуированных объектов с помощью композиции бифункторов, и композиция этого отображения с компонентой гомоморфа-изоморфизма совпадает с прямым действием, получаемым по двум последовательным шагам.
LaTeX
$$$$ιMapTrifunctorMapObj(\mathrm{bifunctorComp}_{12} F_{12} G)\; r X_1 X_2 X_3 i_1 i_2 i_3 j h \; \circ \; (\mathrm{mapBifunctorComp}_{12}\mathrm{MapObjIso} F_{12} G\;\rho_{12} X_1 X_2 X_3).\mathrm{hom} \, j = ιMapBifunctor₁₂BifunctorMapObj F_{12} G_{?} \; X_1 X_2 X_3 i_1 i_2 i_3 j h$$
Lean4
@[reassoc (attr := simp)]
theorem ι_mapBifunctorComp₁₂MapObjIso_hom (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (j : J) (h : r (i₁, i₂, i₃) = j) :
ιMapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ i₁ i₂ i₃ j h ≫
(mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).hom j =
ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j h :=
by
dsimp [mapBifunctorComp₁₂MapObjIso]
apply CofanMapObjFun.ιMapObj_iso_inv
