mathlib3 documentation

category_theory.idempotents.homological_complex

Idempotent completeness and homological complexes #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source
@[simp]
theorem category_theory.idempotents.karoubi.homological_complex.p_comp_d_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 ≫ f'
source
@[simp]
theorem category_theory.idempotents.karoubi.homological_complex.p_comp_d {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 : ι) :
P.p.f n ≫ f.f.f n = f.f.f n
source
@[simp]
theorem category_theory.idempotents.karoubi.homological_complex.comp_p_d {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 : ι) :
f.f.f n ≫ Q.p.f n = f.f.f n
source
@[simp]
theorem category_theory.idempotents.karoubi.homological_complex.comp_p_d_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') :
f.f.f n ≫ Q.p.f n ≫ f' = f.f.f n ≫ f'
source
theorem category_theory.idempotents.karoubi.homological_complex.p_comm_f {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 : ι) :
P.p.f n ≫ f.f.f n = f.f.f n ≫ Q.p.f n
source
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'
source
@[simp]
theorem category_theory.idempotents.karoubi.homological_complex.p_idem_assoc {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (n : ι) {X' : C} (f' : P.X.X n ⟶ X') :
P.p.f n ≫ P.p.f n ≫ f' = P.p.f n ≫ f'
source
@[simp]
theorem category_theory.idempotents.karoubi.homological_complex.p_idem {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (n : ι) :
P.p.f n ≫ P.p.f n = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj_d_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (i j : ι) :
((category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj P).d i j).f = P.p.f i ≫ P.X.d i j
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj_X_p {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (n : ι) :
((category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj P).X n).p = P.p.f n
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) :
homological_complex (category_theory.idempotents.karoubi C) c

The functor karoubi (homological_complex C c) ⥤ homological_complex (karoubi C) c, on objects.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj_X_X {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (n : ι) :
((category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj P).X n).X = P.X.X n
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.functor.map_f_f {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 : ι) :
((category_theory.idempotents.karoubi_homological_complex_equivalence.functor.map f).f n).f = f.f.f n
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.functor.map {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) :
category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj P ⟶ category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj Q

The functor karoubi (homological_complex C c) ⥤ homological_complex (karoubi C) c, on morphisms.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.functor_map {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) :
category_theory.idempotents.karoubi_homological_complex_equivalence.functor.map f = category_theory.idempotents.karoubi_homological_complex_equivalence.functor.map f
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.functor {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} :
category_theory.idempotents.karoubi (homological_complex C c) ⥤ homological_complex (category_theory.idempotents.karoubi C) c

The functor karoubi (homological_complex C c) ⥤ homological_complex (karoubi C) c.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.functor_obj {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) :
category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj P = category_theory.idempotents.karoubi_homological_complex_equivalence.functor.obj P
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj_p_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (K : homological_complex (category_theory.idempotents.karoubi C) c) (n : ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj K).p.f n = (K.X n).p
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj_X_d {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (K : homological_complex (category_theory.idempotents.karoubi C) c) (i j : ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj K).X.d i j = (K.d i j).f
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (K : homological_complex (category_theory.idempotents.karoubi C) c) :
category_theory.idempotents.karoubi (homological_complex C c)

The functor homological_complex (karoubi C) c ⥤ karoubi (homological_complex C c), on objects

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj_X_X {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (K : homological_complex (category_theory.idempotents.karoubi C) c) (n : ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj K).X.X n = (K.X n).X
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.map {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} {K L : homological_complex (category_theory.idempotents.karoubi C) c} (f : K ⟶ L) :
category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj K ⟶ category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj L

The functor homological_complex (karoubi C) c ⥤ karoubi (homological_complex C c), on morphisms

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.map_f_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} {K L : homological_complex (category_theory.idempotents.karoubi C) c} (f : K ⟶ L) (n : ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.map f).f.f n = (f.f n).f
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.inverse_obj {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (K : homological_complex (category_theory.idempotents.karoubi C) c) :
category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj K = category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.obj K
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.inverse_map {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (K L : homological_complex (category_theory.idempotents.karoubi C) c) (f : K ⟶ L) :
category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.map f = category_theory.idempotents.karoubi_homological_complex_equivalence.inverse.map f
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.inverse {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} :
homological_complex (category_theory.idempotents.karoubi C) c ⥤ category_theory.idempotents.karoubi (homological_complex C c)

The functor homological_complex (karoubi C) c ⥤ karoubi (homological_complex C c).

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso_hom {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} :
category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso.hom = category_theory.eq_to_hom category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso._proof_1
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso_inv {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} :
category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso.inv = category_theory.eq_to_hom _
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} :
category_theory.idempotents.karoubi_homological_complex_equivalence.inverse ⋙ category_theory.idempotents.karoubi_homological_complex_equivalence.functor ≅ 𝟭 (homological_complex (category_theory.idempotents.karoubi C) c)

The counit isomorphism of the equivalence karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.unit_iso_inv_app_f_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (n : ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence.unit_iso.inv.app P).f.f n = P.p.f n
source
def category_theory.idempotents.karoubi_homological_complex_equivalence.unit_iso {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} :
𝟭 (category_theory.idempotents.karoubi (homological_complex C c)) ≅ category_theory.idempotents.karoubi_homological_complex_equivalence.functor ⋙ category_theory.idempotents.karoubi_homological_complex_equivalence.inverse

The unit isomorphism of the equivalence karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence.unit_iso_hom_app_f_f {C : Type u_1} [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} {c : complex_shape ι} (P : category_theory.idempotents.karoubi (homological_complex C c)) (n : ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence.unit_iso.hom.app P).f.f n = P.p.f n
source
def category_theory.idempotents.karoubi_homological_complex_equivalence (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} (c : complex_shape ι) :
category_theory.idempotents.karoubi (homological_complex C c) ≌ homological_complex (category_theory.idempotents.karoubi C) c

The equivalence karoubi (homological_complex C c) ≌ homological_complex (karoubi C) c.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence_functor (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} (c : complex_shape ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence C c).functor = category_theory.idempotents.karoubi_homological_complex_equivalence.functor
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence_inverse (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} (c : complex_shape ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence C c).inverse = category_theory.idempotents.karoubi_homological_complex_equivalence.inverse
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence_counit_iso (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} (c : complex_shape ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence C c).counit_iso = category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso
source
@[simp]
theorem category_theory.idempotents.karoubi_homological_complex_equivalence_unit_iso (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} (c : complex_shape ι) :
(category_theory.idempotents.karoubi_homological_complex_equivalence C c).unit_iso = category_theory.idempotents.karoubi_homological_complex_equivalence.unit_iso
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_functor_obj_X_X (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.down α))) (n : α) :
(((category_theory.idempotents.karoubi_chain_complex_equivalence C α).functor.obj P).X n).X = P.X.X n
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_inverse_obj_X_X (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.down α)) (n : α) :
((category_theory.idempotents.karoubi_chain_complex_equivalence C α).inverse.obj K).X.X n = (K.X n).X
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_inverse_obj_p_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.down α)) (n : α) :
((category_theory.idempotents.karoubi_chain_complex_equivalence C α).inverse.obj K).p.f n = (K.X n).p
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_functor_obj_X_p (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.down α))) (n : α) :
(((category_theory.idempotents.karoubi_chain_complex_equivalence C α).functor.obj P).X n).p = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_inverse_map_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K L : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.down α)) (f : K ⟶ L) (n : α) :
((category_theory.idempotents.karoubi_chain_complex_equivalence C α).inverse.map f).f.f n = (f.f n).f
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_functor_obj_d_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.down α))) (i j : α) :
(((category_theory.idempotents.karoubi_chain_complex_equivalence C α).functor.obj P).d i j).f = P.X.d i j ≫ P.p.f j
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_functor_map_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P Q : category_theory.idempotents.karoubi (homological_complex C (complex_shape.down α))) (f : P ⟶ Q) (n : α) :
(((category_theory.idempotents.karoubi_chain_complex_equivalence C α).functor.map f).f n).f = f.f.f n
source
def category_theory.idempotents.karoubi_chain_complex_equivalence (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] :
category_theory.idempotents.karoubi (chain_complex C α) ≌ chain_complex (category_theory.idempotents.karoubi C) α

