Theorems · Theorem · category theory

CategoryTheory.Adjunction.leftAdjointCompIso_comp_id

∀ {C₀ : Type u_1} {C₁ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₀]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₁] {F₀₁ : CategoryTheory.Functor C₀ C₁}
  {F₁₁' : CategoryTheory.Functor C₁ C₁} {G₁₀ : CategoryTheory.Functor C₁ C₀} {G₁'₁ : CategoryTheory.Functor C₁ C₁}
  (adj₀₁ : F₀₁ ⊣ G₁₀) (adj₁₁' : F₁₁' ⊣ G₁'₁) (e₀₁₁' : G₁'₁.comp G₁₀ ≅ G₁₀) (e₁'₁ : G₁'₁ ≅ CategoryTheory.Functor.id C₁),
  e₀₁₁' = CategoryTheory.Functor.isoWhiskerRight e₁'₁ G₁₀ ≪≫ G₁₀.leftUnitor →
    adj₀₁.leftAdjointCompIso adj₁₁' adj₀₁ e₀₁₁' = F₀₁.isoWhiskerLeft (adj₁₁'.leftAdjointIdIso e₁'₁) ≪≫ F₀₁.rightUnitor

Defined in

Mathlib.CategoryTheory.Adjunction.CompositionIso

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Category