English
Another commutation shift instance for mapDerivedCategory with integer shifts.
Русский
Ещё один экземпляр коммутируемого сдвига для mapDerivedCategory с целочисленным сдвигом.
LaTeX
$$$F.mapDerivedCategory.CommShift\ Int$$$
Lean4
instance : NatTrans.CommShift F.mapDerivedCategoryFactors.hom ℤ :=
NatTrans.CommShift.verticalComposition (DerivedCategory.quotientCompQhIso C₁).inv
(DerivedCategory.quotientCompQhIso C₂).hom (F.mapHomotopyCategoryFactors (ComplexShape.up ℤ)).hom
F.mapDerivedCategoryFactorsh.hom F.mapDerivedCategoryFactors.hom ℤ
(by
ext K
dsimp
simp only [id_comp, mapDerivedCategoryFactorsh_hom_app, assoc, comp_id, ← Functor.map_comp_assoc,
Iso.inv_hom_id_app, map_id, comp_obj])
