Derived categories in mathlib

Stream: homology

[Joël Riou]

I have just finished preparing a series of PR which ends with the construction of the derived category of an abelian category, as a triangulated category:

• #11740 feat(CategoryTheory): triangulated subcategories
• #11789 feat(CategoryTheory): the class of morphisms whose cone belongs to a triangulated subcategory
• #11759 feat(CategoryTheory/Triangulated): homological functors
• #11805 feat(CategoryTheory/Triangulated): the long exact sequence of a homological functor
• #11760 feat: the homological functor on the homotopy category of cochain complexes in an abelian category
• #11721 feat(CategoryTheory/Localization): dualize results for right calculus of fractions
• #11737 feat(CategoryTheory): more lemmas for the calculus of fractions
• #11728 feat(CategoryTheory/Localization): the localized category is preadditive
• #11738 feat(CategoryTheory): localization of pretriangulated categories
• #11786 feat(CategoryTheory): localization of triangulated categories
• #11764 feat(CategoryTheory/Shift): the induced shift sequence
• #11782 feat(Algebra/Homology): compatibilities of homology and shifts
• #11806 feat: the derived category of an abelian category

[Joël Riou]

A first version of my paper Formalization of derived categories in Lean/mathlib is online at https://hal.science/hal-04546712

It is supported by a Lean file at https://github.com/joelriou/lean-derived-categories

Abstract: This paper outlines the formalization of derived categories in the mathematical library of the proof assistant Lean 4. The derived category D(C) of any abelian category C is formalized as the localization of the category of unbounded cochain complexes with respect to the class of quasi-isomorphisms, and it is endowed with a triangulated structure.

[Kim Morrison]

I've merged #11764 and #11737 above, and delegated #11740.

[Johan Commelin]

I delegated #11728 and #11782.

[Joël Riou]

Only two PR to go before the derived category enters mathlib: #11786 which shows that the localization of a triangulated category satisfies the octahedron axiom, and the final one #11806.

[Joël Riou]

Thanks to an insight by @Andrew Yang https://github.com/leanprover-community/mathlib4/pull/11786#discussion_r1628462240, a new dependency just appeared #13558: if L : C ⥤ D is a localization functor for a class of morphisms W that has a left or right calculus of fractions, then any finite composition of morphisms in D can be lifted up to isomorphisms in C (i.e. L.mapComposableArrows n is essentially surjective for all n). I had done this previously only in the case n = 0, n = 1 and n = 2 (assuming both left/right calculus of fractions).
The consequence is that it is possible to localize a triangulated category assuming only left calculus of fractions (and other standard conditions), which is a sharper result than what was known (to me, at least).

[Johan Commelin]

Very nice! borsificated

[Andrew Yang]

Having left calculus of fractions is exactly the left ore condition so it is reasonable that one side is enough.
Time to refactor Monoids in mathlib as categories with one object so that we can reuse these great localization api without duplicating them as OreLocalization /j

[Kevin Buzzard]

categories with one object and an nsmul field, right?

[Joël Riou]

Derived categories are now in mathlib. For me, the next target will be to refactor Ext-groups using morphisms in derived categories, so that we get long exact sequences of Ext (which will allow definitions of projective/injective dimension, etc). One technical hurdle is that morphisms in the derived category may be in a larger universe, so that I intend to define first something named LargeExt #13599, and after that, provide some API to shrink these groups (at least when there are enough projectives or enough injectives).

(Note: A priori, I do not intend to define projectiveDimension X : WithTop ℕ, but rather a typeclass ProjectiveDimensionLE X n.)

[Joël Riou]

Thanks to all reviewers @Johan Commelin @Andrew Yang @Markus Himmel @Riccardo Brasca @Kevin Buzzard @Kim Morrison @Dagur Asgeirsson!

[Kevin Buzzard]

(Note: A priori, I do not intend to define projectiveDimension X : WithTop ℕ, but rather a typeclass ProjectiveDimensionLE X n.)

I really like that idea. Functions like the degree of a polynomial and the dimension of an algebraic variety are historically what everyone uses, but they have problems when formalising; what is the dimension of the empty variety, or the degree of the zero polynomial? And the fibres are also poorly-behaved, for example polynomials of degree n don't necessarily add or subtract to give a polynomial of degree n, and they don't necessarily multiply to give a polynomial of degree 2n if you're not over an integral domain. In contrast, polynomials of degree at most n are a very natural object, they're an R-submodule of R[X]. Arguably even more natural is "polynomials of degree less than n" because then you can get {0} with n=0. If you look at the API for polynomials, you can see "<= n" everywhere and "= n" far more rarely. Similarly with dimension: Jujian ended up defining the Krull dimension of a topological space or commutative ring to be in WithBot(WithTop(Nat)) and here you can just do the same thing: you can ask "is the dimension less than n" for n any natural and now you can say everything which you can say with the WithBot(WithTop) hack (for example an infinite-dimensional ring is just something which doesn't have dimension less than n for any n) but without ever leaving the world of naturals.

[Brendan Seamas Murphy]

I don't like this design. How you do state "projectiveDimension M = n" with this API? How do you state a formula which has the projective dimensions of two different modules on both sides? Also, I don't get the reasoning for using a typeclass here

Coincidentally, I just started defining projective dimension (preparing for auslander buchsbaum) and intended to define it as the infimum over all projective resolutions P of the amplitide of P (defined to be 0 for the 0 resolution). I'm not sure how I should proceed now

[Johan Commelin]

@Joël Riou maybe this has been discussed before, but can we now also get bounded derived cats easily?

[Joël Riou]

Johan Commelin said:

Joël Riou maybe this has been discussed before, but can we now also get bounded derived cats easily?

After we define the homology functor from the derived category of C to C, it would be easy to define the bounded/bounded below/bounded above. However, the better definition shall be by developing more the API of t-structures, and defining this in that context. If there is a need, we may give a more direct definition as soon as it is possible. (However, showing something like the category D^-, as a full subcategory of D, is the localization of the category of bounded above complexes requires results about localizing subcategories and truncations (which I have formalised), and these ingredients are essentially what we need to construct the canonical t-structure.

[Joël Riou]

Brendan Seamas Murphy said:

I don't like this design. How you do state "projectiveDimension M = n" with this API?

I have used typeclasses for my code on truncations (saying that a complex is strictly/cohomologically less/greater than or equal to a certain n, and it has worked quite nicely.

I think that typeclasses could be very nice in order to formalise results about categories of global dimension less and or equal to 0 (or 1) for example. Of course, if there is a need, we may also define a term projectiveDimension, but as Kevin suggests, it is likely that many lemmas would have projectiveDimension X <= n as assumptions...

My first idea would be to define the projective dimension in terms of the vanishing of Ext in big enough degrees (and show the equivalence with the definition you suggest when the category has enough projectives).

At this stage, I do not want to hinder the development of applications of homological algebra. You may very well proceed with your implementation, and when more ingredients from the language of derived categories become available, we may proceed with a refactor.

[Damiano Testa]

For what is worth, while working on compute_degree, I also played with a typeclass for degree/natDegree of polynomials at most something and it worked very well. In fact, most of the tactic is devoted to computing exact degree: the upper bound you get almost immediately. What is hard is showing that the not-known-to-be-sharp bound is indeed correct.

[Joël Riou]

I have implemented HasProjectiveDimensionLT in #19604.