mapDerivedCategoryFactorsh — Mathlib

English

There is an isomorphism between Qh ∘ F.mapDerivedCategory and F.mapHomotopyCategory ∘ Qh.

Русский

Существует изоморфизм между Qh ∘ F.mapDerivedCategory и F.mapHomotopyCategory ∘ Qh.

LaTeX

$$$\mathrm{Qh} \circ F.mapDerivedCategory \cong F.mapHomotopyCategory(\text{ComplexShape.up }\mathbb{Z}) \circ \mathrm{Qh}$$$

Lean4

/-- The functor `F.mapDerivedCategory` is induced
by `F.mapHomotopyCategory (ComplexShape.up ℤ)`. -/
noncomputable def mapDerivedCategoryFactorsh :
    DerivedCategory.Qh ⋙ F.mapDerivedCategory ≅ F.mapHomotopyCategory (ComplexShape.up ℤ) ⋙ DerivedCategory.Qh :=
  F.mapHomologicalComplexUpToQuasiIsoFactorsh _

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