hasColimit_of_hasColimit_comp_forget

English

For any J, if C has colimits of shape J, then the over category Over X also has colimits of shape J.

Русский

Для любой формы J, если в C существуют колимиты формы J, то в категориях Over X существуют колимиты формы J.

LaTeX

$$$ [\\text{HasColimits}(J,C)] \\Rightarrow \\text{HasColimits}(J,\\mathrm{Over}(X)). $$$

Lean4

instance hasColimit_of_hasColimit_comp_forget (F : J ⥤ Over X) [i : HasColimit (F ⋙ forget X)] : HasColimit F :=
  CostructuredArrow.hasColimit (i₁ := i)

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