categoryStruct

Mathlib.CategoryTheory.Bicategory.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Pseudofunctor.Grothendieck.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 ⟨X.base⟩).hom.app X.fiber }
  comp {X _ _} f
    g :=
    { base := f.base ≫ g.base
      fiber := (F.mapComp f.base.toLoc g.base.toLoc).hom.app X.fiber ≫ (F.map g.base.toLoc).map f.fiber ≫ g.fiber }

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

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

Разделы

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

Аффилиация

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