Theorems · Theorem · category theory

CategoryTheory.Over.postAdjunctionLeft_counit_app_left

∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X : C} {F : CategoryTheory.Functor C D}
  {G : CategoryTheory.Functor D C} (a : F ⊣ G)
  (X_1 : CategoryTheory.Over ((CategoryTheory.Functor.id D).obj (F.obj X))),
  ((CategoryTheory.Over.postAdjunctionLeft a).counit.app X_1).left =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Limits.pullback.fst (G.map X_1.hom) (a.unit.app X)))
      (a.counit.app X_1.left)

Defined in

Mathlib.CategoryTheory.Comma.Over.Pullback

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasPullbacks