fromStructuredArrow

Mathlib.CategoryTheory.Limits.ConeCategory

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

Lean4

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

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

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

Разделы

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

Аффилиация

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