Derivability structures

Let Φ : LocalizerMorphism W₁ W₂ be a localizer morphism, i.e. W₁ : MorphismProperty C₁, W₂ : MorphismProperty C₂, and Φ.functor : C₁ ⥤ C₂ is a functors which maps W₁ to W₂. Following the definition introduced by Bruno Kahn and Georges Maltsiniotis in Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité, we say that Φ is a right derivability structure if Φ has right resolutions and the following 2-square is Guitart exact, where L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ are localization functors for W₁ and W₂, and F : D₁ ⥤ D₂ is the induced functor on the localized categories:

    Φ.functor
  C₁   ⥤   C₂
  |         |
L₁|         | L₂
  v         v
  D₁   ⥤   D₂
       F

Implementation details

In the field guitartExact' of the structure LocalizerMorphism.IsRightDerivabilityStructure, The condition that the square is Guitart exact is stated for the localization functors of the constructed categories (W₁.Q and W₂.Q). The lemma LocalizerMorphism.isRightDerivabilityStructure_iff show that it does not depend of the choice of the localization functors.

TODO

• Construct derived functors using derivability structures
• Define the notion of left derivability structures
• Construct the injective derivability structure in order to derive functor from the bounded below homotopy category in an abelian category with enough injectives
• Construct the projective derivability structure in order to derive functor from the bounded above homotopy category in an abelian category with enough projectives
• Construct the flat derivability structure on the bounded above homotopy category of categories of modules (and categories of sheaves of modules)
• Define the product derivability structure and formalize derived functors of functors in several variables

References

• Bruno Kahn and Georges Maltsiniotis, Structures de dérivabilité

class CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) : Prop

A localizer morphism Φ : LocalizerMorphism W₁ W₂ is a right derivability structure if it has right resolutions and the 2-square where the left and right functors are localizations functors for W₁ and W₂ are Guitart exact.

• hasRightResolutions : Φ.HasRightResolutions
• guitartExact' : CategoryTheory.TwoSquare.GuitartExact (CategoryTheory.CatCommSq.iso Φ.functor W₁.Q W₂.Q (Φ.localizedFunctor W₁.Q W₂.Q)).hom

theorem CategoryTheory.LocalizerMorphism.isRightDerivabilityStructure_iff {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2} [CategoryTheory.Category.{u_4, u_1} D₁] [CategoryTheory.Category.{u_3, u_2} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] (F : CategoryTheory.Functor D₁ D₂) [Φ.HasRightResolutions] (e : Φ.functor.comp L₂ ≅ L₁.comp F) : Φ.IsRightDerivabilityStructure ↔ CategoryTheory.TwoSquare.GuitartExact e.hom

theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure' {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2} [CategoryTheory.Category.{u_4, u_1} D₁] [CategoryTheory.Category.{u_3, u_2} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] (F : CategoryTheory.Functor D₁ D₂) [h : Φ.IsRightDerivabilityStructure] (e : Φ.functor.comp L₂ ≅ L₁.comp F) : CategoryTheory.TwoSquare.GuitartExact e.hom

theorem CategoryTheory.LocalizerMorphism.guitartExact_of_isRightDerivabilityStructure {C₁ : Type u₁} {C₂ : Type u₂} [CategoryTheory.Category.{v₁, u₁} C₁] [CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁} {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {D₁ : Type u_1} {D₂ : Type u_2} [CategoryTheory.Category.{u_3, u_1} D₁] [CategoryTheory.Category.{u_4, u_2} D₂] (L₁ : CategoryTheory.Functor C₁ D₁) (L₂ : CategoryTheory.Functor C₂ D₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] [Φ.IsRightDerivabilityStructure] : CategoryTheory.TwoSquare.GuitartExact (CategoryTheory.CatCommSq.iso Φ.functor L₁ L₂ (Φ.localizedFunctor L₁ L₂)).hom

instance CategoryTheory.LocalizerMorphism.instHasRightResolutionsIdOfContainsIdentities {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} [W₁.ContainsIdentities] : (CategoryTheory.LocalizerMorphism.id W₁).HasRightResolutions

instance CategoryTheory.LocalizerMorphism.instIsRightDerivabilityStructureIdOfContainsIdentities {C₁ : Type u₁} [CategoryTheory.Category.{v₁, u₁} C₁] {W₁ : CategoryTheory.MorphismProperty C₁} [W₁.ContainsIdentities] : (CategoryTheory.LocalizerMorphism.id W₁).IsRightDerivabilityStructure