Theorems · Theorem · category theory

CategoryTheory.Adjunction.leftAdjointCompIso_hom_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₀₁₂).hom.app X =
    CategoryTheory.CategoryStruct.comp (F₁₂.map (F₀₁.map (adj₀₂.unit.app X)))
      (CategoryTheory.CategoryStruct.comp (F₁₂.map (F₀₁.map (e₀₁₂.inv.app (F₀₂.obj X))))
        (CategoryTheory.CategoryStruct.comp (F₁₂.map (adj₀₁.counit.app (G₂₁.obj (F₀₂.obj X))))
          (adj₁₂.counit.app (F₀₂.obj X))))

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.Category