English
There is an inclusion map ι for a summand in mapBifunctor, picking out the (i1,i2,i3)-th component corresponding to a fixed j via the ρ-indexing.
Русский
Существует инклюзия ι для суммы в mapBifunctor, выделяющая (i1,i2,i3)-й компоненту, соответствующую фиксированному j через индексацию ρ.
LaTeX
$$$\\iota: (G(X) \\otimes (F(X)))_j \\to (\\text{mapBifunctor} ...)_j$$$
Lean4
/-- The inclusion of a summand in `mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄`. -/
noncomputable def ι (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ComplexShape.r c₁ c₂ c₃ c₁₂ c₄ (i₁, i₂, i₃) = j) :
(G.obj ((F₁₂.obj (K₁.X i₁)).obj (K₂.X i₂))).obj (K₃.X i₃) ⟶
(mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j :=
GradedObject.ιMapBifunctor₁₂BifunctorMapObj _ _ (ComplexShape.ρ₁₂ c₁ c₂ c₃ c₁₂ c₄) _ _ _ _ _ _ _ h
