instHasLimitsOfShape — Mathlib

English

Let J be a small category. If C has limits of shape J, then CosimplicialObject C has limits of shape J; equivalently, the functor category Fun(J, CosimplicialObject C) has limits computed pointwise from C.

Русский

Пусть J — малая категория. Если в категории C существуют пределы по форме J, то в CosimplicialObject C существуют пределы по форме J; эквивалентно, категория-функторов Fun(J, CosimplicialObject C) имеет пределы, вычисляемые по точкам в C.

LaTeX

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

Lean4

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

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