Commit 2022-12-03 19:18 31019c25
View on Github →feat(category_theory/idempotents): an equivalence of categories for homological complexes (#17569)
This PR constructs an equivalence of categories karoubi_homological_complex_equivalence C c : karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c. The automation for karoubi categories is also made better by the introduction of the simp lemma karoubi.comp_f.