Derived hom and tensor

Stream: homology

[Brendan Seamas Murphy]

Assuming the derived categories PR is fully merged, how far off would defining the derived hom and tensor product be? I guess the biggest roadblock would be making sense of K-projective (cofibrant in projective model structure) and K-injective (fibrant in injective model structure) resolutions? I'd be happy to work on this but I want to make sure no one else has a plan in mind already (and I'm not sure what the right design decision is if we want to handle the noncommutative and commutative cases on equal footing. Should we end up with two different "RHom"s over a commutative ring, one a chain complex of modules and one a chain complex of abelian groups?)

[Brendan Seamas Murphy]

Maybe I should first ask about the underived hom and tensor of complexes? (for some reason I thought we had these)

[Joël Riou]

I already have working code for the total right derived functor on the bounded below derived category K^+ when we have enough injectives. (I have obtained the Grothendieck spectral sequence for the composition of these.) The technical part was to obtain the CM5 factorization axiom for the model category structure on C^+.

[Joël Riou]

My plan for derived functors of several variables is to start with the tensor product. I should obtain very soon the "flat derivability structure": roughly speaking (the API will be more general), the inclusion K^-(ModuleCatFlat R) ⥤ K^-(ModuleCat R) induces an equivalence on the localized categories with respect to quasi-isomorphisms. Using that, we may define derived functors of functors which preserves quasi-isos between bounded above complexes of flat objects. (I have already obtained some technical lemmas, like if f is a morphisms of bicomplexes (with some bounds) such that f induces a quasi-iso on each column, then the induced map on the total complexes is a quasi-iso.)

[Joël Riou]

Then, the plan is to obtain the monoidal category structure on the bounded above derived category of modules, and obtain a symmetric Tor bifunctor with long exact sequences on both variables, which would allow the development of local algebra (Koszul complexes, etc.).

[Joël Riou]

The API for derived functors in two variables that I am thinking of should be good enough to handle both the case of the derived tensor of a functor that is covariant in both variables (like the tensor product), but also Hom, etc.

[Joël Riou]

I have already done some PRs for the extension of functors to bicomplexes #10880, compatibilities with shifts #11517, etc.

[Joël Riou]

(In a more remote future, we may remove + and - in some of the constructions above. The main difficulty is to get suitable resolution lemmas, e.g. every complex admits a K-injective resolution.)

[Brendan Seamas Murphy]

Yeah, local algebra is what I wanted this for. But it's tricky to stay within just left or just right bounded complexes for that, imo. Usually we're going to start with right-bounded complexes (projective resolutions of modules) and then as soon as we want to RHom out of these we leave that world

[Brendan Seamas Murphy]

It sounds like this is not going to be finished in the near future, so I'll probably need to stick with juggling Ext groups to prove things about regular sequences for now

[Brendan Seamas Murphy]

(I would be happy to try and add K projective and K injective resolutions, but the rest of the API also seems like it'll take a minute to get set up)

[Joël Riou]

An alternative is to formalize Proposition 3.13 in https://arxiv.org/abs/math/0102087 (I would be very happy not to work on this!).

(For flat resolutions, I am starting with the C^- case, but K-flat resolutions of unbounded complexes are not so hard to get, as far as I remember.)

Still, I think that there is already a lot of things to do using only Ext and Tor functorS.

[Joël Riou]

I have essentially obtained flat resolutions. More precisely, if ι : A ⥤ C is a fully faithful functor from an additive category A to an abelian category C equipped with a functor F : C ⥤ A (preserving zero maps, but not necessarily additive) and a natural transformation π : F ⋙ ι ⟶ 𝟭 C such that [Epi (π.app X)] for all X (it shall be so with C := ModuleCat R and A the full subcategory of flat modules, using a small modification of the free module functor, and this will also apply to (pre)sheaves of modules), then any bounded above cochain complex in C admits a functorial quasi-iso from a bounded above cochain complex in A. Then, I show that the bounded above derived category of C identifies to the localization of CochainComplex.Minus A with respect to the morphisms which become quasi-isomorphisms in CochainComplex.Minus A https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/Algebra/Homology/LeftResolution/DerivabilityStructure.lean#L42

It also obviously satisfies the dual assumptions for the constructor of derivability structure I have obtained in #12676, so that when I dualize the notion of right derivability structures #12633 to left derivability structures, we shall get the "flat" left derivability structure, and once the suitable API for derived functors is formalized (this depends on #12206), it will be possible to derive the tensor product as a functor in two variables.