Homology and exact derived functors #
An exact functor between arbitrary abelian categories commutes with canonical
derived-category homology. This is the generic comparison used by geometric
realizations such as coherent sheaves and Dqc(X).
noncomputable def
CategoryTheory.mapDerivedCategoryHomologyIso
{A : Type u}
{B : Type v}
[Category.{u_1, u} A]
[Category.{u_2, v} B]
[Abelian A]
[Abelian B]
[HasDerivedCategory A]
[HasDerivedCategory B]
(F : Functor A B)
(hadd : F.Additive)
(hlim : Limits.PreservesFiniteLimits F)
(hcolim : Limits.PreservesFiniteColimits F)
(E : DerivedCategory A)
(n : ℤ)
:
(DerivedCategory.homologyFunctor B n).obj (F.mapDerivedCategory.obj E) ≅ F.obj ((DerivedCategory.homologyFunctor A n).obj E)
Exact functors commute with homology after passage to derived categories. The isomorphism is constructed from a representative complex, the two localization comparison isomorphisms, and preservation of homology.
Equations
- One or more equations did not get rendered due to their size.