Theorems · Theorem · category theory

CategoryTheory.Adjunction.leftAdjointCompNatTrans_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₃₀) (τ₀₁₂ : G₂₀ ⟶ G₂₁.comp G₁₀)
  (τ₁₂₃ : G₃₁ ⟶ G₃₂.comp G₂₁) (τ₀₁₃ : G₃₀ ⟶ G₃₁.comp G₁₀) (τ₀₂₃ : G₃₀ ⟶ G₃₂.comp G₂₀),
  CategoryTheory.CategoryStruct.comp τ₀₂₃ (G₃₂.whiskerLeft τ₀₁₂) =
      CategoryTheory.CategoryStruct.comp τ₀₁₃
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight τ₁₂₃ G₁₀)
          (G₃₂.associator G₂₁ G₁₀).hom) →
    CategoryTheory.CategoryStruct.comp (F₀₁.whiskerLeft (adj₁₂.leftAdjointCompNatTrans adj₂₃ adj₁₃ τ₁₂₃))
        (adj₀₁.leftAdjointCompNatTrans adj₁₃ adj₀₃ τ₀₁₃) =
      CategoryTheory.CategoryStruct.comp (F₀₁.associator F₁₂ F₂₃).inv
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.whiskerRight (adj₀₁.leftAdjointCompNatTrans adj₁₂ adj₀₂ τ₀₁₂) F₂₃)
          (adj₀₂.leftAdjointCompNatTrans adj₂₃ adj₀₃ τ₀₂₃))

Defined in

Mathlib.CategoryTheory.Adjunction.CompositionIso

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category