colimitCompWhiskeringRightIsoColimitComp

Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

URI: https://scilib.ai/kg/mathlib#CategoryTheory.colimitCompWhiskeringRightIsoColimitComp

Lean4

/-- Whiskering right and then taking a colimit is the same as taking the colimit and applying the
functor. -/
def colimitCompWhiskeringRightIsoColimitComp {C : Type*} [Category C] {D : Type*} [Category D] {E : Type*} [Category E]
    {J : Type*} [Category J] [HasColimitsOfShape J D] (F : D ⥤ E) [PreservesColimitsOfShape J F] (G : J ⥤ C ⥤ D) :
    colimit (G ⋙ (whiskeringRight _ _ _).obj F) ≅ colimit G ⋙ F :=
  (preservesColimitIso _ _).symm

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

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

Разделы

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

Аффилиация

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