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

      The left derived functors of an additive functor.

      Equations
      Instances For
        source
        noncomputable def CategoryTheory.ProjectiveResolution.isoLeftDerivedObj {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) :
          CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (Q.isoLeftDerivedObj F n).hom = CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj Q.complex) ⟶ Z) :
          CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).hom h) = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) :
          CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv ((F.leftDerived n).map f) = CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {Z : D} (h : (F.leftDerived n).obj Y ⟶ Z) :
          CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).inv (CategoryTheory.CategoryStruct.comp ((F.leftDerived n).map f) h) = CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ)) (CategoryTheory.CategoryStruct.comp (Q.isoLeftDerivedObj F n).inv h)
          source
          theorem CategoryTheory.Functor.isZero_leftDerived_obj_projective_succ {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Projective X] :
          CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {X : C} {Y : C} (f : X ⟶ Y) {P : CategoryTheory.ProjectiveResolution X} {Q : CategoryTheory.ProjectiveResolution Y} (g : P.complex ⟶ Q.complex) (w : CategoryTheory.CategoryStruct.comp g Q.π = CategoryTheory.CategoryStruct.comp P.π ((ChainComplex.single₀ C).map f)) :
          (F.leftDerived n).map f = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) :
            (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedToHomotopyCategoryObj F).hom (CategoryTheory.CategoryStruct.comp ((HomotopyCategory.quotient D (ComplexShape.down ℕ)).map ((CategoryTheory.NatTrans.mapHomologicalComplex α (ComplexShape.down ℕ)).app P.complex)) (P.isoLeftDerivedToHomotopyCategoryObj G).inv)
            source
            @[simp]
            theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] :
            CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.id F) = CategoryTheory.CategoryStruct.id F.leftDerivedToHomotopyCategory
            source
            @[simp]
            theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] :
            CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β) = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β)
            source
            theorem CategoryTheory.NatTrans.leftDerivedToHomotopyCategory_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H) [F.Additive] [G.Additive] [H.Additive] {Z : CategoryTheory.Functor C (HomotopyCategory D (ComplexShape.down ℕ))} (h : H.leftDerivedToHomotopyCategory ⟶ Z) :
            CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory (CategoryTheory.CategoryStruct.comp α β)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory α) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerivedToHomotopyCategory β) h)
            source
            noncomputable def CategoryTheory.NatTrans.leftDerived {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) :
              CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.id F) n = CategoryTheory.CategoryStruct.id (F.leftDerived n)
              source
              @[simp]
              theorem CategoryTheory.NatTrans.leftDerived_comp {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) :
              CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.NatTrans.leftDerived β n)
              source
              theorem CategoryTheory.NatTrans.leftDerived_comp_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} {H : CategoryTheory.Functor C D} [F.Additive] [G.Additive] [H.Additive] (α : F ⟶ G) (β : G ⟶ H) (n : ℕ) {Z : CategoryTheory.Functor C D} (h : H.leftDerived n ⟶ Z) :
              CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived (CategoryTheory.CategoryStruct.comp α β) n) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived α n) (CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.leftDerived β n) h)
              source
              theorem CategoryTheory.ProjectiveResolution.leftDerived_app_eq {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) {X : C} (P : CategoryTheory.ProjectiveResolution X) (n : ℕ) :
              (CategoryTheory.NatTrans.leftDerived α n).app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F n).hom (CategoryTheory.CategoryStruct.comp ((HomologicalComplex.homologyFunctor D (ComplexShape.down ℕ) n).map ((CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] :
                CategoryTheory.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} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] {Z : D} (h : F.obj X ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex).pOpcycles 0) (CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) h) = CategoryTheory.CategoryStruct.comp (F.map (P.π.f 0)) h
                source
                theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality {D : Type u_1} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] :
                CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (Q.fromLeftDerivedZero' F) = CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (F.map f)
                source
                theorem CategoryTheory.ProjectiveResolution.fromLeftDerivedZero'_naturality_assoc {D : Type u_1} [CategoryTheory.Category.{u_4, u_1} D] [CategoryTheory.Abelian D] {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Abelian C] {X : C} {Y : C} (f : X ⟶ Y) (P : CategoryTheory.ProjectiveResolution X) (Q : CategoryTheory.ProjectiveResolution Y) (φ : P.complex ⟶ Q.complex) (comm : CategoryTheory.CategoryStruct.comp (φ.f 0) (Q.π.f 0) = CategoryTheory.CategoryStruct.comp (P.π.f 0) f) (F : CategoryTheory.Functor C D) [F.Additive] {Z : D} (h : F.obj Y ⟶ Z) :
                CategoryTheory.CategoryStruct.comp (HomologicalComplex.opcyclesMap ((F.mapHomologicalComplex (ComplexShape.down ℕ)).map φ) 0) (CategoryTheory.CategoryStruct.comp (Q.fromLeftDerivedZero' F) h) = CategoryTheory.CategoryStruct.comp (P.fromLeftDerivedZero' F) (CategoryTheory.CategoryStruct.comp (F.map f) h)
                source
                instance CategoryTheory.ProjectiveResolution.instIsIsoFromLeftDerivedZero'Self {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) [CategoryTheory.Projective X] :
                CategoryTheory.IsIso ((CategoryTheory.ProjectiveResolution.self X).fromLeftDerivedZero' F)
                Equations
                • ⋯ = ⋯
                source
                noncomputable def CategoryTheory.Functor.fromLeftDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] {X : C} (P : CategoryTheory.ProjectiveResolution X) (F : CategoryTheory.Functor C D) [F.Additive] :
                  F.fromLeftDerivedZero.app X = CategoryTheory.CategoryStruct.comp (P.isoLeftDerivedObj F 0).hom (CategoryTheory.CategoryStruct.comp (ChainComplex.isoHomologyι₀ ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj P.complex)).hom (P.fromLeftDerivedZero' F))
                  source
                  instance CategoryTheory.instIsIsoAppFromLeftDerivedZeroOfProjective {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (X : C) [CategoryTheory.Projective X] :
                  CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.instIsIsoFromLeftDerivedZero' {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {X : C} (P : CategoryTheory.ProjectiveResolution X) :
                  CategoryTheory.IsIso (P.fromLeftDerivedZero' F)
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.instIsIsoAppFromLeftDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) :
                  CategoryTheory.IsIso (F.fromLeftDerivedZero.app X)
                  Equations
                  • ⋯ = ⋯
                  source
                  instance CategoryTheory.instIsIsoFunctorFromLeftDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :
                  CategoryTheory.IsIso F.fromLeftDerivedZero
                  Equations
                  • ⋯ = ⋯
                  source
                  noncomputable def CategoryTheory.Functor.leftDerivedZeroIsoSelf {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.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} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :
                    F.leftDerivedZeroIsoSelf.hom = F.fromLeftDerivedZero
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :
                    CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero F.leftDerivedZeroIsoSelf.inv = CategoryTheory.CategoryStruct.id (F.leftDerived 0)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F.leftDerived 0 ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero (CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] :
                    CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv F.fromLeftDerivedZero = CategoryTheory.CategoryStruct.id F
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv (CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) :
                    CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (F.leftDerivedZeroIsoSelf.inv.app X) = CategoryTheory.CategoryStruct.id ((F.leftDerived 0).obj X)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : (F.leftDerived 0).obj X ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) (CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) h) = h
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) :
                    CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (F.fromLeftDerivedZero.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
                    source
                    @[simp]
                    theorem CategoryTheory.Functor.leftDerivedZeroIsoSelf_inv_hom_id_app_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian C] [CategoryTheory.HasProjectiveResolutions C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteColimits F] (X : C) {Z : D} (h : F.obj X ⟶ Z) :
                    CategoryTheory.CategoryStruct.comp (F.leftDerivedZeroIsoSelf.inv.app X) (CategoryTheory.CategoryStruct.comp (F.fromLeftDerivedZero.app X) h) = h