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é][KahnMaltsiniotis2008],
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é][KahnMaltsiniotis2008]
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₂)
:
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
Instances
theorem
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.hasRightResolutions
{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₂}
[self : Φ.IsRightDerivabilityStructure]
:
Φ.HasRightResolutions
theorem
CategoryTheory.LocalizerMorphism.IsRightDerivabilityStructure.guitartExact'
{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₂}
[self : Φ.IsRightDerivabilityStructure]
:
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)
:
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
Equations
- ⋯ = ⋯
instance
CategoryTheory.LocalizerMorphism.instIsRightDerivabilityStructureIdOfContainsIdentities
{C₁ : Type u₁}
[CategoryTheory.Category.{v₁, u₁} C₁]
{W₁ : CategoryTheory.MorphismProperty C₁}
[W₁.ContainsIdentities]
:
(CategoryTheory.LocalizerMorphism.id W₁).IsRightDerivabilityStructure
Equations
- ⋯ = ⋯