Triangulated categories refactor

Stream: homology

[Joël Riou]

While working on localization of triangulated categories, I had some ideas about some refactors that would make the API more convenient:

• Namespaces: move category_theory.triangulated.pretriangulated to category_theory.pretriangulated and introduce category.triangulated for triangulated categories (i.e. pretriangulated categories which satisfy the octahedron axiom)

• Remove some unnecessary explicit parameters like for triangle.mk which is currently Π (C : Type u_2) [_inst_1 : category C] [_inst_2 : has_shift C ℤ] {X Y Z : C}, (X ⟶ Y) → (Y ⟶ Z) → (Z ⟶ (shift_functor C 1).obj X) → triangle C, where (C) should be {C}.

• Shift functors are automatically additive. Currently, working with triangulated categories requires the following variables:
  variables {C : Type*} [category C] [preadditive C] [has_zero_object C] [has_shift C ℤ] [∀ (n : ℤ), functor.additive (shift_functor C n)] [pretriangulated C]
  The assumption that the shift functors are additive could be removed, if one observes that they are equivalences of categories (automatic because the shift is indexed by the group ℤ), and that an equivalence of categories between preadditive categories is additive (this is not yet in mathlib?).

• Triangulated functors:

  • Currently, the commutation with the shift is stated only for ⟦1⟧: it should be stated for all ⟦n⟧, n : ℤ with some coherence properties. (I have draft code which shows that the datum of a series of such isos is equivalent to the datum of the commutation with ⟦1⟧.)
  • The definition of triangulated is currently bundled. This is obviously ok for the definition of the category of triangulated functors between two pretriangulated categories, but I would think it would be more convenient to consider them as ordinary functors F : C ⥤ D with a class instance [functor.triangulated F] which would say that for a certain series of commutation iso with the shift, F preserves distinguished triangles.

Any comments about these possible changes?

[Andrew Yang]

equivalence of categories between preadditive categories is additive

Is this true? Over a category with a single object, this seems to suggest that multiplicative morphisms between rings are automatically ring homomorphisms.

[Joël Riou]

Andrew Yang said:

equivalence of categories between preadditive categories is additive

Is this true? Over a category with a single object, this seems to suggest that multiplicative morphisms between rings are automatically ring homomorphisms.

Ah, I have forgotten to say that pretriangulated categories have finite coproducts. A better suggestion would be to assume [has_finite_biproducts C] instead of requiring that shift functors are additive. (I do not think that there is any case where checking the existence of finite biproducts would be harder than verifying that shift functors are additive.)