Exact functors induce triangle functors on stable categories

An exact functor between Frobenius exact categories that preserves projective-injective objects induces a triangle functor on their stable categories, with the suspension comparison obtained from injective presentations. The essential compatibility is that the image of a connecting map, followed by this comparison, is the connecting map of the image conflation. Consequently the image of a standard conflation triangle is isomorphic to the standard triangle of the image conflation, and every distinguished triangle is preserved.

StableConflationExact.stableFunctorIsTriangulated supplies Mathlib's Functor.IsTriangulated structure for the previously constructed shift compatibility. As for the stable shift and pretriangulated structure, the Frobenius hypotheses are explicit propositions: install the resulting structures with letI.

References

• Dieter Happel, Triangulated Categories in the Representation Theory of Finite Dimensional Algebras, Chapter I, Section 2.

theorem TauCeti.StableConflationExact.stableFunctorIsTriangulated {C : Type u₁} {D : Type u₂} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasBinaryBiproducts C] [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.Preadditive D] [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasBinaryBiproducts D] {E : ExactStructure C} {E' : ExactStructure D} {F : CategoryTheory.Functor C D} [F.Additive] (hF : StableConflationExact E E' F) (hE : E.IsFrobenius) (hE' : E'.IsFrobenius) : let this := hE.stableHasShift; let this_1 := hE'.stableHasShift; have this_2 := ⋯; have this_3 := ⋯; have this_4 := hE.stablePretriangulated; have this_5 := hE'.stablePretriangulated; have this_6 := hF.stableFunctorCommShift hE hE'; (hF.stableFunctor hE).IsTriangulated

An exact functor preserving projective-injectives induces a triangle functor between Frobenius stable categories, with the shift comparison constructed from injective presentations.