instHasColimitsOfShape — Mathlib

English

For any J, if C has colimits of shape J, then CosimplicialObject C has colimits of shape J.

Русский

Пусть J — любая форма, тогда если в C существуют колиминты формы J, то CosimplicialObject C имеет колиминты формы J.

LaTeX

$$$\text{HasColimitsOfShape } J\,\big(\mathrm{CosimplicialObject}\,C\big)$$$

Lean4

instance {J : Type v} [SmallCategory J] [HasColimitsOfShape J C] : HasColimitsOfShape J (CosimplicialObject C) :=
  by
  dsimp [CosimplicialObject]
  infer_instance

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