Theorems · Theorem · category theory

CategoryTheory.Adjunction.leftAdjointCompIso_inv_app

∀ {C₀ : Type u_1} {C₁ : Type u_2} {C₂ : Type u_3} [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₂]
  {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₀}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₂ : F₁₂ ⊣ G₂₁) (adj₀₂ : F₀₂ ⊣ G₂₀) (e₀₁₂ : G₂₁.comp G₁₀ ≅ G₂₀) (X : C₀),
  (adj₀₁.leftAdjointCompIso adj₁₂ adj₀₂ e₀₁₂).inv.app X =
    CategoryTheory.CategoryStruct.comp (F₀₂.map (adj₀₁.unit.app X))
      (CategoryTheory.CategoryStruct.comp (F₀₂.map (G₁₀.map (adj₁₂.unit.app (F₀₁.obj X))))
        (CategoryTheory.CategoryStruct.comp (F₀₂.map (e₀₁₂.hom.app (F₁₂.obj (F₀₁.obj X))))
          (adj₀₂.counit.app (F₁₂.obj (F₀₁.obj X)))))

Defined in

Mathlib.CategoryTheory.Adjunction.CompositionIso

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category