Theorems · Theorem · category theory

CategoryTheory.Adjunction.derived_counit

∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂] {G : CategoryTheory.Functor C₁ C₂} {F : CategoryTheory.Functor C₂ C₁}
  (adj : G ⊣ F) {L₁ : CategoryTheory.Functor C₁ D₁} {L₂ : CategoryTheory.Functor C₂ D₂}
  (W₁ : CategoryTheory.MorphismProperty C₁) (W₂ : CategoryTheory.MorphismProperty C₂) [inst_4 : L₁.IsLocalization W₁]
  [inst_5 : L₂.IsLocalization W₂] {G' : CategoryTheory.Functor D₁ D₂} {F' : CategoryTheory.Functor D₂ D₁}
  (α : L₁.comp G' ⟶ G.comp L₂) (β : F.comp L₁ ⟶ L₂.comp F') [inst_6 : G'.IsLeftDerivedFunctor α W₁]
  [inst_7 : F'.IsRightDerivedFunctor β W₂]
  [inst_8 :
    (G'.comp F').IsLeftDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (L₁.associator G' F').inv (CategoryTheory.Functor.whiskerRight α F')) W₁]
  [inst_9 :
    (F'.comp G').IsRightDerivedFunctor
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight β G') (L₂.associator F' G').hom) W₂],
  (adj.derived W₁ W₂ α β).counit = adj.derivedε W₂ α β

Defined in

Mathlib.CategoryTheory.Functor.Derived.Adjunction

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLocalizationCategoryTheory.Functor.IsLeftDerivedFunctorCategoryTheory.Functor.IsRightDerivedFunctorCategoryTheory.Functor.IsLeftDerivedFunctorCategoryTheory.Functor.IsRightDerivedFunctor