category

Mathlib.CategoryTheory.Bicategory.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.CoGrothendieck.category

Lean4

/-- The category structure on `∫ᶜ F`. -/
instance category : Category (∫ᶜ F)
    where
  toCategoryStruct := Pseudofunctor.CoGrothendieck.categoryStruct
  id_comp {a b}
    f := by
    ext
    · simp
    · simp [F.mapComp_id_right_inv_app, Strict.rightUnitor_eqToIso, ← NatTrans.naturality_assoc]
  comp_id {a b}
    f := by
    ext
    · simp
    · simp [F.mapComp_id_left_inv_app, ← Functor.map_comp_assoc, Strict.leftUnitor_eqToIso]
  assoc f g
    h := by
    ext
    · simp
    · simp [← NatTrans.naturality_assoc, F.mapComp_assoc_right_inv_app, Strict.associator_eqToIso]

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

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

Разделы

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

Аффилиация

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