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.

[Joël Riou]

I have just obtained the following result at https://github.com/leanprover-community/mathlib4/blob/773a0884841ba21e8632ff41f30a95551bc8eb26/Mathlib/CategoryTheory/Monoidal/Derived.lean :

CategoryTheory.DerivedMonoidal.instMonoidalCategory.{u_1, u_2, u_3, u_4}
    {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D]
    [MonoidalCategory C] (L : C ⥤ D) (W : MorphismProperty C)
    [L.IsLocalization W] [W.ContainsIdentities] [L.HasDerivedMonoidalCategory W] :
    MonoidalCategory (DerivedMonoidal L W)

[Joël Riou]

It says that if L : C ⥤ D makes D the localized category of C with respect to W : MorphismProperty C and if C has a monoidal category structure, then there is a left derived monoidal category structure on D (the statement involves the type synonym DerivedMonoidal L W) if L and W satisfy a technical condition L.HasDerivedMonoidalCategory W which is that the bifunctor (X₁, X₂) ↦ L.obj (X₁ ⊗ X₂) has a left derived functor which satisfies some additional properties (it mostly says that the "iterated" versions of this bifunctor also give the left derived functor of the tensor product in 3 or 4 variables). In order to do this, I had to develop notions of left derived functors in two, three and even four variables (this is because the pentagon axiom of monoidal categories involves 4 objects), which I translated in terms of left derived functors in one variable via uncurryfication.

[Joël Riou]

In order to apply this to the derived category, my plan is to generalize the results of #23915 about the construction and recognition principles for derived functors using derivability structures (a notion introduced by Bruno Kahn and Georges Maltsiniotis). As I have shown that derivability structures behave well with respect to products of categories, I should get generalizations of #23915 for functors in two, three or four variables. What I expect to show is that if Φ : LocalizerMorphism W₀ W is a left derivability structure whose functor Φ₀.functor : C₀ ⥤ C is a monoidal functor which "derives" the tensor product on C with respect to W, then the assumptions of the previous definition will hold, which shall give a (left derived) monoidal category structure on the localized category D.

[Joël Riou]

With some more work polishing the flat or "K-flat" derivability structure on the homotopy category of complexes in suitable abelian categories A, I intend to obtain a monoidal category structure on DerivedCategory A, and hopefully this will allow a definition of Tor. (The "properties" of Tor would require further investigation of the compatibilities with shifts.)

[Joël Riou]

(This was outlined in https://hal.science/hal-04546712 §5.3.4)

[Johan Commelin]

That's really cool!

[Joël Riou]

In between, I have obtained the expected result about the existence of a (derived) monoidal structure on the localized category under the assumption that we can derive the tensor product using a left derivability structure Φ such that the underlying functor Φ.functor is monoidal:

CategoryTheory.LocalizerMorphism.DerivesMonoidalStructure.hasDerivedMonoidalCategory
  {C₀ C D : Type*} [Category C₀] [Category C] [Category D] [MonoidalCategory C₀]
  [MonoidalCategory C] {W₀ : MorphismProperty C₀} {W : MorphismProperty C}
  (Φ : LocalizerMorphism W₀ W) [W₀.ContainsIdentities] [W.ContainsIdentities]
  [Φ.IsLeftDerivabilityStructure] [Φ.functor.Monoidal] (L : C ⥤ D) [L.IsLocalization W]
  (h : Φ.DerivesMonoidalStructure L) :
  L.HasDerivedMonoidalCategory W

https://github.com/leanprover-community/mathlib4/blob/1f7a1c0960a5cb55fd9271640a7430207ac9541d/Mathlib/CategoryTheory/Localization/DerivabilityStructure/Monoidal.lean#L50

[Joël Riou]

Then, I have formalized the K-flat derivability structure on cochain complexes (and on the homotopy category). Under the assumption that a monoidal abelian category A has a functorial flat resolution (i.e. for any X : A, there is an epimorphism P ⟶ X with P flat, which is functorial in X) and a few basic assumptions (including that A has exact colimits of shape ℤ, a property which holds for Grothendieck abelian categories), I have obtained a functorial K-flat resolution of (unbounded) complexes in A (the proof is similar as in Spaltenstein's original paper), and it follows that the inclusion functor from K-flat cochain complexes to cochain complexes induces a left derivability structure. Using some small facts about Guitart exact squares (a rather esoteric categorical notion which appears in the definition of a derivability structure), including https://github.com/leanprover-community/mathlib4/blob/jriou_localization/Mathlib/CategoryTheory/GuitartExact/Quotient.lean , I have deduced that there is a "quotient" left derivability structure given by the inclusion of the homotopy category of K-flat complexes in the whole homotopy category (as this inclusion functor is triangulated, this will have consequences about interactions between the derived tensor product and distinguished triangles...).

https://github.com/leanprover-community/mathlib4/blob/1f7a1c0960a5cb55fd9271640a7430207ac9541d/Mathlib/CategoryTheory/Abelian/Flat/KFlat.lean#L505-L516

[Joël Riou]

In particular, I have applied this to categories of modules:

noncomputable example (R : Type u) [CommRing R] [HasDerivedCategory (ModuleCat.{u} R)] :
  MonoidalCategory (DerivedCategory (ModuleCat.{u} R)) := inferInstance

I am sorry this is not computable! and I have a new definition of Tor:

protected noncomputable def tor (P Q : ModuleCat.{u} R) (n : ℤ) : ModuleCat.{u} R :=
  (t.homology (-n)).obj ((t.ιHeart.obj P ⊗ t.ιHeart.obj Q))

where t is the canonical t-structure on the derived category of the category of R-modules. (The same will hold for categories of sheaves of modules.) The definition suggests that internally, Tor will be defined whenever we have a monoidal triangulated category equipped with a t-structure.
(I have quite precise ideas on how to show that the derived tensor product is a "triangulated functor in two variables", which would give the long exact sequences of Tor, but I will probably not work on this very soon.)
https://github.com/leanprover-community/mathlib4/blob/1f7a1c0960a5cb55fd9271640a7430207ac9541d/Mathlib/CategoryTheory/Abelian/Flat/ModuleCat.lean