Theorems · Definition · category theory

CategoryTheory.LocalizerMorphism.rightDerivedFunctorComparison

{C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {D₁ : Type u₄} →
              {D₂ : Type u₅} →
                [inst_3 : CategoryTheory.Category.{v₄, u₄} D₁] →
                  [inst_4 : CategoryTheory.Category.{v₅, u₅} D₂] →
                    {W₁ : CategoryTheory.MorphismProperty C₁} →
                      {W₂ : CategoryTheory.MorphismProperty C₂} →
                        (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
                          (L₁ : CategoryTheory.Functor C₁ D₁) →
                            (L₂ : CategoryTheory.Functor C₂ D₂) →
                              [inst_5 : L₁.IsLocalization W₁] →
                                [inst_6 : L₂.IsLocalization W₂] →
                                  (F : CategoryTheory.Functor C₂ H) →
                                    (F₁ : CategoryTheory.Functor D₁ H) →
                                      (α₁ : Φ.functor.comp F ⟶ L₁.comp F₁) →
                                        (F₂ : CategoryTheory.Functor D₂ H) →
                                          (F ⟶ L₂.comp F₂) →
                                            [F₁.IsRightDerivedFunctor α₁ W₁] → F₁ ⟶ (Φ.localizedFunctor L₁ L₂).comp F₂

If Φ is a localizer morphism from W₁ : MorphismProperty C₁ to W₂ : MorphismProperty C₂, if L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ are localization functors for W₁ and W₂, if F : C₂ ⥤ H is a functor, if F₁ : D₁ ⥤ H is a right derived functor of Φ.functor ⋙ F, and if F₂ : D₂ ⥤ H is a functor equipped with a natural transformation α₂ : F ⟶ L₂ ⋙ F₂, this is the canonical morphism F₁ ⟶ Φ.localizedFunctor L₁ L₂ ⋙ F₂.

Defined in

Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived

Cited by

6 results in Mathlib

Foundations

Depth 83 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsRightDerivedFunctor