mathlib documentation


Idempotent completeness and homological complexes #

This file contains simplifications lemmas for categories karoubi (homological_complex C c).

TODO @joelriou : Get an equivalence of categories karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c for all preadditive categories C and complex shape c.

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'