Deriving functors using a derivability structure #
Let Φ : LocalizerMorphism W₁ W₂ be a localizer morphism between classes
of morphisms on categories C₁ and C₂. Let F : C₂ ⥤ H.
When Φ is a left or right derivability structure, it allows to derive
the functor F (with respect to W₂) when Φ.functor ⋙ F : C₁ ⥤ H
inverts W₁ (this is the most favorable case when we can apply the lemma
hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure).
We define Φ.Derives F as an abbreviation for W₁.IsInvertedBy (Φ.functor ⋙ F).
When h : Φ.Derives F holds and Φ is a right derivability structure,
we show that F has a right derived functor with respect to W₂.
Under this assumption, if L₂ : C₂ ⥤ D₂ is a localization functor
for W₂, then a functor RF : D₂ ⥤ H equipped with a natural
transformation α : F ⟶ L₂ ⋙ RF is the right derived functor of F iff
for any X₁ : C₁, the map α.app (Φ.functor.obj X₁) is an isomorphism.
Given a localizer morphism Φ : LocalizerMorphism W₁ W₂ between
morphism properties on C₁ and C₂, and a functor C₂ ⥤ H, this
is the property that W₁ is inverted by Φ.functor ⋙ F.
In case Φ is a (left/right) derivability structure, this allows
the construction of a derived functor for F relatively to W₂.
Equations
- Φ.Derives F = W₁.IsInvertedBy (Φ.functor.comp F)