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 : HomologicalComplex.X Q.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f.f n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.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 (HomologicalComplex.Hom.f P.p n) (HomologicalComplex.Hom.f f.f n) = HomologicalComplex.Hom.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 : HomologicalComplex.X Q.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f.f n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f Q.p n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.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 (HomologicalComplex.Hom.f f.f n) (HomologicalComplex.Hom.f Q.p n) = HomologicalComplex.Hom.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 : HomologicalComplex.X Q.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f.f n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f.f n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f Q.p 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 (HomologicalComplex.Hom.f P.p n) (HomologicalComplex.Hom.f f.f n) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f f.f n) (HomologicalComplex.Hom.f Q.p 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 : HomologicalComplex.X P.X n ⟶ Z) :
CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p n) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p n) h) = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p 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 (HomologicalComplex.Hom.f P.p n) (HomologicalComplex.Hom.f P.p n) = HomologicalComplex.Hom.f P.p 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 : ι) :
(HomologicalComplex.X (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P) n).p = HomologicalComplex.Hom.f P.p 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 : ι) :
(HomologicalComplex.d (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P) i j).f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.Hom.f P.p i) (HomologicalComplex.d P.X 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 : ι) :
(HomologicalComplex.X (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P) n).X = HomologicalComplex.X P.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.

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 : ι) :
    (HomologicalComplex.Hom.f (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f) n).f = HomologicalComplex.Hom.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.

    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.

      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 : ι) :
        HomologicalComplex.d (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X i j = (HomologicalComplex.d K 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 : ι) :
        HomologicalComplex.X (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).X n = (HomologicalComplex.X K 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 : ι) :
        HomologicalComplex.Hom.f (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K).p n = (HomologicalComplex.X K 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

        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 : ι) :
          HomologicalComplex.Hom.f (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f).f n = (HomologicalComplex.Hom.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

          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).

            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 (_ : CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor = CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c))
              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 (_ : CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) c) = CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor)
              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.

              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 : ι) :
                HomologicalComplex.Hom.f (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.inv.app P).f n = HomologicalComplex.Hom.f P.p 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 : ι) :
                HomologicalComplex.Hom.f (CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso.hom.app P).f n = HomologicalComplex.Hom.f P.p 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.

                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.

                  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 : α), (HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.map f) n).f = HomologicalComplex.Hom.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 : α) :
                    (HomologicalComplex.d ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P) i j).f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.X i j) (HomologicalComplex.Hom.f P.p 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 : α) :
                    HomologicalComplex.X ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X n = (HomologicalComplex.X K 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 : α) :
                    HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).p n = (HomologicalComplex.X K 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 : α) :
                    (HomologicalComplex.X ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P) n).X = HomologicalComplex.X P.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 (_ : CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)) = CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor)
                    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 : α) :
                    HomologicalComplex.d ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.obj K).X i j = (HomologicalComplex.d K 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 : α), HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).inverse.map f).f n = (HomologicalComplex.Hom.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 (_ : CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor = CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.down α)))
                    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 : α) :
                    HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.hom.app P).f n = HomologicalComplex.Hom.f P.p 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 : α) :
                    HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.inv.app P).f n = HomologicalComplex.Hom.f P.p 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 : α) :
                    (HomologicalComplex.X ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).functor.obj P) n).p = HomologicalComplex.Hom.f P.p 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) α.

                    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 : α) :
                      (HomologicalComplex.X ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P) n).X = HomologicalComplex.X P.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 : α), HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.map f).f n = (HomologicalComplex.Hom.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 : α) :
                      (HomologicalComplex.d ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P) i j).f = CategoryTheory.CategoryStruct.comp (HomologicalComplex.d P.X i j) (HomologicalComplex.Hom.f P.p 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 : α) :
                      HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.inv.app P).f n = HomologicalComplex.Hom.f P.p 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 (_ : CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)) = CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor)
                      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 : α) :
                      HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).p n = (HomologicalComplex.X K 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 : α) :
                      HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).unitIso.hom.app P).f n = HomologicalComplex.Hom.f P.p 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 : α), (HomologicalComplex.Hom.f ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.map f) n).f = HomologicalComplex.Hom.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 (_ : CategoryTheory.Functor.comp CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.inverse CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.functor = CategoryTheory.Functor.id (HomologicalComplex (CategoryTheory.Idempotents.Karoubi C) (ComplexShape.up α)))
                      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 : α) :
                      (HomologicalComplex.X ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).functor.obj P) n).p = HomologicalComplex.Hom.f P.p 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 : α) :
                      HomologicalComplex.d ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X i j = (HomologicalComplex.d K 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 : α) :
                      HomologicalComplex.X ((CategoryTheory.Idempotents.karoubiCochainComplexEquivalence C α).inverse.obj K).X n = (HomologicalComplex.X K 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) α.

                      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)