colimitLimitIso — Mathlib

English

If C has products and filtered colimits and is IPC, then any functor D ⥤ C is IPC.

Русский

Если в C есть произведения и фильтрованные колимиты и C имеет свойство IPC, тогда любая категория-функтор D ⥤ C также имеет IPC.

LaTeX

$$[IsIPC on functors] IsIPC (D ⥤ C)$$

Lean4

/-- A curried version of the fact that filtered colimits commute with finite limits. -/
noncomputable def colimitLimitIso (F : J ⥤ K ⥤ C) : colimit (limit F) ≅ limit (colimit F.flip) :=
  (isLimitOfPreserves colim (limit.isLimit _)).conePointUniqueUpToIso (limit.isLimit _) ≪≫
    HasLimit.isoOfNatIso (colimitFlipIsoCompColim _).symm

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