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.

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

Instances For
    @[simp]
    @[simp]
    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
      @[simp]
      @[simp]
      @[simp]
      @[simp]
      @[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_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]
      @[simp]