English
For mapBifunctor₂₃, the third differential decomposes as a sum of three components D1, D2, D3.
Русский
Для mapBifunctor₂₃ третьий дифференциал раскладывается на три компонента D1, D2, D3.
LaTeX
$$$\bigl(mapBifunctor K_1 (mapBifunctor K_2 K_3 G_{2 3} c_{2 3}) F c_4\bigr).d j j' = D_1 F G_{2 3} K_1 K_2 K_3 c_{2 3} c_4 j j' + D_2 F G_{2 3} K_1 K_2 K_3 c_{1 2} c_{2 3} c_4 j j' + D_3 F G_{2 3} K_1 K_2 K_3 c_{1 2} c_{2 3} c_4 j j'$$$
Lean4
/-- The inclusion of a summand `(F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n`
of the total cochain complex when `n₁ + n₂ = n`. -/
noncomputable abbrev ιMapBifunctor [HasMapBifunctor K₁ K₂ F] (n₁ n₂ n : ℤ) (h : n₁ + n₂ = n) :
(F.obj (K₁.X n₁)).obj (K₂.X n₂) ⟶ (mapBifunctor K₁ K₂ F).X n :=
HomologicalComplex.ιMapBifunctor K₁ K₂ F _ _ _ _ h
