Documentation

Mathlib.CategoryTheory.Abelian.InjectiveResolution

Abelian categories with enough injectives have injective resolutions #

Main results #

When the underlying category is abelian:

Auxiliary construction for desc.

Equations
Instances For

    A morphism in C descends to a chain map between injective resolutions.

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

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

      An auxiliary definition for descHomotopyZero.

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

        Any descent of the zero morphism is homotopic to zero.

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

          The descent of the identity morphism is homotopic to the identity cochain map.

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

            The descent of a composition is homotopic to the composition of the descents.

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

              Any two injective resolutions are homotopy equivalent.

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

                An arbitrarily chosen injective resolution of an object.

                Equations
                Instances For

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

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

                    If I : InjectiveResolution X, then the chosen (injectiveResolutions C).obj X is isomorphic (in the homotopy category) to I.cocomplex.

                    Equations
                    Instances For

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

                      Auxiliary definition for InjectiveResolution.of.

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

                        In any abelian category with enough injectives, InjectiveResolution.of Z constructs an injective resolution of the object Z.

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