mkTerminalOfRightAdjoint

Mathlib.CategoryTheory.Adjunction.Comma

URI: https://scilib.ai/kg/mathlib#CategoryTheory.mkTerminalOfRightAdjoint

Lean4

/-- Given a right adjoint to `F`, we can construct a terminal object in each costructured arrow
category on `F`. -/
def mkTerminalOfRightAdjoint (h : F ⊣ G) (A : D) :
    IsTerminal (CostructuredArrow.mk (h.counit.app A) : CostructuredArrow F A)
    where
  lift B := CostructuredArrow.homMk (h.homEquiv _ _ B.pt.hom)
  uniq s m
    _ := by
    apply CostructuredArrow.ext
    simp [← CostructuredArrow.w m]

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

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

Разделы

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

Аффилиация

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