preservesColimitsOfShapeOfPreservesFiniteColimits

English

If F preserves finite colimits, then F preserves colimits of any finite shape J.

Русский

Если F сохраняет конечные колимиты, то F сохраняет колимиты по любой конечной форме J.

LaTeX

$$$\forall J\, [\text{SmallCategory } J] [\text{FinCategory } J], \; \mathrm{PreservesColimitsOfShape}(J, F)$$$

Lean4

/-- Preserving finite colimits also implies preserving colimits over finite shapes in higher
universes.
-/
instance (priority := 100) preservesColimitsOfShapeOfPreservesFiniteColimits (F : C ⥤ D) [PreservesFiniteColimits F]
    (J : Type w) [SmallCategory J] [FinCategory J] : PreservesColimitsOfShape J F := by
  apply
    preservesColimitsOfShape_of_equiv
      (FinCategory.equivAsType J)
        -- This is a dangerous instance as it has unbound universe variables.

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