Idempotent completeness and homological complexes

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

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

@[simp]

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

theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P Q : Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C} (h : Q.X.X n ⟶ Z) : CategoryStruct.comp (P.p.f n) (CategoryStruct.comp (f.f.f n) h) = CategoryStruct.comp (f.f.f n) h

@[simp]

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

theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P Q : Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C} (h : Q.X.X n ⟶ Z) : CategoryStruct.comp (f.f.f n) (CategoryStruct.comp (Q.p.f n) h) = CategoryStruct.comp (f.f.f n) h

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

theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P Q : Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C} (h : Q.X.X n ⟶ Z) : CategoryStruct.comp (P.p.f n) (CategoryStruct.comp (f.f.f n) h) = CategoryStruct.comp (f.f.f n) (CategoryStruct.comp (Q.p.f n) h)

@[simp]

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

theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) (n : ι) {Z : C} (h : P.X.X n ⟶ Z) : CategoryStruct.comp (P.p.f n) (CategoryStruct.comp (P.p.f n) h) = CategoryStruct.comp (P.p.f n) h

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) : HomologicalComplex (Karoubi C) c

The functor Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c, on objects.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) (i j : ι) : ((obj P).d i j).f = CategoryStruct.comp (P.p.f i) (P.X.d i j)

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_X {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) (n : ι) : ((obj P).X n).X = P.X.X n

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) (n : ι) : ((obj P).X n).p = P.p.f n

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P Q : Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) : obj P ⟶ obj Q

The functor Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c, on morphisms.

Equations

• CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f = { f := fun (n : ι) => { f := f.f.f n, comm := ⋯ }, comm' := ⋯ }

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P Q : Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) : ((map f).f n).f = f.f.f n

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} : Functor (Karoubi (HomologicalComplex C c)) (HomologicalComplex (Karoubi C) c)

The functor Karoubi (HomologicalComplex C c) ⥤ HomologicalComplex (Karoubi C) c.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_obj {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) : functor.obj P = Functor.obj P

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_map {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {X✝ Y✝ : Karoubi (HomologicalComplex C c)} (f : X✝ ⟶ Y✝) : functor.map f = Functor.map f

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (Karoubi C) c) : Karoubi (HomologicalComplex C c)

The functor HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c), on objects

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (Karoubi C) c) (i j : ι) : (obj K).X.d i j = (K.d i j).f

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (Karoubi C) c) (n : ι) : (obj K).p.f n = (K.X n).p

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (Karoubi C) c) (n : ι) : (obj K).X.X n = (K.X n).X

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex (Karoubi C) c} (f : K ⟶ L) : obj K ⟶ obj L

The functor HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c), on morphisms

Equations

• CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f = { f := { f := fun (n : ι) => (f.f n).f, comm' := ⋯ }, comm := ⋯ }

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex (Karoubi C) c} (f : K ⟶ L) (n : ι) : (map f).f.f n = (f.f n).f

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} : Functor (HomologicalComplex (Karoubi C) c) (Karoubi (HomologicalComplex C c))

The functor HomologicalComplex (Karoubi C) c ⥤ Karoubi (HomologicalComplex C c).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_map {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {X✝ Y✝ : HomologicalComplex (Karoubi C) c} (f : X✝ ⟶ Y✝) : inverse.map f = Inverse.map f

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_obj {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (Karoubi C) c) : inverse.obj K = Inverse.obj K

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} : inverse.comp functor ≅ Functor.id (HomologicalComplex (Karoubi C) c)

The counit isomorphism of the equivalence Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c.

Equations

• CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso = CategoryTheory.eqToIso ⋯

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} : counitIso.hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} : counitIso.inv = eqToHom ⋯

def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} : Functor.id (Karoubi (HomologicalComplex C c)) ≅ functor.comp inverse

The unit isomorphism of the equivalence Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) (n : ι) : (unitIso.inv.app P).f.f n = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_hom_app_f_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : Karoubi (HomologicalComplex C c)) (n : ι) : (unitIso.hom.app P).f.f n = P.p.f n

def CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence (C : Type u_1) [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} (c : ComplexShape ι) : Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c

