categoryStruct

Mathlib.CategoryTheory.Bicategory.Grothendieck

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

Lean4

@[simps! id_base id_fiber comp_base comp_fiber]
instance categoryStruct : CategoryStruct (∫ᶜ F)
    where
  Hom X Y := Hom X Y
  id
    X :=
    { base := 𝟙 X.base
      fiber := (F.mapId ⟨op X.base⟩).inv.app X.fiber }
  comp {_ _ Z} f
    g :=
    { base := f.base ≫ g.base
      fiber :=
        f.fiber ≫ (F.map f.base.op.toLoc).map g.fiber ≫ (F.mapComp g.base.op.toLoc f.base.op.toLoc).inv.app Z.fiber }

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

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

Разделы

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

Аффилиация

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