instPreservesFiniteLimitsFunctorColimOfPreservesColimitsOfShapeOfHasFiniteLimitsOfReflectsIsomorphismsForget

English

If K is filtered and J is finite, the colimit over K of Type-valued diagrams preserves finite limits.

Русский

Если K фильтрована и J конечна, колимит над K для диаграмм в Type сохраняет конечные пределы.

LaTeX

$$PreservesFiniteLimits (colim : (K ⥤ Type v) ⥤ _)$$

Lean4

noncomputable instance [PreservesFiniteLimits (forget C)] [PreservesColimitsOfShape K (forget C)] [HasFiniteLimits C]
    [HasColimitsOfShape K C] [(forget C).ReflectsIsomorphisms] : PreservesFiniteLimits (colim : (K ⥤ C) ⥤ _) :=
  by
  apply preservesFiniteLimits_of_preservesFiniteLimitsOfSize.{v}
  intro J _ _
  infer_instance

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