The equivalence karoubi (chain_complex C α) ≌ chain_complex (karoubi C) α.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_counit_iso_hom (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] :
(category_theory.idempotents.karoubi_chain_complex_equivalence C α).counit_iso.hom = category_theory.eq_to_hom category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso._proof_1
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_unit_iso_hom_app_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.down α))) (n : α) :
((category_theory.idempotents.karoubi_chain_complex_equivalence C α).unit_iso.hom.app P).f.f n = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_inverse_obj_X_d (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.down α)) (i j : α) :
((category_theory.idempotents.karoubi_chain_complex_equivalence C α).inverse.obj K).X.d i j = (K.d i j).f
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_counit_iso_inv (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] :
(category_theory.idempotents.karoubi_chain_complex_equivalence C α).counit_iso.inv = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.idempotents.karoubi_chain_complex_equivalence_unit_iso_inv_app_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.down α))) (n : α) :
((category_theory.idempotents.karoubi_chain_complex_equivalence C α).unit_iso.inv.app P).f.f n = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_counit_iso_hom (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] :
(category_theory.idempotents.karoubi_cochain_complex_equivalence C α).counit_iso.hom = category_theory.eq_to_hom category_theory.idempotents.karoubi_homological_complex_equivalence.counit_iso._proof_1
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_functor_obj_X_p (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.up α))) (n : α) :
(((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).functor.obj P).X n).p = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_inverse_map_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K L : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.up α)) (f : K ⟶ L) (n : α) :
((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).inverse.map f).f.f n = (f.f n).f
source
def category_theory.idempotents.karoubi_cochain_complex_equivalence (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] :
category_theory.idempotents.karoubi (cochain_complex C α) ≌ cochain_complex (category_theory.idempotents.karoubi C) α

