mathlib documentation

category_theory.idempotents.simplicial_object

Idempotent completeness of categories of simplicial objects #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file, we provide an instance expressing that simplicial_object C and cosimplicial_object C are idempotent complete categories when the category C is.

source
@[protected, instance]
def category_theory.idempotents.category_theory.simplicial_object.category_theory.is_idempotent_complete {C : Type u_1} [category_theory.category C] [category_theory.is_idempotent_complete C] :
category_theory.is_idempotent_complete (category_theory.simplicial_object C)
source
@[protected, instance]
def category_theory.idempotents.category_theory.cosimplicial_object.category_theory.is_idempotent_complete {C : Type u_1} [category_theory.category C] [category_theory.is_idempotent_complete C] :
category_theory.is_idempotent_complete (category_theory.cosimplicial_object C)