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
    def CategoryTheory.InjectiveResolution.descFSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z) (n : ) (g : J.cocomplex.X n I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) I.cocomplex.X (n + 1)) (w : CategoryTheory.CategoryStruct.comp (J.cocomplex.d n (n + 1)) g' = CategoryTheory.CategoryStruct.comp g (I.cocomplex.d n (n + 1))) :
    (g'' : J.cocomplex.X (n + 2) I.cocomplex.X (n + 2)) ×' CategoryTheory.CategoryStruct.comp (J.cocomplex.d (n + 1) (n + 2)) g'' = CategoryTheory.CategoryStruct.comp g' (I.cocomplex.d (n + 1) (n + 2))

    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

        An auxiliary definition for descHomotopyZero.

        Equations
        Instances For

          An auxiliary definition for descHomotopyZero.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def CategoryTheory.InjectiveResolution.descHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex J.cocomplex) (n : ) (g : I.cocomplex.X (n + 1) J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))) :
            I.cocomplex.X (n + 3) J.cocomplex.X (n + 2)

            An auxiliary definition for descHomotopyZero.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z✝} (f : I.cocomplex J.cocomplex) (n : ) (g : I.cocomplex.X (n + 1) J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))) {Z : C} (h : J.cocomplex.X (n + 2) Z) :
              @[simp]
              theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {Y : C} {Z : C} {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex J.cocomplex) (n : ) (g : I.cocomplex.X (n + 1) J.cocomplex.X n) (g' : I.cocomplex.X (n + 2) J.cocomplex.X (n + 1)) (w : f.f (n + 1) = CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryTheory.CategoryStruct.comp g (J.cocomplex.d n (n + 1))) :
              CategoryTheory.CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3)) (CategoryTheory.InjectiveResolution.descHomotopyZeroSucc f n g g' w) = f.f (n + 2) - CategoryTheory.CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))

              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

                Two descents of the same morphism are homotopic.

                Equations
                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
                                Instances For