English
The cofan consisting of the inclusions given by ιMapBifunctorMapObj exists for the triple of graded objects X1, X2, X3, and the index data ρ1₂; it is the canonical cocone obtained by composing the bifunctor X1 ⟶ X2 to C ⥤, then mapping X3 via G, in the setting of the triple trifunctor.
Русский
Существование кофана, состоящего из инклюзий, заданных ιMapBifunctorMapObj, для тройки градационных объектов X1, X2, X3 и данных индекса ρ1₂; это канонический кокон, получаемый путем композиции бифункторов X1 ⟶ X2, затем отображения X3 через G, в контексте трифункторного построения.
LaTeX
$$$\text{cofan}_{3}(\text{MapBifunctor}_{1 2} F, G, ρ_1 2, X_1, X_2, X_3, r)\;: $$
Lean4
/-- The cofan consisting of the inclusions given by `ιMapBifunctor₁₂BifunctorMapObj`. -/
noncomputable def cofan₃MapBifunctor₁₂BifunctorMapObj (j : J) :
((((mapTrifunctor (bifunctorComp₁₂ F₁₂ G) I₁ I₂ I₃).obj X₁).obj X₂).obj X₃).CofanMapObjFun r j :=
Cofan.mk (mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ j)
(fun ⟨⟨i₁, i₂, i₃⟩, (hi : r ⟨i₁, i₂, i₃⟩ = j)⟩ => ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i₁ i₂ i₃ j hi)
