fiberwiseColimCompEvaluationIso

Mathlib.CategoryTheory.Limits.Shapes.Grothendieck

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.fiberwiseColimCompEvaluationIso

Lean4

/-- Composing `fiberwiseColim F H` with the evaluation functor `(evaluation C H).obj c` is
naturally isomorphic to precomposing the Grothendieck inclusion `Grothendieck.ι` to `colim`. -/
@[simps!]
def fiberwiseColimCompEvaluationIso (c : C) :
    fiberwiseColim F H ⋙ (evaluation C H).obj c ≅ (whiskeringLeft _ _ _).obj (Grothendieck.ι F c) ⋙ colim :=
  Iso.refl _

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

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

Разделы

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

Аффилиация

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