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.

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

@[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

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

@[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

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)

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)

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

@[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

@[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

@[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)

@[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

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.

@[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

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

• CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f = HomologicalComplex.Hom.mk fun (n : ι) => CategoryTheory.Idempotents.Karoubi.Hom.mk (f.f.f n)

@[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.toPrefunctor.obj P = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.obj P

@[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.toPrefunctor.map f = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Functor.map f

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.

@[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

@[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

@[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

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.

@[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

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

• CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f = CategoryTheory.Idempotents.Karoubi.Hom.mk (HomologicalComplex.Hom.mk fun (n : ι) => (f.f n).f)

@[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.toPrefunctor.obj K = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.obj K

@[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.toPrefunctor.map f = CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.Inverse.map f

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.

@[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))

@[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)

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

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

@[simp]

theorem CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.unitIso_inv_app_f_f {C : Type u_1} [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

@[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

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.

@[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

@[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

@[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

@[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

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.

@[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.toPrefunctor.map f).f n).f = f.f.f n

@[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.toPrefunctor.obj P).d i j).f = CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)

@[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.toPrefunctor.obj K).X.X n = (K.X n).X

@[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.toPrefunctor.obj K).p.f n = (K.X n).p

@[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.toPrefunctor.obj P).X n).X = P.X.X n

@[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)

@[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.toPrefunctor.obj K).X.d i j = (K.d i j).f

@[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.toPrefunctor.map f).f.f n = (f.f n).f

@[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 α)))

@[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

@[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

@[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.toPrefunctor.obj P).X n).p = P.p.f n

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

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

@[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.toPrefunctor.obj P).X n).X = P.X.X n

@[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.toPrefunctor.map f).f.f n = (f.f n).f

@[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.toPrefunctor.obj P).d i j).f = CategoryTheory.CategoryStruct.comp (P.X.d i j) (P.p.f j)

@[simp]

theorem CategoryTheory.Idempotents.karoubiCochainComplexEquivalence_unitIso_inv_app_f_f (C : Type u_1) [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

@[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)

@[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.toPrefunctor.obj K).p.f n = (K.X n).p

@[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

@[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.toPrefunctor.map f).f n).f = f.f.f n

@[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 α)))

@[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.toPrefunctor.obj P).X n).p = P.p.f n

@[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.toPrefunctor.obj K).X.d i j = (K.d i j).f

@[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.toPrefunctor.obj K).X.X n = (K.X n).X

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

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

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

• (_ : CategoryTheory.IsIdempotentComplete (HomologicalComplex C c)) = (_ : CategoryTheory.IsIdempotentComplete (HomologicalComplex C c))