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

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, on morphisms.

    Equations
    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), on morphisms

          Equations
          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

              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

                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