Documentation

Mathlib.CategoryTheory.Functor.Derived.RightDerivedComposition

Comparison morphism for the composition of right derived functors #

     F₁₂  F₂₃
  C₁ ⥤ C₂ = C₃
L₁|  L₂|   L₃|
  v    v     v
  D₁ ⥤ D₂ ⥤ D₃
   RF₁₂   RF₂₃

In the situation above, when we have natural transformations α₁₂ : F₁₂ ⋙ L₂ ⟶ L₁ ⋙ RF₁₂, α₂₃ : F₂₃ ⋙ L₃ ⟶ L₂ ⋙ RF₂₃, an isomorphism e : F₁₂ ⋙ F₂₃ ≅ F₁₃ where F₁₃ : C₁ ⥤ C₃, and a natural transformation α₁₃ : F₁₃ ⋙ L₃ ⟶ L₁ ⋙ RF₁₃ which makes RF₁₃ the derived functor of of F₁₃ ⋙ L₃ (with respect to W₁ : MorphismProperty C₁), we define a natural transformation RF₁₃ ⟶ RF₁₂ ⋙ RF₂₃ (see Functor.natTransOfIsRightDerivedFunctorComp). We may say that this is the comparison morphism for the composition of right derived functors, even though the definition only assumes that RF₁₃ is a right derived functor. (In applications, both RF₁₂ and RF₂₃ would usually be derived functors as well.)

source
noncomputable def CategoryTheory.Functor.natTransOfIsRightDerivedFunctorComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (e : F₁₂.comp F₂₃ ≅ F₁₃) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {RF₁₂ : Functor D₁ D₂} {RF₂₃ : Functor D₂ D₃} {RF₁₃ : Functor D₁ D₃} (α₁₂ : F₁₂.comp L₂ ⟶ L₁.comp RF₁₂) (α₂₃ : F₂₃.comp L₃ ⟶ L₂.comp RF₂₃) (α₁₃ : F₁₃.comp L₃ ⟶ L₁.comp RF₁₃) [RF₁₃.IsRightDerivedFunctor α₁₃ W₁] :
RF₁₃ ⟶ RF₁₂.comp RF₂₃

