diagram

Mathlib.CategoryTheory.GlueData

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GlueData.diagram

Lean4

/-- (Implementation) The diagram to take colimit of. -/
def diagram : MultispanIndex (.prod D.J) C where
  left := D.V
  right := D.U
  fst := fun ⟨i, j⟩ => D.f i j
  snd := fun ⟨i, j⟩ => D.t i j ≫ D.f j i

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

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

Разделы

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

Аффилиация

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