Documentation

Mathlib.CategoryTheory.Abelian.Injective.Resolution

Abelian categories with enough injectives have injective resolutions #

Main results #

When the underlying category is abelian:

theorem CategoryTheory.InjectiveResolution.exact₀ {C : Type u} [Category.{v, u} C] [Abelian C] {Z : C} (I : InjectiveResolution Z) :
{ X₁ := ((CochainComplex.single₀ C).obj Z).X 0, X₂ := I.cocomplex.X 0, X₃ := I.cocomplex.X 1, f := I.ι.f 0, g := I.cocomplex.d 0 1, zero := }.Exact
def CategoryTheory.InjectiveResolution.descFSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} (I : InjectiveResolution Y) (J : InjectiveResolution Z) (n : ) (g : J.cocomplex.X n I.cocomplex.X n) (g' : J.cocomplex.X (n + 1) I.cocomplex.X (n + 1)) (w : CategoryStruct.comp (J.cocomplex.d n (n + 1)) g' = CategoryStruct.comp g (I.cocomplex.d n (n + 1))) :
(g'' : J.cocomplex.X (n + 2) I.cocomplex.X (n + 2)) ×' CategoryStruct.comp (J.cocomplex.d (n + 1) (n + 2)) g'' = 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
      @[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
        def CategoryTheory.InjectiveResolution.descHomotopyZeroSucc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : 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) = CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + 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 {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : 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) = CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryStruct.comp g (J.cocomplex.d n (n + 1))) :
          CategoryStruct.comp (I.cocomplex.d (n + 2) (n + 3)) (descHomotopyZeroSucc f n g g' w) = f.f (n + 2) - CategoryStruct.comp g' (J.cocomplex.d (n + 1) (n + 2))
          @[simp]
          theorem CategoryTheory.InjectiveResolution.comp_descHomotopyZeroSucc_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {Y Z : C} {I : InjectiveResolution Y} {J : 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) = CategoryStruct.comp (I.cocomplex.d (n + 1) (n + 2)) g' + CategoryStruct.comp g (J.cocomplex.d n (n + 1))) {Z✝ : C} (h : J.cocomplex.X (n + 2) Z✝) :

          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
                        theorem CategoryTheory.exact_f_d {C : Type u} [Category.{v, u} C] [Abelian C] [EnoughInjectives C] {X Y : C} (f : X Y) :
                        { X₁ := X, X₂ := Y, X₃ := Injective.syzygies f, f := f, g := Injective.d f, zero := }.Exact

                        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
                            theorem CategoryTheory.InjectiveResolution.of_def {C : Type u_1} [Category.{u_2, u_1} C] [Abelian C] [EnoughInjectives C] (Z : C) :
                            of Z = { cocomplex := ofCocomplex Z, injective := , hasHomology := , ι := ((ofCocomplex Z).fromSingle₀Equiv Z).symm Injective.ι Z, , quasiIso := }