rightDerivedToHomotopyCategory — Mathlib

English

There is a canonical isomorphism between F.rightDerivedToHomotopyCategory.obj X and the image under F of the injective resolution cocomplex, i.e., the isomorphism with the mapped cocomplex as described.

Русский

Существует каноническое изоморфизм между F.rightDerivedToHomotopyCategory.obj X и отображением F когомологического разрешения, т.е. изоморфизм с отображенным кокомологическим комплексом.

LaTeX

$$$F^{\\mathrm{rightDerivedToHomotopyCategory}}(X) \\cong (F\\circ \\text{mapHomologicalComplex})(I.cocomplex)$$$

Lean4

/-- When `F : C ⥤ D` is an additive functor, this is
the functor `C ⥤ HomotopyCategory D (ComplexShape.up ℕ)` which
sends `X : C` to `F` applied to an injective resolution of `X`. -/
noncomputable def rightDerivedToHomotopyCategory (F : C ⥤ D) [F.Additive] :
    C ⥤ HomotopyCategory D (ComplexShape.up ℕ) :=
  injectiveResolutions C ⋙ F.mapHomotopyCategory _

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