postAdjunctionRight

Mathlib.CategoryTheory.Comma.Over.Pullback

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Under.postAdjunctionRight

Lean4

/-- 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)`. -/
@[simps!]
def postAdjunctionRight [HasPushouts D] {Y : D} {F : C ⥤ D} {G : D ⥤ C} (a : F ⊣ G) :
    post F ⋙ pushout (a.counit.app Y) ⊣ post G :=
  ((postAdjunctionLeft a).comp (mapPushoutAdj (a.counit.app Y))).ofNatIsoRight <|
    NatIso.ofComponents fun Y ↦ isoMk (.refl _)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru