Magnitude conjecture

MagnitudeConjecture.CategoryTheory.IdempotentCompleteFullSubcategory

Idempotent completeness of retract-stable full subcategories #

A full subcategory cut out by a retract-stable object property inherits idempotent completeness from its ambient category. The splitting object is the ambient retract selected by the idempotent.

source
theorem MagnitudeConjecture.isIdempotentComplete_fullSubcategory_of_stableUnderRetracts {C : Type u} [CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts] [CategoryTheory.IsIdempotentComplete C] :
CategoryTheory.IsIdempotentComplete P.FullSubcategory

A retract-stable full subcategory of an idempotent-complete category is idempotent-complete.