forgetMapTerminal

Mathlib.CategoryTheory.Comma.Over.Pullback

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.forgetMapTerminal

Lean4

/-- The category over any object `X` factors through the category over the terminal object `T`. -/
@[simps!]
noncomputable def forgetMapTerminal {T : C} (hT : IsTerminal T) :
    forget X ≅ map (hT.from X) ⋙ (equivalenceOfIsTerminal hT).functor :=
  NatIso.ofComponents fun X ↦ .refl _

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

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

Разделы

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

Аффилиация

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