limitCompWhiskeringRightIsoLimitComp

Mathlib.CategoryTheory.Limits.Preserves.FunctorCategory

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

Lean4

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

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

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

Разделы

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

Аффилиация

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