The equivalence karoubi (cochain_complex C α) ≌ cochain_complex (karoubi C) α.

Equations
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_inverse_obj_X_X (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.up α)) (n : α) :
((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).inverse.obj K).X.X n = (K.X n).X
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_functor_map_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P Q : category_theory.idempotents.karoubi (homological_complex C (complex_shape.up α))) (f : P ⟶ Q) (n : α) :
(((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).functor.map f).f n).f = f.f.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_inverse_obj_p_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.up α)) (n : α) :
((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).inverse.obj K).p.f n = (K.X n).p
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_inverse_obj_X_d (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (K : homological_complex (category_theory.idempotents.karoubi C) (complex_shape.up α)) (i j : α) :
((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).inverse.obj K).X.d i j = (K.d i j).f
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_functor_obj_d_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.up α))) (i j : α) :
(((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).functor.obj P).d i j).f = P.X.d i j ≫ P.p.f j
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_unit_iso_inv_app_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.up α))) (n : α) :
((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).unit_iso.inv.app P).f.f n = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_unit_iso_hom_app_f_f (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.up α))) (n : α) :
((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).unit_iso.hom.app P).f.f n = P.p.f n
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_functor_obj_X_X (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] (P : category_theory.idempotents.karoubi (homological_complex C (complex_shape.up α))) (n : α) :
(((category_theory.idempotents.karoubi_cochain_complex_equivalence C α).functor.obj P).X n).X = P.X.X n
source
@[simp]
theorem category_theory.idempotents.karoubi_cochain_complex_equivalence_counit_iso_inv (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] (α : Type u_4) [add_right_cancel_semigroup α] [has_one α] :
(category_theory.idempotents.karoubi_cochain_complex_equivalence C α).counit_iso.inv = category_theory.eq_to_hom _
source
@[protected, instance]
def category_theory.idempotents.homological_complex.category_theory.is_idempotent_complete (C : Type u_1) [category_theory.category C] [category_theory.preadditive C] {ι : Type u_3} (c : complex_shape ι) [category_theory.is_idempotent_complete C] :
category_theory.is_idempotent_complete (homological_complex C c)