English
There is a canonical isomorphism between shifting the first argument inside a mapBifunctor and shifting the target of mapBifunctor itself; signs do not appear in this isomorphism.
Русский
Существует каноническая изоморфия между сдвигом первого аргумента внутри отображения mapBifunctor и смещением самого результата mapBifunctor; знаки здесь не участвуют.
LaTeX
$$$ mapBifunctor (K_1\langle x\rangle) K_2 F \cong (mapBifunctor K_1 K_2 F)\langle x\rangle. $$$
Lean4
/-- The canonical isomorphism `mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧`.
This isomorphism does not involve signs. -/
noncomputable def mapBifunctorShift₁Iso : mapBifunctor (K₁⟦x⟧) K₂ F ≅ (mapBifunctor K₁ K₂ F)⟦x⟧ :=
HomologicalComplex₂.total.mapIso (mapBifunctorHomologicalComplexShift₁Iso K₁ K₂ F x) _ ≪≫
(((F.mapBifunctorHomologicalComplex _ _).obj K₁).obj K₂).totalShift₁Iso x
