triangles and shifts

Stream: condensed mathematics

[Johan Commelin]

I have been thinking more about triangles and shifts. I think it's going to be really annoying that $X[1][-1]$ is not equal to $X$. It's not just that they aren't defeq, they aren't even equal, in a generic category with shifts.
And with the approach in the literature, these shifts are all over the place when you work with triangles.

Usually, we solve these sorts of issues using characteristic predicates, redundant data, forgetful inheritance, you name it. But these techniques don't seem to work this time. If someone has ideas on how to design triangulated categories with an agile UX, please contribute!

[Julian Külshammer]

Do you consider the axiomatization of triangulated category where [1] is an equivalence or an automorphism? Would it help to switch to the other one, or have both around and sometimes switch between the two?

[Johan Commelin]

@Julian Külshammer Yes, I've thought about it a bit. But I fear that the "switching between the two" might be painful. Currently, we don't have isomorphisms of categories. So it would probably mean a lot of duplication of APIs.

[Johan Commelin]

Also, are there natural examples where the shift is not an honest automorphism? Probably there are such examples in algebraic topology?

[Julian Külshammer]

The stable module category of a group algebra (or more generally a selfinjective algebra) should be an example. But there is some strictification result. I of course have no idea how annoying it would be to use this.

[Julian Külshammer]

What is the solution for monoidal and strict monoidal categories?

[Johan Commelin]

@Scott Morrison I guess you know :this: best?

[Scott Morrison]

@Markus Himmel and @Bhavik Mehta are actually the people to ask. There was a branch which doesn't seem to have ever reached PR status, which I can try to find. There is a proof of the coherence result for monoidal categories out there on a branch.

[Scott Morrison]

But actually making strictification into something that makes your life pleasant(er) is something that requires tactic support: the mere fact that you can change to an equivalent strict monoidal category doesn't seem to be helpful in practice.

[Scott Morrison]

The most recent thread about this is at https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/rigid.20.28autonomous.29.20categories

[Yaël Dillies]

The branch is called Mon_something, I think. There are a handful of them called like that.

[Reid Barton]

Johan Commelin said:

Also, are there natural examples where the shift is not an honest automorphism? Probably there are such examples in algebraic topology?

For an algebraic topologist the situation is the opposite--the shift is not even extra data, it is determined by the structure of the underlying $\infty$-category

[Reid Barton]

So then you can apply your characteristic predicate style technology

[Johan Commelin]

Right, I had this vague sense that $∞$-cats provide a different way to tackle this problem.
But I also have the vague sense that doing $∞$-cats in Lean will be a pretty massive undertaking.

[Reid Barton]

Right, I don't think this is a helpful path forward, but maybe helpful for context to why you are in this situation

[Reid Barton]

In short, passing to the homotopy category discarded the information you need to characterize $A[1]$ in terms of $A$ in the same sort of way that you can still characterize, say, $A \oplus A$ in terms of $A$

[Johan Commelin]

Do you have suggestions for how to get the triangles mentioned here https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/breen.20deligne.20lemma into Lean as smoothly as possible?

[Matthew Ballard]

What is a “generic category with a shift”? Just a pair $(\mathcal C, S)$ with $\mathcal C$ a category and $S: \mathcal C \to \mathcal C$ an auto-equivalence?

[Matthew Ballard]

There exists un-enhancable triangulated categories so homotopy category of stable $\infty$-category only goes so far.

[Matthew Ballard]

(The usual approach to these in some circles: “Abomination! Lock them in cellar with Sloth!”)

[Johan Commelin]

Are there examples of such un-enhancable triangulated cats that you meet in the wild? I guess not, right? Everything we care about in practice also has an infty-cat version.

[Matthew Ballard]

Johan Commelin said:

Are there examples of such un-enhancable triangulated cats that you meet in the wild? I guess not, right? Everything we care about in practice also has an infty-cat version.

Poor Sloth

[Matthew Ballard]

Short answer: you glue along an un-enhancable functor. Rizzardo and Van den Bergh’s method involves studying $A_n$ structures that don’t lift all the way to $A_\infty$ ones. That idea in and of itself is very interesting.

[Matthew Ballard]

There should be a family of structures that interpolates between plain triangulated categories and homotopy categories.

[Matthew Ballard]

There may already be. I’d have to ask Siri.

[Reid Barton]

Matthew Ballard said:

(The usual approach to these in some circles: “Abomination! Lock them in cellar with Sloth!”)

Well, I would put this position a bit differently. It's not that the homotopy categories of stable $\infty$-categories are good, and the triangulated categories that don't arise this way are bad. Rather, if you start with a stable $\infty$-category, then you shouldn't be discarding the higher information by forming the homotopy category in the first place.

[Reid Barton]

But maybe this is getting too far off topic.

[Matthew Ballard]

Reid Barton said:

Matthew Ballard said:

(The usual approach to these in some circles: “Abomination! Lock them in cellar with Sloth!”)

Well, I would put this position a bit differently. It's not that the homotopy categories of stable $\infty$-categories are good, and the triangulated categories that don't arise this way are bad. Rather, if you start with a stable $\infty$-category, then you shouldn't be discarding the higher information by forming the homotopy category in the first place.

I agree. There are useful tools that rely on just the underlying triangulated structure and there are things that impossible when doing this. Drawing the line well is important especially in a foundational library.

[Matthew Ballard]

For a more constructive idea, how far can you get with “candidate” triangles? (Those triples which go to long exact sequences under Hom)

[Johan Commelin]

@Matthew Ballard Could you please expand a bit on that idea? Do you mean that we try to build a bunch of API around triples that give a LES, and see if we can get to the triangle we want from there?

[Matthew Ballard]

Maybe but after things about this I don't think you are getting away from the problem.

[Johan Commelin]

Yeah, I guess I'll just have to sit down and do it. This week I finally seem to have an empty calendar again. (But today was already eaten up by generic lean/mathlib stuff.)

[Matthew Ballard]

I find Neeman's exposition to be the most clear and straight-forward presentation of the basic results in triangulated categories. I think Stacks uses it as a guide too.