Derived adjunction

Assume that functors G : C₁ ⥤ C₂ and F : C₂ ⥤ C₁ are part of an adjunction adj : G ⊣ F, that we have localization functors L₁ : C₁ ⥤ D₁ and L₂ : C₂ ⥤ D₂ with respect to classes of morphisms W₁ and W₂, and that G admits a left derived functor G' : D₁ ⥤ D₂ and F a right derived functor F' : D₂ ⥤ D₁. We show that there is an adjunction G' ⊣ F' under the additional assumption that F' and G' are absolute derived functors, i.e. they remain derived functors after the post-composition with any functor (we actually only need to know that G' ⋙ F' is the left derived functor of G ⋙ L₂ ⋙ F' and that F' ⋙ G' is the right derived functor of F ⋙ L₁ ⋙ G').

References

• [Georges Maltsiniotis, Le théorème de Quillen, d'adjonction des foncteurs dérivés, revisité][Maltsiniotis2007]

def CategoryTheory.Adjunction.derived' {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂] (η : Functor.id D₁ ⟶ G'.comp F') (ε : F'.comp G' ⟶ Functor.id D₂) (hη : ∀ (X₁ : C₁), CategoryStruct.comp (η.app (L₁.obj X₁)) (F'.map (α.app X₁)) = CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁)) := by cat_disch) (hε : ∀ (X₂ : C₂), CategoryStruct.comp (G'.map (β.app X₂)) (ε.app (L₂.obj X₂)) = CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)) := by cat_disch) : G' ⊣ F'

Auxiliary definition for Adjunction.derived.

@[simp]

theorem CategoryTheory.Adjunction.derived'_counit {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂] (η : Functor.id D₁ ⟶ G'.comp F') (ε : F'.comp G' ⟶ Functor.id D₂) (hη : ∀ (X₁ : C₁), CategoryStruct.comp (η.app (L₁.obj X₁)) (F'.map (α.app X₁)) = CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁)) := by cat_disch) (hε : ∀ (X₂ : C₂), CategoryStruct.comp (G'.map (β.app X₂)) (ε.app (L₂.obj X₂)) = CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)) := by cat_disch) : (adj.derived' W₁ W₂ α β η ε hη hε).counit = ε

@[simp]

theorem CategoryTheory.Adjunction.derived'_unit {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂] (η : Functor.id D₁ ⟶ G'.comp F') (ε : F'.comp G' ⟶ Functor.id D₂) (hη : ∀ (X₁ : C₁), CategoryStruct.comp (η.app (L₁.obj X₁)) (F'.map (α.app X₁)) = CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁)) := by cat_disch) (hε : ∀ (X₂ : C₂), CategoryStruct.comp (G'.map (β.app X₂)) (ε.app (L₂.obj X₂)) = CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂)) := by cat_disch) : (adj.derived' W₁ W₂ α β η ε hη hε).unit = η

noncomputable def CategoryTheory.Adjunction.derivedη {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [(G'.comp F').IsLeftDerivedFunctor (CategoryStruct.comp (L₁.associator G' F').inv (Functor.whiskerRight α F')) W₁] : Functor.id D₁ ⟶ G'.comp F'

The unit of the derived adjunction, see Adjunction.derived.

@[simp]

theorem CategoryTheory.Adjunction.derivedη_fac_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_6, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_5, u_3} D₁] [Category.{u_7, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [(G'.comp F').IsLeftDerivedFunctor (CategoryStruct.comp (L₁.associator G' F').inv (Functor.whiskerRight α F')) W₁] (X₁ : C₁) : CategoryStruct.comp ((adj.derivedη W₁ α β).app (L₁.obj X₁)) (F'.map (α.app X₁)) = CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (β.app (G.obj X₁))

@[simp]

theorem CategoryTheory.Adjunction.derivedη_fac_app_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_6, u_1} C₁] [Category.{u_8, u_2} C₂] [Category.{u_5, u_3} D₁] [Category.{u_7, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) [L₁.IsLocalization W₁] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [(G'.comp F').IsLeftDerivedFunctor (CategoryStruct.comp (L₁.associator G' F').inv (Functor.whiskerRight α F')) W₁] (X₁ : C₁) {Z : D₁} (h : F'.obj (L₂.obj (G.obj X₁)) ⟶ Z) : CategoryStruct.comp ((adj.derivedη W₁ α β).app (L₁.obj X₁)) (CategoryStruct.comp (F'.map (α.app X₁)) h) = CategoryStruct.comp (L₁.map (adj.unit.app X₁)) (CategoryStruct.comp (β.app (G.obj X₁)) h)

noncomputable def CategoryTheory.Adjunction.derivedε {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₂ : MorphismProperty C₂) [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [(F'.comp G').IsRightDerivedFunctor (CategoryStruct.comp (Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂] : F'.comp G' ⟶ Functor.id D₂

The counit of the derived adjunction, see Adjunction.derived.

@[simp]

theorem CategoryTheory.Adjunction.derivedε_fac_app {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_7, u_2} C₂] [Category.{u_6, u_3} D₁] [Category.{u_5, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₂ : MorphismProperty C₂) [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [(F'.comp G').IsRightDerivedFunctor (CategoryStruct.comp (Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂] (X₂ : C₂) : CategoryStruct.comp (G'.map (β.app X₂)) ((adj.derivedε W₂ α β).app (L₂.obj X₂)) = CategoryStruct.comp (α.app (F.obj X₂)) (L₂.map (adj.counit.app X₂))

@[simp]

theorem CategoryTheory.Adjunction.derivedε_fac_app_assoc {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_8, u_1} C₁] [Category.{u_7, u_2} C₂] [Category.{u_6, u_3} D₁] [Category.{u_5, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₂ : MorphismProperty C₂) [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [(F'.comp G').IsRightDerivedFunctor (CategoryStruct.comp (Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂] (X₂ : C₂) {Z : D₂} (h : L₂.obj X₂ ⟶ Z) : CategoryStruct.comp (G'.map (β.app X₂)) (CategoryStruct.comp ((adj.derivedε W₂ α β).app (L₂.obj X₂)) h) = CategoryStruct.comp (α.app (F.obj X₂)) (CategoryStruct.comp (L₂.map (adj.counit.app X₂)) h)

noncomputable def CategoryTheory.Adjunction.derived {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂] [(G'.comp F').IsLeftDerivedFunctor (CategoryStruct.comp (L₁.associator G' F').inv (Functor.whiskerRight α F')) W₁] [(F'.comp G').IsRightDerivedFunctor (CategoryStruct.comp (Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂] : G' ⊣ F'

An adjunction between functors induces an adjunction between the corresponding left/right derived functors, when these derived functors are absolute, i.e. they remain derived functors after the post-composition with any functor.

(One actually only needs that G' ⋙ F' is the left derived functor of G ⋙ L₂ ⋙ F' and that F' ⋙ G' is the right derived functor of F ⋙ L₁ ⋙ G').

@[simp]

theorem CategoryTheory.Adjunction.derived_unit {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂] [(G'.comp F').IsLeftDerivedFunctor (CategoryStruct.comp (L₁.associator G' F').inv (Functor.whiskerRight α F')) W₁] [(F'.comp G').IsRightDerivedFunctor (CategoryStruct.comp (Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂] : (adj.derived W₁ W₂ α β).unit = adj.derivedη W₁ α β

@[simp]

theorem CategoryTheory.Adjunction.derived_counit {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [Category.{u_5, u_1} C₁] [Category.{u_6, u_2} C₂] [Category.{u_7, u_3} D₁] [Category.{u_8, u_4} D₂] {G : Functor C₁ C₂} {F : Functor C₂ C₁} (adj : G ⊣ F) {L₁ : Functor C₁ D₁} {L₂ : Functor C₂ D₂} (W₁ : MorphismProperty C₁) (W₂ : MorphismProperty C₂) [L₁.IsLocalization W₁] [L₂.IsLocalization W₂] {G' : Functor D₁ D₂} {F' : Functor D₂ D₁} (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [G'.IsLeftDerivedFunctor α W₁] [F'.IsRightDerivedFunctor β W₂] [(G'.comp F').IsLeftDerivedFunctor (CategoryStruct.comp (L₁.associator G' F').inv (Functor.whiskerRight α F')) W₁] [(F'.comp G').IsRightDerivedFunctor (CategoryStruct.comp (Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂] : (adj.derived W₁ W₂ α β).counit = adj.derivedε W₂ α β