English
Canonical isomorphism mapBifunctor K1 (K2⟦y⟧) F ≅ (mapBifunctor K1 K2 F)⟦y⟧, with signs (p*y).negOnePow on summands.
Русский
Канонический изоморфизм mapBifunctor K1 (K2⟦y⟧) F ≅ (mapBifunctor K1 K2 F)⟦y⟧ с знаками (p*y).negOnePow на уменьшаемых сумматорах.
LaTeX
$$$ mapBifunctor K_1 (K_2\llbracket y \rrbracket) F \cong (mapBifunctor K_1 K_2 F)\llbracket y \rrbracket $$$
Lean4
theorem mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso :
mapBifunctorShift₁Iso K₁ (K₂⟦y⟧) F x ≪≫ (CategoryTheory.shiftFunctor _ x).mapIso (mapBifunctorShift₂Iso K₁ K₂ F y) =
(x * y).negOnePow •
(mapBifunctorShift₂Iso (K₁⟦x⟧) K₂ F y ≪≫
(CategoryTheory.shiftFunctor _ y).mapIso (mapBifunctorShift₁Iso K₁ K₂ F x) ≪≫
(shiftFunctorComm (CochainComplex D ℤ) x y).app _) :=
by
ext1
dsimp [mapBifunctorShift₁Iso, mapBifunctorShift₂Iso]
rw [Functor.map_comp, Functor.map_comp, assoc, assoc, assoc, ←
HomologicalComplex₂.totalShift₁Iso_hom_naturality_assoc, HomologicalComplex₂.totalShift₁Iso_hom_totalShift₂Iso_hom,
← HomologicalComplex₂.totalShift₂Iso_hom_naturality_assoc, Linear.comp_units_smul, Linear.comp_units_smul,
smul_left_cancel_iff, ← HomologicalComplex₂.total.map_comp_assoc, ← HomologicalComplex₂.total.map_comp_assoc, ←
HomologicalComplex₂.total.map_comp_assoc]
congr 2
ext a b
dsimp [HomologicalComplex₂.shiftFunctor₁₂CommIso]
simp only [id_comp]