The comparison morphism for the composition of right derived functors.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Functor.comp_whiskerLeft_natTransOfIsRightDerivedFunctorComp {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (e : F₁₂.comp F₂₃ ≅ F₁₃) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {RF₁₂ : Functor D₁ D₂} {RF₂₃ : Functor D₂ D₃} {RF₁₃ : Functor D₁ D₃} (α₁₂ : F₁₂.comp L₂ ⟶ L₁.comp RF₁₂) (α₂₃ : F₂₃.comp L₃ ⟶ L₂.comp RF₂₃) (α₁₃ : F₁₃.comp L₃ ⟶ L₁.comp RF₁₃) [RF₁₃.IsRightDerivedFunctor α₁₃ W₁] :
    CategoryStruct.comp α₁₃ (L₁.whiskerLeft (natTransOfIsRightDerivedFunctorComp e L₁ L₂ L₃ W₁ α₁₂ α₂₃ α₁₃)) = CategoryStruct.comp (whiskerRight e.inv L₃) (CategoryStruct.comp (F₁₂.associator F₂₃ L₃).hom (CategoryStruct.comp (F₁₂.whiskerLeft α₂₃) (CategoryStruct.comp (F₁₂.associator L₂ RF₂₃).inv (CategoryStruct.comp (whiskerRight α₁₂ RF₂₃) (L₁.associator RF₁₂ RF₂₃).hom))))
    source
    @[simp]
    theorem CategoryTheory.Functor.comp_whiskerLeft_natTransOfIsRightDerivedFunctorComp_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (e : F₁₂.comp F₂₃ ≅ F₁₃) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {RF₁₂ : Functor D₁ D₂} {RF₂₃ : Functor D₂ D₃} {RF₁₃ : Functor D₁ D₃} (α₁₂ : F₁₂.comp L₂ ⟶ L₁.comp RF₁₂) (α₂₃ : F₂₃.comp L₃ ⟶ L₂.comp RF₂₃) (α₁₃ : F₁₃.comp L₃ ⟶ L₁.comp RF₁₃) [RF₁₃.IsRightDerivedFunctor α₁₃ W₁] {Z : Functor C₁ D₃} (h : L₁.comp (RF₁₂.comp RF₂₃) ⟶ Z) :
    CategoryStruct.comp α₁₃ (CategoryStruct.comp (L₁.whiskerLeft (natTransOfIsRightDerivedFunctorComp e L₁ L₂ L₃ W₁ α₁₂ α₂₃ α₁₃)) h) = CategoryStruct.comp (whiskerRight e.inv L₃) (CategoryStruct.comp (F₁₂.associator F₂₃ L₃).hom (CategoryStruct.comp (F₁₂.whiskerLeft α₂₃) (CategoryStruct.comp (F₁₂.associator L₂ RF₂₃).inv (CategoryStruct.comp (whiskerRight α₁₂ RF₂₃) (CategoryStruct.comp (L₁.associator RF₁₂ RF₂₃).hom h)))))
    source
    @[simp]
    theorem CategoryTheory.Functor.comp_natTransOfIsRightDerivedFunctorComp_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (e : F₁₂.comp F₂₃ ≅ F₁₃) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {RF₁₂ : Functor D₁ D₂} {RF₂₃ : Functor D₂ D₃} {RF₁₃ : Functor D₁ D₃} (α₁₂ : F₁₂.comp L₂ ⟶ L₁.comp RF₁₂) (α₂₃ : F₂₃.comp L₃ ⟶ L₂.comp RF₂₃) (α₁₃ : F₁₃.comp L₃ ⟶ L₁.comp RF₁₃) [RF₁₃.IsRightDerivedFunctor α₁₃ W₁] (X : C₁) :
    CategoryStruct.comp (α₁₃.app X) ((natTransOfIsRightDerivedFunctorComp e L₁ L₂ L₃ W₁ α₁₂ α₂₃ α₁₃).app (L₁.obj X)) = CategoryStruct.comp (L₃.map (e.inv.app X)) (CategoryStruct.comp (α₂₃.app (F₁₂.obj X)) (RF₂₃.map (α₁₂.app X)))
    source
    @[simp]
    theorem CategoryTheory.Functor.comp_natTransOfIsRightDerivedFunctorComp_app_assoc {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (e : F₁₂.comp F₂₃ ≅ F₁₃) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {RF₁₂ : Functor D₁ D₂} {RF₂₃ : Functor D₂ D₃} {RF₁₃ : Functor D₁ D₃} (α₁₂ : F₁₂.comp L₂ ⟶ L₁.comp RF₁₂) (α₂₃ : F₂₃.comp L₃ ⟶ L₂.comp RF₂₃) (α₁₃ : F₁₃.comp L₃ ⟶ L₁.comp RF₁₃) [RF₁₃.IsRightDerivedFunctor α₁₃ W₁] (X : C₁) {Z : D₃} (h : RF₂₃.obj (RF₁₂.obj (L₁.obj X)) ⟶ Z) :
    CategoryStruct.comp (α₁₃.app X) (CategoryStruct.comp ((natTransOfIsRightDerivedFunctorComp e L₁ L₂ L₃ W₁ α₁₂ α₂₃ α₁₃).app (L₁.obj X)) h) = CategoryStruct.comp (L₃.map (e.inv.app X)) (CategoryStruct.comp (α₂₃.app (F₁₂.obj X)) (CategoryStruct.comp (RF₂₃.map (α₁₂.app X)) h))
    source
    theorem CategoryTheory.Functor.isIso_natTransOfIsRightDerivedFunctorComp_app {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6} [Category.{v_1, u_1} C₁] [Category.{v_2, u_2} C₂] [Category.{v_3, u_3} C₃] [Category.{v_4, u_4} D₁] [Category.{v_5, u_5} D₂] [Category.{v_6, u_6} D₃] {F₁₂ : Functor C₁ C₂} {F₂₃ : Functor C₂ C₃} {F₁₃ : Functor C₁ C₃} (e : F₁₂.comp F₂₃ ≅ F₁₃) (L₁ : Functor C₁ D₁) (L₂ : Functor C₂ D₂) (L₃ : Functor C₃ D₃) (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {RF₁₂ : Functor D₁ D₂} {RF₂₃ : Functor D₂ D₃} {RF₁₃ : Functor D₁ D₃} (α₁₂ : F₁₂.comp L₂ ⟶ L₁.comp RF₁₂) (α₂₃ : F₂₃.comp L₃ ⟶ L₂.comp RF₂₃) (α₁₃ : F₁₃.comp L₃ ⟶ L₁.comp RF₁₃) [RF₁₃.IsRightDerivedFunctor α₁₃ W₁] (X : C₁) (h₁₂ : IsIso (α₁₃.app X) := by infer_instance) :
    autoParam (IsIso (α₁₂.app X)) isIso_natTransOfIsRightDerivedFunctorComp_app._auto_3 → ∀ (h₂₃ : autoParam (IsIso (α₂₃.app (F₁₂.obj X))) isIso_natTransOfIsRightDerivedFunctorComp_app._auto_5), IsIso ((natTransOfIsRightDerivedFunctorComp e L₁ L₂ L₃ W₁ α₁₂ α₂₃ α₁₃).app (L₁.obj X))