Documentation

Mathlib.CategoryTheory.Abelian.ProjectiveResolution

Abelian categories with enough projectives have projective resolutions #

Main results #

When the underlying category is abelian:

Auxiliary construction for lift.

Equations
Instances For

    A morphism in C lift to a chain map between projective resolutions.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      @[simp]

      The resolution maps intertwine the lift of a morphism and that morphism.

      An auxiliary definition for liftHomotopyZero.

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

        Any lift of the zero morphism is homotopic to zero.

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

          The lift of the identity morphism is homotopic to the identity chain map.

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

            The lift of a composition is homotopic to the composition of the lifts.

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

              Any two projective resolutions are homotopy equivalent.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[reducible, inline]

                An arbitrarily chosen projective resolution of an object.

                Equations
                Instances For

                  Taking projective resolutions is functorial, if considered with target the homotopy category (-indexed chain complexes and chain maps up to homotopy).

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

                    If P : ProjectiveResolution X, then the chosen (projectiveResolutions C).obj X is isomorphic (in the homotopy category) to P.complex.

                    Equations
                    Instances For

                      Our goal is to define ProjectiveResolution.of Z : ProjectiveResolution Z. The 0-th object in this resolution will just be Projective.over Z, i.e. an arbitrarily chosen projective object with a map to Z. After that, we build the n+1-st object as Projective.syzygies applied to the previously constructed morphism, and the map from the n-th object as Projective.d.

                      Auxiliary definition for ProjectiveResolution.of.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[irreducible]

                        In any abelian category with enough projectives, ProjectiveResolution.of Z constructs an projective resolution of the object Z.

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