Documentation

Mathlib.CategoryTheory.Abelian.LeftDerived

Left-derived functors #

We define the left-derived functors F.leftDerived n : C ⥤ D for any additive functor F out of a category with projective resolutions.

We first define a functor F.leftDerivedToHomotopyCategory : C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which is projectiveResolutions C ⋙ F.mapHomotopyCategory _. We show that if X : C and P : ProjectiveResolution X, then F.leftDerivedToHomotopyCategory.obj X identifies to the image in the homotopy category of the functor F applied objectwise to P.complex (this isomorphism is P.isoLeftDerivedToHomotopyCategoryObj F).

Then, the left-derived functors F.leftDerived n : C ⥤ D are obtained by composing F.leftDerivedToHomotopyCategory with the homology functors on the homotopy category.

Similarly we define natural transformations between left-derived functors coming from natural transformations between the original additive functors, and show how to compute the components.

Main results #

TODO #

source
noncomputable def CategoryTheory.Functor.leftDerivedToHomotopyCategory {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] :
Functor C (HomotopyCategory D (ComplexShape.down ℕ))

When F : C ⥤ D is an additive functor, this is the functor C ⥤ HomotopyCategory D (ComplexShape.down ℕ) which sends X : C to F applied to a projective resolution of X.

Equations
Instances For
    source
    noncomputable def CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X : C} (P : ProjectiveResolution X) (F : Functor C D) [F.Additive] :
    F.leftDerivedToHomotopyCategory.obj X ≅ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).obj P.complex

    If P : ProjectiveResolution Z and F : C ⥤ D is an additive functor, this is an isomorphism between F.leftDerivedToHomotopyCategory.obj X and the complex obtained by applying F to P.complex.

    Equations
    Instances For
      source
      theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] :
      CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (F.leftDerivedToHomotopyCategory.map f) = CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map φ) (Q.isoLeftDerivedToHomotopyCategoryObj F).inv
      source
      theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : F.leftDerivedToHomotopyCategory.obj Y ⟶ Z) :
      CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).inv (CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) h) = CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).inv h)
      source
      theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] :
      CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (Q.isoLeftDerivedToHomotopyCategoryObj F).hom = CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomotopyCategory.quotient D (ComplexShape.down ℕ))).map φ)
      source
      theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedToHomotopyCategoryObj_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] {Z : HomotopyCategory D (ComplexShape.down ℕ)} (h : (HomotopyCategory.quotient D (ComplexShape.down ℕ)).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) :
      CategoryStruct.comp (F.leftDerivedToHomotopyCategory.map f) (CategoryStruct.comp (Q.isoLeftDerivedToHomotopyCategoryObj F).hom h) = CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) h)
      source
      noncomputable def CategoryTheory.Functor.leftDerived {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) :
      Functor C D

      The left derived functors of an additive functor.

      Equations
      Instances For
        source
        noncomputable def CategoryTheory.ProjectiveResolution.isoLeftDerivedObj {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X : C} (P : ProjectiveResolution X) (F : Functor C D) [F.Additive] (n : ℕ) :
        (F.leftDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)

        We can compute a left derived functor using a chosen projective resolution.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] (n : ℕ) :
          CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map φ)
          source
          theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_hom_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) :
          CategoryStruct.comp ((F.leftDerived n).map f) (CategoryStruct.comp (Q.isoLeftDerivedObj F n).hom h) = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) h)
          source
          theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] (n : ℕ) :
          CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) = CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map φ) (Q.isoLeftDerivedObj F n).inv
          source
          theorem CategoryTheory.ProjectiveResolution.isoLeftDerivedObj_inv_naturality_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (F.leftDerived n).obj Y ⟶ Z) :
          CategoryStruct.comp (P.isoLeftDerivedObj F n).inv (CategoryStruct.comp ((F.leftDerived n).map f) h) = CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryStruct.comp (Q.isoLeftDerivedObj F n).inv h)
          source
          theorem CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) (X : C) [Projective X] :
          Limits.IsZero ((F.leftDerived (n + 1)).obj X)

          The higher derived functors vanish on projective objects.

          source
          theorem CategoryTheory.Functor.leftDerived_map_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) {X Y : C} (f : X ⟶ Y) {P : ProjectiveResolution X} {Q : ProjectiveResolution Y} (g : P.complex ⟶ Q.complex) (w : CategoryStruct.comp g Q.π = CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) :
          (F.leftDerived n).map f = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).comp (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n)).map g) (Q.isoLeftDerivedObj F n).inv)

          We can compute a left derived functor on a morphism using a descent of that morphism to a chain map between chosen projective resolutions.

          source
          noncomputable def CategoryTheory.NatTrans.leftDerivedToHomotopyCategory {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) :
          F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory

          The natural transformation F.leftDerivedToHomotopyCategory ⟶ G.leftDerivedToHomotopyCategory induced by a natural transformation F ⟶ G between additive functors.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem CategoryTheory.ProjectiveResolution.leftDerivedToHomotopyCategory_app_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : ProjectiveResolution X) :
            (NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedToHomotopyCategoryObj G).inv)
            source
            @[simp]
            theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] :
            leftDerivedToHomotopyCategory (CategoryStruct.id F) = CategoryStruct.id F.leftDerivedToHomotopyCategory
            source
            @[simp]
            theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] :
            leftDerivedToHomotopyCategory (CategoryStruct.comp α β) = CategoryStruct.comp (leftDerivedToHomotopyCategory α) (leftDerivedToHomotopyCategory β)
            source
            theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G H : Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] {Z : Functor C (HomotopyCategory D (ComplexShape.down ℕ))} (h : H.leftDerivedToHomotopyCategory ⟶ Z) :
            CategoryStruct.comp (leftDerivedToHomotopyCategory (CategoryStruct.comp α β)) h = CategoryStruct.comp (leftDerivedToHomotopyCategory α) (CategoryStruct.comp (leftDerivedToHomotopyCategory β) h)
            source
            noncomputable def CategoryTheory.NatTrans.leftDerived {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) :
            F.leftDerived n ⟶ G.leftDerived n

            The natural transformation between left-derived functors induced by a natural transformation.

            Equations
            Instances For
              source
              @[simp]
              theorem CategoryTheory.NatTrans.leftDerived_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (n : ℕ) :
              leftDerived (CategoryStruct.id F) n = CategoryStruct.id (F.leftDerived n)
              source
              @[simp]
              theorem CategoryTheory.NatTrans.leftDerived_comp {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G H : Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) :
              leftDerived (CategoryStruct.comp α β) n = CategoryStruct.comp (leftDerived α n) (leftDerived β n)
              source
              theorem CategoryTheory.NatTrans.leftDerived_comp_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G H : Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : Functor C D} (h : H.leftDerived n ⟶ Z) :
              CategoryStruct.comp (leftDerived (CategoryStruct.comp α β) n) h = CategoryStruct.comp (leftDerived α n) (CategoryStruct.comp (leftDerived β n) h)
              source
              theorem CategoryTheory.ProjectiveResolution.leftDerived_app_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : ProjectiveResolution X) (n : ℕ) :
              (NatTrans.leftDerived α n).app X = CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedObj G n).inv)

              A component of the natural transformation between left-derived functors can be computed using a chosen projective resolution.

              source
              noncomputable def CategoryTheory.ProjectiveResolution.fromLeftDerivedZero' {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [Abelian D] {X : C} (P : ProjectiveResolution X) (F : Functor C D) [F.Additive] :
              ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).opcycles 0 ⟶ F.obj X

              If P : ProjectiveResolution X and F is an additive functor, this is the canonical morphism from the opcycles in degree 0 of (F.mapHomologicalComplex _).obj P.complex to F.obj X.

              Equations
              Instances For
                source
                @[simp]
                theorem CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero' {D : Type u_1} [Category.{u_4, u_1} D] [Abelian D] {C : Type u_2} [Category.{u_3, u_2} C] [Abelian C] {X : C} (P : ProjectiveResolution X) (F : Functor C D) [F.Additive] :
                CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0) (P.fromLeftDerivedZero' F) = F.map (P.π.f 0)
                source
                @[simp]
                theorem CategoryTheory.ProjectiveResolution.pOpcycles_comp_fromLeftDerivedZero'_assoc {D : Type u_1} [Category.{u_4, u_1} D] [Abelian D] {C : Type u_2} [Category.{u_3, u_2} C] [Abelian C] {X : C} (P : ProjectiveResolution X) (F : Functor C D) [F.Additive] {Z : D} (h : F.obj X ⟶ Z) :
                CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0) (CategoryStruct.comp (P.fromLeftDerivedZero' F) h) = CategoryStruct.comp (F.map (P.π.f 0)) h
                source
                theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality {D : Type u_1} [Category.{u_4, u_1} D] [Abelian D] {C : Type u_2} [Category.{u_3, u_2} C] [Abelian C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] :
                CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (Q.fromLeftDerivedZero' F) = CategoryStruct.comp (P.fromLeftDerivedZero' F) (F.map f)
                source
                theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc {D : Type u_1} [Category.{u_4, u_1} D] [Abelian D] {C : Type u_2} [Category.{u_3, u_2} C] [Abelian C] {X Y : C} (f : X ⟶ Y) (P : ProjectiveResolution X) (Q : ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryStruct.comp (P.π.f 0) f) (F : Functor C D) [F.Additive] {Z : D} (h : F.obj Y ⟶ Z) :
                CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (CategoryStruct.comp (Q.fromLeftDerivedZero' F) h) = CategoryStruct.comp (P.fromLeftDerivedZero' F) (CategoryStruct.comp (F.map f) h)
                source
                instance CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] (X : C) [Projective X] :
                IsIso ((self X).fromLeftDerivedZero' F)
                source
                noncomputable def CategoryTheory.Functor.fromLeftDerivedZero {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] :
                F.leftDerived 0 ⟶ F

                The natural transformation F.leftDerived 0 ⟶ F.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero_eq {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] {X : C} (P : ProjectiveResolution X) (F : Functor C D) [F.Additive] :
                  F.fromLeftDerivedZero.app X = CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom (CategoryStruct.comp (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom (P.fromLeftDerivedZero' F))
                  source
                  instance CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] (X : C) [Projective X] :
                  IsIso (F.fromLeftDerivedZero.app X)
                  source
                  instance CategoryTheory.instIsIsoFromLeftDerivedZero' {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] {X : C} (P : ProjectiveResolution X) :
                  IsIso (P.fromLeftDerivedZero' F)
                  source
                  instance CategoryTheory.instIsIsoAppFromLeftDerivedZero {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] (X : C) :
                  IsIso (F.fromLeftDerivedZero.app X)
                  source
                  instance CategoryTheory.instIsIsoFunctorFromLeftDerivedZero {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] :
                  IsIso F.fromLeftDerivedZero
                  source
                  noncomputable def CategoryTheory.Functor.leftDerivedZeroIsoSelf {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] :
                  F.leftDerived 0 ≅ F

                  The canonical isomorphism F.leftDerived 0 ≅ F when F is right exact (i.e. preserves finite colimits).

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] :
                    F.leftDerivedZeroIsoSelf.hom = F.fromLeftDerivedZero
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] :
                    CategoryStruct.comp F.fromLeftDerivedZero F.leftDerivedZeroIsoSelf.inv = CategoryStruct.id (F.leftDerived 0)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] {Z : Functor C D} (h : F.leftDerived 0 ⟶ Z) :
                    CategoryStruct.comp F.fromLeftDerivedZero (CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] :
                    CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv F.fromLeftDerivedZero = CategoryStruct.id F
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] {Z : Functor C D} (h : F ⟶ Z) :
                    CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv (CategoryStruct.comp F.fromLeftDerivedZero h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] (X : C) :
                    CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) = CategoryStruct.id ((F.leftDerived 0).obj X)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : (F.leftDerived 0).obj X ⟶ Z) :
                    CategoryStruct.comp (F.fromLeftDerivedZero.app X) (CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] (X : C) :
                    CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) = CategoryStruct.id (F.obj X)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app_assoc {C : Type u} [Category.{v, u} C] {D : Type u_1} [Category.{u_2, u_1} D] [Abelian C] [HasProjectiveResolutions C] [Abelian D] (F : Functor C D) [F.Additive] [Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z) :
                    CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (CategoryStruct.comp (F.fromLeftDerivedZero.app X) h) = h