Exactness of the Serre functor #
The signed shift comparison gives the rotation boundary for the image of a
distinguished triangle. Complete that boundary to a distinguished triangle,
then use Serre duality and the exact Hom sequences to identify its middle
object with the Serre image. The resulting SerreFunctorData.isTriangulated
requires no equivalence or Hom-finiteness hypothesis.
This file uses an arbitrary distinguished completion. It does not postulate the image triangle as distinguished.
theorem
CategoryTheory.SerreFunctor.SerreFunctorData.isTriangulated
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)]
[Limits.HasZeroObject C]
[Pretriangulated C]
(D : SerreFunctorData k C)
:
The Serre functor preserves distinguished triangles with the signed shift comparison. This does not require it to be an equivalence.