instCommShiftDerivedCategoryMapDerivedCategoryInt

English

There is an instance of a commuting shift structure on mapDerivedCategory for the integer group.

Русский

Существует экземпляр коммутируемого сдвига для mapDerivedCategory над целыми.

LaTeX

$$$F.mapDerivedCategory.CommShift\ \mathbb{Z}$$$

Lean4

noncomputable instance : F.mapDerivedCategory.CommShift ℤ :=
  Functor.commShiftOfLocalization DerivedCategory.Qh (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ)) ℤ
    (F.mapHomotopyCategory _ ⋙ DerivedCategory.Qh) F.mapDerivedCategory

Похожие утверждения