Transporting a triangulation along an equivalence

An equivalence of categories F : C ⥤ D is a localization functor for the class of isomorphisms of C. This class admits a left calculus of fractions, and, when C is pretriangulated, it is compatible with the triangulation. Consequently Mathlib's construction CategoryTheory.Triangulated.Localization.pretriangulated applies to F: if D carries a shift by ℤ for which F commutes with the shifts, then D is pretriangulated, with distinguished triangles the triangles isomorphic to images of distinguished triangles of C, F is a triangle functor, and D is triangulated as soon as C is (CategoryTheory.Triangulated.Localization.isTriangulated).

This is the transport used for homotopy categories that are identified with the stable category of a Frobenius exact category: Happel's triangulation of the stable category is transported along the identification, after the shift of the homotopy category has been matched with stable suspension.

Main results

• TauCeti.instHasLeftCalculusOfFractionsIsomorphisms: the isomorphisms admit a left calculus of fractions.
• TauCeti.instIsCompatibleWithShiftIsomorphisms: the isomorphisms are compatible with every shift by an additive group.
• TauCeti.instIsCompatibleWithTriangulationIsomorphisms: in a pretriangulated category, the isomorphisms are compatible with the triangulation.
• TauCeti.instIsLocalizationIsomorphisms: an equivalence is a localization functor for the isomorphisms of its source.

instance TauCeti.instHasLeftCalculusOfFractionsIsomorphisms {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] : (CategoryTheory.MorphismProperty.isomorphisms C).HasLeftCalculusOfFractions

The isomorphisms of a category admit a left calculus of fractions: a right fraction s⁻¹ ≫ f with s an isomorphism is the left fraction (inv s ≫ f) ≫ (𝟙)⁻¹.

instance TauCeti.instIsLocalizationIsomorphisms {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2} [CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.IsEquivalence] : F.IsLocalization (CategoryTheory.MorphismProperty.isomorphisms C)

An equivalence of categories is a localization functor for the isomorphisms of its source.

instance TauCeti.instIsCompatibleWithShiftIsomorphisms {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] (A : Type u_2) [AddGroup A] [CategoryTheory.HasShift C A] : (CategoryTheory.MorphismProperty.isomorphisms C).IsCompatibleWithShift A

The isomorphisms of a category are compatible with every shift by an additive group: a morphism is an isomorphism exactly when its shift is.

instance TauCeti.instIsCompatibleWithTriangulationIsomorphisms {C : Type u_1} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.HasShift C ℤ] [CategoryTheory.Preadditive C] [CategoryTheory.Limits.HasZeroObject C] [∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [CategoryTheory.Pretriangulated C] : (CategoryTheory.MorphismProperty.isomorphisms C).IsCompatibleWithTriangulation

In a pretriangulated category, the isomorphisms are compatible with the triangulation: a morphism of distinguished triangles whose first two components are isomorphisms can be completed by an isomorphism.