mkInitialOfLeftAdjoint

Mathlib.CategoryTheory.Adjunction.Comma

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

Lean4

/-- Given a left adjoint to `G`, we can construct an initial object in each structured arrow
category on `G`. -/
def mkInitialOfLeftAdjoint (h : F ⊣ G) (A : C) : IsInitial (StructuredArrow.mk (h.unit.app A) : StructuredArrow A G)
    where
  desc B := StructuredArrow.homMk ((h.homEquiv _ _).symm B.pt.hom)
  uniq s m
    _ := by
    apply StructuredArrow.ext
    simp [← StructuredArrow.w m]

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

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

Разделы

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

Аффилиация

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