Generators in triangulated categories

Stream: mathlib4

[Justus Springer]

So I would like to formalise the definition of strong and classical generators in triangulated categories (stacks#09SJ). This needs the closure operators $\langle E \rangle_n$ of an object $E$ (or more generally for mathlib, of any ObjectProperty), which in turn are defined using the following four closure operators in triangulated categories, see stacks#0FX0:

1. The closure under taking shifts, which stacks denotes as $E[-\infty, \infty]$. I already added this to mathlib in #35079.

2. The closure under taking finite sums, which stacks denotes as $add$. This should be a special case of docs#CategoryTheory.ObjectProperty.limitsClosure.

3. The closure under taking summands, which stacks denotes as $smd$. The corresponding predicate is what stacks calls "saturated" (stacks#05RB) but "thick" also seems to be a common name. I couldn't find anything like this in mathlib (?). I guess, a more general approach would be to define a sort of inverse of limitsClosure, saying that if a direct limit $\lim_i D_i$ of some shape satisfies $P$, then all the $D_i$ satisfy $P$.

4. The closure under taking cones, which stacks denotes as $\mathcal{A} \star \mathcal{B}$. We have the predicate docs#CategoryTheory.ObjectProperty.IsTriangulatedClosed₂, which is very close, but I think I would need a generalization of that allowing different object properties on the different vertices of the triangle, and then define the corresponding closure operator, taking in two object properties and producing a third. We also have docs#CategoryTheory.ObjectProperty.IsTriangulated, which is a combination of 4. and 1.

To the experts in triangulated categories (which I am not), does this sound like a reasonable plan? And would mathlib even want this, or is it too niche?

[Johan Commelin]

cc @Joël Riou

[Matthew Ballard]

This is something I am interested in seeing in the library and it is nice someone has the bandwidth to tackle it. I think one could make contact with Inventiones level math pretty quickly here.

Some comments:

• Nothing said mentioned nwhich to me is the most important piece of information
• In my limited thought experiments, I don't see anything better than an custom inductive, along the lines of what limitsClosure is doing

[Justus Springer]

The definition of strong generator mentions n. The individual closure operators listed don't, of course.

[Justus Springer]

Yes, my motivation is actually to make contact with Annals level math :)

[Matthew Ballard]

That is much further away but a very good goal.

[Matthew Ballard]

I don't know of a reasonable definition of a classical generator (in general, in this flavor) that doesn't go through n-step generation

[Matthew Ballard]

Another good target (given the requisite geometry) is https://www.sciencedirect.com/science/article/abs/pii/S0021782423000612

[Matthew Ballard]

I assume we want GAGA

[Matthew Ballard]

Other comments:

• thick is indeed the "standard" terminology but I can imagine versions where you don't want to impose this on each step
• similarly Neeman (in the referenced paper) constrains the shifts allowed
• I don't think there is any world we don't want it closed under isomorphisms
• the above suggests having a very flexible definition that can be specialized to the usual definition of nth level
• I think we already have the Karoubi closure as a reference point

[Matthew Ballard]

Ideally I would like decide to work ;)

[Matthew Ballard]

You will of course want the "big" version where you use coproducts of a given size, beyond finite.

I am not sure of the value of closure under other colimit shapes generally in this setting. I am not sure anyone has really thought about it. Certainly it is something you want more generally though.

[Joël Riou]

I think it would be nice to have these constructions. (For triangulated categories, I believe that the only (co)limits which are relevant are coproducts and products.)
On a related topic, at some point, I will upstream definitions about left/right localizing triangulated subcategories.

[Matthew Ballard]

Yes, you don't get a lot for free in a general triangulated category

[Justus Springer]

I just opened #35497, which defines the extension product $\mathcal{A} \star \mathcal{B}$ of two object properties in a triangulated category and proves associativity.