Theorems · Definition · category theory

CategoryTheory.Under.postAdjunctionRight

{C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasPushouts D] →
          {Y : D} →
            {F : CategoryTheory.Functor C D} →
              {G : CategoryTheory.Functor D C} →
                (a : F ⊣ G) →
                  (CategoryTheory.Under.post F).comp (CategoryTheory.Under.pushout (a.counit.app Y)) ⊣
                    CategoryTheory.Under.post G

If G is a right adjoint and its source category has pushouts, then so is post G : Under Y ⥤ Under (G Y). If the left adjoint of G is F, then the left adjoint of post G is given by (G Y ⟶ X) ↦ (Y ⟶ Y ⨿_{F G Y} F X ⟶ F X).

Defined in

Mathlib.CategoryTheory.Comma.Over.Pullback

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasPushouts