toOver

Mathlib.CategoryTheory.Limits.ConeCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cocone.toOver

Lean4

/-- A cocone `c` on `F : J ⥤ C` lifts to a cocone in `Over c.pt` with cone point `𝟙 c.pt`. -/
@[simps]
def toOver {F : J ⥤ C} (c : Cocone F) : Cocone (c.toCostructuredArrow ⋙ CostructuredArrow.toOver _ _)
    where
  pt := Over.mk (𝟙 c.pt)
  ι := { app := fun j => Over.homMk (c.ι.app j) (by simp) }

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

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

Разделы

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

Аффилиация

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