The equivalence Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (Karoubi C) c.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso (C : Type u_1) [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} (c : ComplexShape ι) : (karoubiHomologicalComplexEquivalence C c).counitIso = KaroubiHomologicalComplexEquivalence.counitIso

@[simp]

theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor (C : Type u_1) [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} (c : ComplexShape ι) : (karoubiHomologicalComplexEquivalence C c).functor = KaroubiHomologicalComplexEquivalence.functor

@[simp]

theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse (C : Type u_1) [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} (c : ComplexShape ι) : (karoubiHomologicalComplexEquivalence C c).inverse = KaroubiHomologicalComplexEquivalence.inverse

@[simp]

theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso (C : Type u_1) [Category.{u_3, u_1} C] [Preadditive C] {ι : Type u_2} (c : ComplexShape ι) : (karoubiHomologicalComplexEquivalence C c).unitIso = KaroubiHomologicalComplexEquivalence.unitIso

def CategoryTheory.Idempotents.karoubiChainComplexEquivalence (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] : Karoubi (ChainComplex C α) ≌ ChainComplex (Karoubi C) α

The equivalence Karoubi (ChainComplex C α) ≌ ChainComplex (Karoubi C) α.

Equations

• CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α = CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C (ComplexShape.down α)

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.down α))) (i j : α) : (((karoubiChainComplexEquivalence C α).functor.obj P).d i j).f = CategoryStruct.comp (P.X.d i j) (P.p.f j)

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) : ((karoubiChainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (Karoubi C) (ComplexShape.down α)) (n : α) : ((karoubiChainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) : (((karoubiChainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) : (((karoubiChainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] : (karoubiChainComplexEquivalence C α).counitIso.inv = eqToHom ⋯

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] {X✝ Y✝ : Karoubi (HomologicalComplex C (ComplexShape.down α))} (f : X✝ ⟶ Y✝) (n : α) : (((karoubiChainComplexEquivalence C α).functor.map f).f n).f = f.f.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] {X✝ Y✝ : HomologicalComplex (Karoubi C) (ComplexShape.down α)} (f : X✝ ⟶ Y✝) (n : α) : ((karoubiChainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] : (karoubiChainComplexEquivalence C α).counitIso.hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) : ((karoubiChainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (Karoubi C) (ComplexShape.down α)) (n : α) : ((karoubiChainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X

@[simp]

theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (Karoubi C) (ComplexShape.down α)) (i j : α) : ((karoubiChainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f

def CategoryTheory.Idempotents.karoubiCochainComplexEquivalence (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] : Karoubi (CochainComplex C α) ≌ CochainComplex (Karoubi C) α

The equivalence Karoubi (CochainComplex C α) ≌ CochainComplex (Karoubi C) α.

Equations

• CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α = CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C (ComplexShape.up α)

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) : (((karoubiCochainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) : ((karoubiCochainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (Karoubi C) (ComplexShape.up α)) (i j : α) : ((karoubiCochainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] : (karoubiCochainComplexEquivalence C α).counitIso.hom = eqToHom ⋯

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] {X✝ Y✝ : Karoubi (HomologicalComplex C (ComplexShape.up α))} (f : X✝ ⟶ Y✝) (n : α) : (((karoubiCochainComplexEquivalence C α).functor.map f).f n).f = f.f.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.up α))) (i j : α) : (((karoubiCochainComplexEquivalence C α).functor.obj P).d i j).f = CategoryStruct.comp (P.X.d i j) (P.p.f j)

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) : ((karoubiCochainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_inv (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] : (karoubiCochainComplexEquivalence C α).counitIso.inv = eqToHom ⋯

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) : (((karoubiCochainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_map_f_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] {X✝ Y✝ : HomologicalComplex (Karoubi C) (ComplexShape.up α)} (f : X✝ ⟶ Y✝) (n : α) : ((karoubiCochainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (Karoubi C) (ComplexShape.up α)) (n : α) : ((karoubiCochainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (Karoubi C) (ComplexShape.up α)) (n : α) : ((karoubiCochainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p

instance CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplex (C : Type u_1) [Category.{u_4, u_1} C] [Preadditive C] {ι : Type u_2} (c : ComplexShape ι) [IsIdempotentComplete C] : IsIdempotentComplete (HomologicalComplex C c)