Theorems · Definition · category theory

CategoryTheory.Over.postAdjunctionLeft

{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) →
                  CategoryTheory.Over.post F ⊣
                    (CategoryTheory.Over.post G).comp (CategoryTheory.Over.pullback (a.unit.app X))

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

Defined in

Mathlib.CategoryTheory.Comma.Over.Pullback

Cited by

2 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.HasPullbacks