instHasLimitsOfShape — Mathlib

English

If J is a small category and C has limits of shape J, then the truncated cosimplicial category CosimplicialObject.Truncated C n also has limits of shape J. In other words, limits commute with the truncation process for truncated cosimplicial objects.

Русский

Если J — маленькая категория и в C существуют пределы по форме J, то уcечённая категория CosimplicialObject.Truncated C n также имеет пределы по форме J.

LaTeX

$$$\\forall C [\\text{Category } C], \\forall n\\in\\mathbb{N}, \\forall J : Type, [SmallCategory J], [HasLimitsOfShape J C] \\, \\Rightarrow \\, HasLimitsOfShape J (\\mathrm{CosimplicialObject.Truncated}\; C\\ n).$$$

Lean4

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

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