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 : ℤ)
:
The canonical isomorphism
DerivedCateogry.singleFunctor C n ⋙ DerivedCateogry.homologyFunctor C n ≅ 𝟭 C
Equations
- One or more equations did not get rendered due to their size.
Instances For
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