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.

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

    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

      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

        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
          @[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
          @[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
          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.Idempotents.KaroubiHomologicalComplexEquivalence.inverse.comp 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
            @[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
            @[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
            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.Idempotents.KaroubiHomologicalComplexEquivalence.functor.comp 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
              @[simp]
              @[simp]
              @[simp]
              @[simp]

              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