Documentation

Mathlib.CategoryTheory.Idempotents.HomologicalComplex

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.

source
@[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
source
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
source
@[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
source
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
source
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)
source
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)
source
@[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
source
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
source
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
    Instances For
      source
      @[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)
      source
      @[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
      source
      @[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
      source
      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
        Instances For
          source
          @[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
          source
          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
            Instances For
              source
              @[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
              source
              @[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
              source
              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
                Instances For
                  source
                  @[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
                  source
                  @[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
                  source
                  @[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
                  source
                  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
                    Instances For
                      source
                      @[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
                      source
                      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
                        Instances For
                          source
                          @[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
                          source
                          @[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
                          source
                          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
                            Instances For
                              source
                              @[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 ⋯
                              source
                              @[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 ⋯
                              source
                              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
                                Instances For
                                  source
                                  @[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
                                  source
                                  @[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
                                  source
                                  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
                                    Instances For
                                      source
                                      @[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
                                      source
                                      @[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
                                      source
                                      @[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
                                      source
                                      @[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
                                      source
                                      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
                                        Instances For
                                          source
                                          @[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)
                                          source
                                          @[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
                                          source
                                          @[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
                                          source
                                          @[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
                                          source
                                          @[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
                                          source
                                          @[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 ⋯
                                          source
                                          @[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
                                          source
                                          @[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
                                          source
                                          @[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 ⋯
                                          source
                                          @[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
                                          source
                                          @[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
                                          source
                                          @[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
                                          source
                                          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
                                            Instances For
                                              source
                                              @[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
                                              source
                                              @[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
                                              source
                                              @[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
                                              source
                                              @[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 ⋯
                                              source
                                              @[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
                                              source
                                              @[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)
                                              source
                                              @[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
                                              source
                                              @[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 ⋯
                                              source
                                              @[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
                                              source
                                              @[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
                                              source
                                              @[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
                                              source
                                              @[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
                                              source
                                              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)