fromCostructuredArrow

Mathlib.CategoryTheory.Limits.ConeCategory

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

Lean4

/-- Given a diagram `CostructuredArrow F X`s, we may obtain a cocone with cone point `X`. -/
@[simps!]
def fromCostructuredArrow (F : C ⥤ D) {X : D} (G : J ⥤ CostructuredArrow F X) :
    Cocone (G ⋙ CostructuredArrow.proj F X ⋙ F) where
  pt := X
  ι := { app := fun j => (G.obj j).hom }

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

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

Разделы

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

Аффилиация

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