mathlib documentation


Idempotent completeness and homological complexes #

This file contains simplifications lemmas for categories karoubi (homological_complex C c) and the construction of an equivalence of categories karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c.

When the category C is idempotent complete, it is shown that homological_complex (karoubi C) c is also idempotent complete.

theorem category_theory.idempotents.karoubi.homological_complex.p_comm_f_assoc {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} {P Q : category_theory.idempotents.karoubi (homological_complex C c)} (f : P Q) (n : ι) {X' : C} (f' : Q.X.X n X') :
P.p.f n f.f.f n f' = f.f.f n Q.p.f n f'