English
The inclusion ιMapBifunctor identifies a summand of the total cochain complex corresponding to the factors F, K1, K2 inside the mapBifunctor construction.
Русский
Инклюзия ιMapBifunctor выделяет сомножитель в общем суммарном коцепном комплексе, соответствующий отображению F и комплексам K1, K2 внутри построения mapBifunctor.
LaTeX
$$$\iota\mathrm{MapBifunctor}_{K_1 K_2 F} = \text{incl of summand } (F.obj (K_1.X n_1)).obj (K_2.X n_2) ⇢ (\mathrm{mapBifunctor} K_1 K_2 F).X n$$$
Lean4
/-- Given `K₁ : CochainComplex C₁ ℤ`, `K₂ : CochainComplex C₂ ℤ`,
a bifunctor `F : C₁ ⥤ C₂ ⥤ D`, this `mapBifunctor K₁ K₂ F : CochainComplex D ℤ`
is the total complex of the bicomplex obtained by applying `F` to `K₁` and `K₂`. -/
noncomputable abbrev mapBifunctor [HasMapBifunctor K₁ K₂ F] : CochainComplex D ℤ :=
HomologicalComplex.mapBifunctor K₁ K₂ F (ComplexShape.up ℤ)
