Theorems · Theorem · category theory

CategoryTheory.Adjunction.leftAdjointCompIso_assoc

∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} {C₃ : 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} C₂]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} C₃] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₂ : CategoryTheory.Functor C₁ C₂} {F₂₃ : CategoryTheory.Functor C₂ C₃} {F₀₂ : CategoryTheory.Functor C₀ C₂}
  {F₁₃ : CategoryTheory.Functor C₁ C₃} {F₀₃ : CategoryTheory.Functor C₀ C₃} {G₁₀ : CategoryTheory.Functor C₁ C₀}
  {G₂₁ : CategoryTheory.Functor C₂ C₁} {G₃₂ : CategoryTheory.Functor C₃ C₂} {G₂₀ : CategoryTheory.Functor C₂ C₀}
  {G₃₁ : CategoryTheory.Functor C₃ C₁} {G₃₀ : CategoryTheory.Functor C₃ C₀} (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁)
  (adj₂₃ : F₂₃ ⊣ G₃₂) (adj₀₂ : F₀₂ ⊣ G₂₀) (adj₁₃ : F₁₃ ⊣ G₃₁) (adj₀₃ : F₀₃ ⊣ G₃₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀)
  (e₁₂₃ : G₃₂.comp G₂₁ ≅ G₃₁) (e₀₁₃ : G₃₁.comp G₁₀ ≅ G₃₀) (e₀₂₃ : G₃₂.comp G₂₀ ≅ G₃₀),
  G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ =
      (G₃₂.associator G₂₁ G₁₀).symm ≪≫ CategoryTheory.Functor.isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃ →
    F₀₁.isoWhiskerLeft (adj₁₂.leftAdjointCompIso adj₂₃ adj₁₃ e₁₂₃) ≪≫ adj₀₁.leftAdjointCompIso adj₁₃ adj₀₃ e₀₁₃ =
      (F₀₁.associator F₁₂ F₂₃).symm ≪≫
        CategoryTheory.Functor.isoWhiskerRight (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂) F₂₃ ≪≫
          adj₀₂.leftAdjointCompIso adj₂₃ adj₀₃ e₀₂₃

Defined in

Mathlib.CategoryTheory.Adjunction.CompositionIso

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category