Zulip Chat Archive
Stream: homology
Topic: Triangulated categories refactor
Joël Riou (Oct 12 2022 at 08:05):
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
tocategory_theory.pretriangulated
and introducecategory.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.
 Currently, the commutation with the shift is stated only for
Any comments about these possible changes?
Andrew Yang (Oct 12 2022 at 08:08):
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 (Oct 12 2022 at 08:29):
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.)
Last updated: Aug 03 2023 at 10:10 UTC