mapDerivedCategoryFactors — Mathlib

English

There is a canonical isomorphism between composing Q with mapDerivedCategory and composing mapHomologicalComplex with Q.

Русский

Существует каноническое изоморфизм между Q ∘ mapDerivedCategory и mapHomologicalComplex( up ℤ ) ∘ Q.

LaTeX

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

Lean4

/-- The functor `F.mapDerivedCategory` is induced
by `F.mapHomologicalComplex (ComplexShape.up ℤ)`. -/
noncomputable def mapDerivedCategoryFactors :
    DerivedCategory.Q ⋙ F.mapDerivedCategory ≅ F.mapHomologicalComplex (ComplexShape.up ℤ) ⋙ DerivedCategory.Q :=
  F.mapHomologicalComplexUpToQuasiIsoFactors _

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