mkCommaObject

Mathlib.CategoryTheory.WithTerminal.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.WithTerminal.mkCommaObject

Lean4

/-- A functor `WithTerminal C ⥤ D` can be seen as an element of the comma category
`Comma (𝟭 (C ⥤ D)) (const C)`. -/
@[simps!]
def mkCommaObject (F : WithTerminal C ⥤ D) : Comma (𝟭 (C ⥤ D)) (Functor.const C)
    where
  right := F.obj .star
  left := (incl ⋙ F)
  hom :=
    { app x := F.map (starTerminal.from (.of x))
      naturality x y
        f := by
        dsimp
        rw [Category.comp_id, ← F.map_comp]
        congr 1 }

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

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

Разделы

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

Аффилиация

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