Documentation

Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful

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.

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