extensions

Mathlib.CategoryTheory.Limits.Cones

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cone.extensions

Lean4

/-- A map to the vertex of a cone naturally induces a cone by composition. -/
@[simps]
def extensions (c : Cone F) : yoneda.obj c.pt ⋙ uliftFunctor.{u₁} ⟶ F.cones where app _ f := (const J).map f.down ≫ c.π

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

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

Разделы

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

Аффилиация

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