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
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C} (h : Q.X.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (P.p.f n) (CategoryTheory.CategoryStruct.comp (f.f.f n) h) = CategoryTheory.CategoryStruct.comp (f.f.f n) h
source
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comp_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) :
CategoryTheory.CategoryStruct.comp (P.p.f n) (f.f.f n) = f.f.f n
source
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C} (h : Q.X.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (f.f.f n) (CategoryTheory.CategoryStruct.comp (Q.p.f n) h) = CategoryTheory.CategoryStruct.comp (f.f.f n) h
source
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.comp_p_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) :
CategoryTheory.CategoryStruct.comp (f.f.f n) (Q.p.f n) = f.f.f n
source
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) {Z : C} (h : Q.X.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (P.p.f n) (CategoryTheory.CategoryStruct.comp (f.f.f n) h) = CategoryTheory.CategoryStruct.comp (f.f.f n) (CategoryTheory.CategoryStruct.comp (Q.p.f n) h)
source
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_comm_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) :
CategoryTheory.CategoryStruct.comp (P.p.f n) (f.f.f n) = CategoryTheory.CategoryStruct.comp (f.f.f n) (Q.p.f n)
source
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem_assoc {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) {Z : C} (h : P.X.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (P.p.f n) (CategoryTheory.CategoryStruct.comp (P.p.f n) h) = CategoryTheory.CategoryStruct.comp (P.p.f n) h
source
@[simp]
theorem CategoryTheory.Idempotents.Karoubi.HomologicalComplex.p_idem {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) :
CategoryTheory.CategoryStruct.comp (P.p.f n) (P.p.f n) = P.p.f n
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_X_p {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) :
((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).X n).p = P.p.f n
source
@[simp]
theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj_d_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (i : ι) (j : ι) :
((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).d i j).f = CategoryTheory.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) :
((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P).X n).X = P.X.X n
source
def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) :
HomologicalComplex (CategoryTheory.Idempotents.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.
Instances For
    source
    @[simp]
    theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map_f_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) (n : ι) :
    ((CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f).f n).f = f.f.f n
    source
    def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} {Q : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : P ⟶ Q) :
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P ⟶ CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj Q

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

    Equations
    Instances For
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) :
      CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.obj P = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P
      source
      @[simp]
      theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
      ∀ {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)} (f : X ⟶ Y), CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor.map f = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f
      source
      def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
      CategoryTheory.Functor (CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (HomologicalComplex (CategoryTheory.Idempotents.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.
      Instances For
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_d {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (i : ι) (j : ι) :
        (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X.d i j = (K.d i j).f
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_X_X {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (n : ι) :
        (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X.X n = (K.X n).X
        source
        @[simp]
        theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj_p_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (n : ι) :
        (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).p.f n = (K.X n).p
        source
        def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) :
        CategoryTheory.Idempotents.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.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map_f_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} {L : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} (f : K ⟶ L) (n : ι) :
          (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f).f.f n = (f.f n).f
          source
          def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} {K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} {L : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} (f : K ⟶ L) :
          CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K ⟶ CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj L

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

          Equations
          Instances For
            source
            @[simp]
            theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_obj {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) :
            CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.obj K = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K
            source
            @[simp]
            theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse_map {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
            ∀ {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c} (f : X ⟶ Y), CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.map f = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f
            source
            def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
            CategoryTheory.Functor (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) (CategoryTheory.Idempotents.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.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_hom {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
              CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso.hom = CategoryTheory.eqToHom ⋯
              source
              @[simp]
              theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso_inv {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
              CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso.inv = CategoryTheory.eqToHom ⋯
              source
              def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
              CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor ≅ CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.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.unitIso_inv_app_f_f {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) :
                (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) (n : ι) :
                (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.hom.app P).f.f n = P.p.f n
                source
                def CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} {c : ComplexShape ι} :
                CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c)) ≅ CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.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.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_inverse (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} (c : ComplexShape ι) :
                  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).inverse = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse
                  source
                  @[simp]
                  theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_functor (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} (c : ComplexShape ι) :
                  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).functor = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor
                  source
                  @[simp]
                  theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} (c : ComplexShape ι) :
                  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).counitIso = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso
                  source
                  @[simp]
                  theorem CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_unitIso (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} (c : ComplexShape ι) :
                  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).unitIso = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso
                  source
                  def CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence (C : Type u_1) [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} (c : ComplexShape ι) :
                  CategoryTheory.Idempotents.Karoubi (HomologicalComplex C c) ≌ HomologicalComplex (CategoryTheory.Idempotents.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.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_map_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                    ∀ {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))} (f : X ⟶ Y) (n : α), (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.map f).f n).f = f.f.f n
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_d_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (i : α) (j : α) :
                    (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).d i j).f = CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_X (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) (n : α) :
                    ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_p_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) (n : α) :
                    ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_X (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) :
                    (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).X n).X = P.X.X n
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_inv (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                    (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).counitIso.inv = CategoryTheory.eqToHom ⋯
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_obj_X_d (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) (i : α) (j : α) :
                    ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_inverse_map_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                    ∀ {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)} (f : X ⟶ Y) (n : α), ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_counitIso_hom (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                    (CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).counitIso.hom = CategoryTheory.eqToHom ⋯
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) :
                    ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_inv_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) :
                    ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.inv.app P).f.f n = P.p.f n
                    source
                    @[simp]
                    theorem CategoryTheory.Idempotents.karoubiChainComplexEquivalence_functor_obj_X_p (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α) :
                    (((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n
                    source
                    def CategoryTheory.Idempotents.karoubiChainComplexEquivalence (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                    CategoryTheory.Idempotents.Karoubi (ChainComplex C α) ≌ ChainComplex (CategoryTheory.Idempotents.Karoubi C) α

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

                    Equations
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_X (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) :
                      (((CategoryTheory.Idempotents.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) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                      ∀ {X Y : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)} (f : X ⟶ Y) (n : α), ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.map f).f.f n = (f.f n).f
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_d_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (i : α) (j : α) :
                      (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).d i j).f = CategoryTheory.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) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) :
                      ((CategoryTheory.Idempotents.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) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                      (CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).counitIso.inv = CategoryTheory.eqToHom ⋯
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_p_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) (n : α) :
                      ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).p.f n = (K.X n).p
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_hom_app_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) :
                      ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_map_f_f (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                      ∀ {X Y : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))} (f : X ⟶ Y) (n : α), (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.map f).f n).f = f.f.f n
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_counitIso_hom (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                      (CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).counitIso.hom = CategoryTheory.eqToHom ⋯
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_functor_obj_X_p (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.up α))) (n : α) :
                      (((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P).X n).p = P.p.f n
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_d (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) (i : α) (j : α) :
                      ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X.d i j = (K.d i j).f
                      source
                      @[simp]
                      theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_inverse_obj_X_X (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] (K : HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) (n : α) :
                      ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X.X n = (K.X n).X
                      source
                      def CategoryTheory.Idempotents.karoubiCochainComplexEquivalence (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] (α : Type u_3) [AddRightCancelSemigroup α] [One α] :
                      CategoryTheory.Idempotents.Karoubi (CochainComplex C α) ≌ CochainComplex (CategoryTheory.Idempotents.Karoubi C) α

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

                      Equations
                      Instances For
                        source
                        instance CategoryTheory.Idempotents.instIsIdempotentCompleteHomologicalComplexPreadditiveHasZeroMorphismsInstCategoryHomologicalComplex (C : Type u_1) [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Preadditive C] {ι : Type u_2} (c : ComplexShape ι) [CategoryTheory.IsIdempotentComplete C] :
                        CategoryTheory.IsIdempotentComplete (HomologicalComplex C c)
                        Equations
                        • ⋯ = ⋯