functorToInterchange

Mathlib.CategoryTheory.Limits.Preserves.Presheaf

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

← MathLib Explorer

Lean4

/-- (Implementation) This is the bifunctor we will apply "filtered colimits commute with finite
limits" to. -/
def functorToInterchange : J ⥤ CostructuredArrow yoneda A ⥤ Type u :=
  K ⋙ coyoneda ⋙ (whiskeringLeft _ _ _).obj (CostructuredArrow.proj _ _)

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

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

Разделы

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

Аффилиация

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