instIsIPCFunctor — Mathlib

English

If C has products, filtered colimits, and IsIPC, then the functor category D ⥤ C also has IsIPC.

Русский

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

LaTeX

$$IsIPC (D ⥤ C)$$

Lean4

instance [HasProducts.{w} C] [HasFilteredColimitsOfSize.{w, w} C] [IsIPC.{w} C] {D : Type u₁} [Category.{v₁} D] :
    IsIPC.{w} (D ⥤ C) := by
  refine ⟨fun β I _ _ F => ?_⟩
  suffices ∀ d, IsIso ((colimitPointwiseProductToProductColimit F).app d) from NatIso.isIso_of_isIso_app _
  exact fun d => colimitPointwiseProductToProductColimit_app F d ▸ inferInstance

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