English
Let F₁₂ and G be bifunctors and ρ₁₂ a data specifying their action on indices, with graded objects X₁, X₂, X₃. The action of composing the two bifunctors on graded objects is canonically isomorphic to the sequential action: mapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅ mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃.
Русский
Пусть тождественные бифункторы F₁₂ и G образуют трифункор; для градуированных объектов X₁, X₂, X₃ и индексных данных ρ₁₂ существует естественный изоморфизм между действием композиции бифункторов и последовательным действием: mapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅ mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃.
LaTeX
$$$$\mathrm{mapTrifunctorMapObj}(\mathrm{bifunctorComp}_{12} F_{12} G)\; r\; X_1\; X_2\; X_3 \; \cong\; \mathrm{mapBifunctorMapObj}\, G\, \rho_{12}.q\big( \mathrm{mapBifunctorMapObj}\, F_{12}\, \rho_{12}.p\; X_1\; X_2 \big)\; X_3.$$$$
Lean4
/-- The action on graded objects of a trifunctor obtained by composition of two
bifunctors can be computed as a composition of the actions of these two bifunctors. -/
noncomputable def mapBifunctorComp₁₂MapObjIso :
mapTrifunctorMapObj (bifunctorComp₁₂ F₁₂ G) r X₁ X₂ X₃ ≅
mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ :=
isoMk _ _ (fun j => (CofanMapObjFun.iso (isColimitCofan₃MapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ j)).symm)
