instIsIdempotentCompleteCosimplicialObject

English

If C is idempotent-complete, then the category of cosimplicial objects in C is idempotent-complete.

Русский

Если в категории C каждый идемпотент распадается, то категория косимпликсов объектов в C также распадается.

LaTeX

$$$\\operatorname{IsIdempotentComplete}(\\operatorname{CosimplicialObject}(C))$$$

Lean4

instance : IsIdempotentComplete (CosimplicialObject C) :=
  Idempotents.functor_category_isIdempotentComplete _ _

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