The fully faithful embedding of the abelian category in its derived category

In this file, we show that for any n : ℤ, the functor singleFunctor C n : C ⥤ DerivedCategory C is fully faithful.

noncomputable def DerivedCategory.singleFunctorCompHomologyFunctorIso (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctor C n).comp (homologyFunctor C n) ≅ CategoryTheory.Functor.id C

The canonical isomorphism DerivedCategory.singleFunctor C n ⋙ DerivedCategory.homologyFunctor C n ≅ 𝟭 C

Equations

• One or more equations did not get rendered due to their size.

instance DerivedCategory.instFaithfulSingleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctor C n).Faithful

instance DerivedCategory.instFullSingleFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [HasDerivedCategory C] (n : ℤ) : (singleFunctor C n).Full