functorCategoryHasColimitsOfSize — Mathlib

English

If C has all colimits of a given size, then the functor category K ⥤ C also has all colimits of that same size.

Русский

Если в категории C существуют все колимиты заданного размера, то категория функторов K ⥤ C также имеет все колимиты этого размера.

LaTeX

$$$\operatorname{HasColimitsOfSize}(C) \Rightarrow \operatorname{HasColimitsOfSize}(K \to C)$$$

Lean4

instance functorCategoryHasColimitsOfSize [HasColimitsOfSize.{v₁, u₁} C] : HasColimitsOfSize.{v₁, u₁} (K ⥤ C) where
  has_colimits_of_shape := inferInstance

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