CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem

theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι), CategoryTheory.CategoryStruct.comp (P.p.f n) (P.p.f n) = P.p.f n

This theorem states that for any category `C` (which is also a preadditive category), any complex shape `c`, any Karoubi envelope `P` of the homological complex of `C` and `c`, and any index `n`, the composition of the morphism `P.p.f n` with itself (denoted by `P.p.f n ≫ P.p.f n` in category theory) is equal to `P.p.f n` itself. This is a property of idempotents, elements that remain unchanged when squared, in the context of categories and homological complexes.

More concisely: In any preadditive category `C` with homological complex `c` and its Karoubi envelope `P`, the morphism `P.p.f n` is idempotent, that is, `P.p.f n ≫ P.p.f n = P.p.f n`.