Serre functors as triangulated autoequivalences #
When a Serre functor is an equivalence, its additive, signed shift, and exact
structures supply the bundled GroupAction.TriEquiv used by the stability
action. This adapter lives with that consumer so the generic Serre theory does
not import the stability-condition tree.
noncomputable def
CategoryTheory.SerreFunctor.SerreFunctorData.toTriEquiv
{k : Type w}
[Field k]
{C : Type u}
[Category.{v, u} C]
[Preadditive C]
[Linear k C]
[Limits.HasZeroObject C]
[HasShift C ℤ]
[∀ (n : ℤ), (shiftFunctor C n).Additive]
[∀ (n : ℤ), Functor.Linear k (shiftFunctor C n)]
[Pretriangulated C]
(D : SerreFunctorData k C)
[D.S.IsEquivalence]
:
Bundle the Serre autoequivalence with its proved additive, signed shift, and triangulated structures. Equivalence is a separate hypothesis, supplied for example by Serre data with a co-Serre witness.
Equations
- D.toTriEquiv = { e := D.S.asEquivalence, fAdd := ⋯, iAdd := ⋯, fCS := inferInstance, iCS := inferInstance, fTri := ⋯, iTri := ⋯ }