instCategoryStruct

Mathlib.AlgebraicTopology.SimplicialNerve

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SimplicialThickening.instCategoryStruct

Lean4

@[simps]
instance (J : Type*) [LinearOrder J] : CategoryStruct (SimplicialThickening J)
    where
  Hom i j := Path i j
  id i := { I := { i } }
  comp {i j k} f
    g :=
    { I := f.I ∪ g.I
      left := Or.inl f.left
      right := Or.inr g.right
      left_le
        l := by
        rintro (h | h)
        exacts [(f.left_le l h), (Path.le f).trans (g.left_le l h)]
      le_right
        l := by
        rintro (h | h)
        exacts [(f.le_right _ h).trans (Path.le g), (g.le_right l h)] }

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

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

Разделы

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

Аффилиация

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