Ext-groups

Stream: homology

[Joël Riou]

If C : Type u is an abelian category (with Category.{v} C), the type of morphisms in the derived category of C may be in a larger universe (like max u v), so that in my API for Ext-groups, there is an assumption HasExt.{w} which assumes that the types of morphisms in the derived category that are relevant for the definition of Ext-groups are Small.{w}. I showed certain properties (like long exact sequences of Ext) with this definition, but it is currently still unusable because we cannot compute anything yet.
However, I have finished a series of PR which identifies Ext^0 to morphisms in C, and deduce by induction that the Ext^n types are w-small (i.e. HasExt.{w} holds) when C has enough projectives. (The dual result would be easy to obtain as well.) This is a major step towards allowing computations of Ext-groups, e.g. in categories of modules. (With just a little more work, we may get the canonical t-structure on the derived category.)
These PRs are mostly about the study of the canonical truncations truncGE and truncLE of cochain complexes, which are developed in the general situation of embeddings of complex shapes (a notion which was introduced in the LTE, but then canonical truncations were not considered).

[Joël Riou]

• #19591 feat(CategoryTheory/Abelian): Ext^0 and Ext-groups when there are enough projectives (ready for review)
• #19585 feat(Algebra/Homology/DerivedCategory): the full embedding of an abelian category in its derived category
• #19584 feat(Algebra/Homology/DerivedCategory): calculus of fractions
• #19579 feat(Algebra/Homology/Embedding): homological properties of canonical truncations on cochain complexes
• #19578 feat(Algebra/Homology/Embedding): canonical truncations on CochainComplex
• #19574 feat(Algebra/Homology/Embedding): the homology of truncLE
• #19550 feat(Algebra/Homology/Embedding): the canonical truncation truncLE
• #19572 feat(Algebra/Homology/Embedding): homology of truncGE
• #20834 feat(Algebra/Homology): acyclic complexes
• #19570 feat(Algebra/Homology/Embedding): homology of truncGE'
• #19203 feat(Algebra/Homology/Embedding): API for the homology of an extension of homological complex
• #19544 feat(Algebra/Homology/Embedding): the morphism from a complex to its truncGE truncation
• #19198 feat(Algebra/Homology/Embedding): the homology of an extension of homological complexes
• #18502 feat(Algebra/Homology/Embedding): the left homology of an extension of homological complexes
• #19543 feat(Algebra/Homology/Embedding): the canonical truncation functor trunGEFunctor
• #19560 feat(Algebra/Homology/Embedding): dualise extend
• #19559 feat(Algebra/Homology): more duality results

[Joël Riou]

(Most of the code is from my branch #4197.)

[Joël Riou]

Note: there are large-import warnings on some of these PRs, but the affected files are those that I am developing, and it would not make sense to split the files here. The extra imports point to files related to the API about the homology of complexes: in downstream uses, when we want to use truncations of complexes, we obviously want to use their homological properties!

[Dagur Asgeirsson]

Joël Riou said:

• #18502 feat(Algebra/Homology/Embedding): the left homology of an extension of homological complexes (ready)
• #19543 feat(Algebra/Homology/Embedding): the canonical truncation functor trunGEFunctor (ready)
• #19560 feat(Algebra/Homology/Embedding): dualise extend (ready)
• #19559 feat(Algebra/Homology): more duality results (ready)

I've put the first three of these are on the maintainer queue, and commented a small question on the last one

[Joël Riou]

Thanks very much for the reviews!

[Joël Riou]

In the series above (towards the relation between Ext^0 defined using the derived category and the type of morphisms in an abelian category), two PRs are ready for review #19203 and #19544.

[Kim Morrison]

#19203 still needs review.

[Joël Riou]

Currently, there are three PRs ready for review in the series above: #19550 #19570 #19203

[Joël Riou]

The next two (independent) PR are #19572 and #19578.

[Joël Riou]

The next PR in the series is #19574, which is about the homology of the canonical truncation truncLE (all results are obtained directly by duality from the same results for truncGE).

[Joël Riou]

#19584 is ready for review: it contains various lemmas that are deduced from the calculus of fractions and canonical truncations:

[Joël Riou]

The penultimate PR is #19585: this is the full embedding of an abelian category in its derived category.

[Joël Riou]

The last PR in this series is #19591: if relates Ext^0 and Hom and shows that the Ext-groups are small when there are enough projectives.