compAsSmallFunctorEquivalence

Mathlib.CategoryTheory.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Grothendieck.compAsSmallFunctorEquivalence

Lean4

/-- Taking the Grothendieck construction on `F ⋙ asSmallFunctor`, where
`asSmallFunctor : Cat ⥤ Cat` is the functor which turns each category into a small category of a
(potentially) larger universe, is equivalent to the Grothendieck construction on `F` itself. -/
@[simps]
def compAsSmallFunctorEquivalence : Grothendieck (F ⋙ Cat.asSmallFunctor.{w}) ≌ Grothendieck F
    where
  functor := compAsSmallFunctorEquivalenceFunctor F
  inverse := compAsSmallFunctorEquivalenceInverse F
  counitIso := Iso.refl _
  unitIso := Iso.refl _

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

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

Разделы

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

Аффилиация

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