Left derived functors on a projective presentation of length one

Let S : 0 ⟶ P₁ ⟶ P₀ ⟶ M ⟶ 0 be a short exact sequence in an abelian category with P₁ and P₀ projective. Then ⋯ ⟶ 0 ⟶ P₁ ⟶ P₀ is a projective resolution of M (CategoryTheory.ShortComplex.ShortExact.projectiveResolution), and for every additive functor F it computes the left derived functors of F at M:

• L₁F(M) is the kernel of F(P₁) ⟶ F(P₀) (CategoryTheory.ShortComplex.ShortExact.leftDerivedOneIsoKernel);
• LₙF(M) vanishes for n ≥ 2 (CategoryTheory.ShortComplex.ShortExact.isZero_leftDerived_add_two).

The complex, its augmentation, and the chain maps induced by morphisms of short complexes are constructed in TauCeti.Algebra.Homology.ShortComplex.Resolution for any category with zero morphisms and a zero object.

The identification of L₁F(M) is natural in the functor F and in maps of such presentations. For an arbitrary additive F the projectivity of P₁ is needed even in degree 1: the long exact sequence only gives L₁F(M) ≅ ker(L₀F(P₁) ⟶ F(P₀)), and L₀F(P₁) = F(P₁) for projective P₁. Over a principal ideal domain every module has such a presentation, by a free module and its kernel, which is again free; applied to the tensor product, this computes Tor₁ in the Künneth and universal coefficient theorems.

The file also records two general facts. The natural transformation LₙF ⟶ LₙG induced by α : F ⟶ G is additive in α (CategoryTheory.NatTrans.leftDerived_add), so that a derived functor depending on a parameter through a natural transformation, such as Tor in its underived variable, is an additive functor of that parameter. An exact additive functor has no positive left derived functors (CategoryTheory.Functor.isZero_leftDerived_succ).

References

• C. A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Section 2.4, for left derived functors computed from a projective resolution.

theorem CategoryTheory.ShortComplex.quasiIso_resolutionπ {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) : _root_.QuasiIso S.resolutionπ

For a short exact S, the augmentation of S.resolutionComplex is a quasi-isomorphism.

noncomputable def CategoryTheory.ShortComplex.ShortExact.projectiveResolution {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] : ProjectiveResolution S.X₃

A short exact sequence 0 ⟶ P₁ ⟶ P₀ ⟶ M ⟶ 0 with P₁ and P₀ projective gives the projective resolution ⋯ ⟶ 0 ⟶ P₁ ⟶ P₀ of M, with P₀ in degree 0.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.projectiveResolution_complex {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] : hS.projectiveResolution.complex = S.resolutionComplex

The complex of the resolution is S.resolutionComplex.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.projectiveResolution_π {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] : hS.projectiveResolution.π = S.resolutionπ

The augmentation of the resolution is S.resolutionπ.

theorem CategoryTheory.ShortComplex.ShortExact.isZero_leftDerived_add_two {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] (n : ℕ) : Limits.IsZero ((F.leftDerived (n + 2)).obj S.X₃)

The left derived functors of F vanish in degrees at least 2 on an object with a projective presentation of length one.

noncomputable def CategoryTheory.ShortComplex.ShortExact.leftDerivedOneIsoKernel {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] : (F.leftDerived 1).obj S.X₃ ≅ Limits.kernel (F.map S.f)

On an object with a projective presentation 0 ⟶ P₁ ⟶ P₀ ⟶ M ⟶ 0, the first left derived functor of F is the kernel of F(P₁) ⟶ F(P₀). It sends the homology class of a cycle of F applied to the resolution to that cycle (homologyπ_comp_isoLeftDerivedObj_inv_comp_leftDerivedOneIsoKernel_hom_comp_ι).

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.homologyπ_comp_isoLeftDerivedObj_inv_comp_leftDerivedOneIsoKernel_hom_comp_ι {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] : CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).homologyπ 1) (CategoryStruct.comp (hS.projectiveResolution.isoLeftDerivedObj F 1).inv (CategoryStruct.comp (hS.leftDerivedOneIsoKernel F).hom (Limits.kernel.ι (F.map S.f)))) = ((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).iCycles 1

The identification of L₁F(M) with the kernel of F(P₁) ⟶ F(P₀) sends the homology class of a cycle of F applied to the resolution to that cycle.

@[simp]

theorem CategoryTheory.ShortComplex.ShortExact.homologyπ_comp_isoLeftDerivedObj_inv_comp_leftDerivedOneIsoKernel_hom_comp_ι_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] {Z : D} (h : F.obj S.X₁ ⟶ Z) : CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).homologyπ 1) (CategoryStruct.comp (CategoryStruct.comp (hS.projectiveResolution.isoLeftDerivedObj F 1).inv (CategoryStruct.comp (hS.leftDerivedOneIsoKernel F).hom (Limits.kernel.ι (F.map S.f)))) h) = CategoryStruct.comp (((F.mapHomologicalComplex (ComplexShape.down ℕ)).obj S.resolutionComplex).iCycles 1) h

The identification of L₁F(M) with the kernel of F(P₁) ⟶ F(P₀) sends the homology class of a cycle of F applied to the resolution to that cycle.

theorem CategoryTheory.ShortComplex.ShortExact.leftDerived_app_comp_leftDerivedOneIsoKernel_hom {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] {G : Functor C D} (hS : S.ShortExact) [G.Additive] (α : F ⟶ G) : CategoryStruct.comp ((NatTrans.leftDerived α 1).app S.X₃) (hS.leftDerivedOneIsoKernel G).hom = CategoryStruct.comp (hS.leftDerivedOneIsoKernel F).hom (Limits.kernel.map (F.map S.f) (G.map S.f) (α.app S.X₁) (α.app S.X₂) ⋯)

The identification of L₁F(M) with the kernel of F(P₁) ⟶ F(P₀) is natural in F.

theorem CategoryTheory.ShortComplex.ShortExact.leftDerived_app_comp_leftDerivedOneIsoKernel_hom_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {S : ShortComplex C} [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] {G : Functor C D} (hS : S.ShortExact) [G.Additive] (α : F ⟶ G) {Z : D} (h : Limits.kernel (G.map S.f) ⟶ Z) : CategoryStruct.comp ((NatTrans.leftDerived α 1).app S.X₃) (CategoryStruct.comp (hS.leftDerivedOneIsoKernel G).hom h) = CategoryStruct.comp (hS.leftDerivedOneIsoKernel F).hom (CategoryStruct.comp (Limits.kernel.map (F.map S.f) (G.map S.f) (α.app S.X₁) (α.app S.X₂) ⋯) h)

The identification of L₁F(M) with the kernel of F(P₁) ⟶ F(P₀) is natural in F.

theorem CategoryTheory.ShortComplex.ShortExact.leftDerived_map_comp_leftDerivedOneIsoKernel_hom {C : Type u} [Category.{v, u} C] [Abelian C] {S S' : ShortComplex C} {hS : S.ShortExact} [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] (hS' : S'.ShortExact) [Projective S'.X₁] [Projective S'.X₂] (φ : S ⟶ S') : CategoryStruct.comp ((F.leftDerived 1).map φ.τ₃) (hS'.leftDerivedOneIsoKernel F).hom = CategoryStruct.comp (hS.leftDerivedOneIsoKernel F).hom (Limits.kernel.map (F.map S.f) (F.map S'.f) (F.map φ.τ₁) (F.map φ.τ₂) ⋯)

The identification of L₁F(M) with the kernel of F(P₁) ⟶ F(P₀) is natural in maps of projective presentations.

theorem CategoryTheory.ShortComplex.ShortExact.leftDerived_map_comp_leftDerivedOneIsoKernel_hom_assoc {C : Type u} [Category.{v, u} C] [Abelian C] {S S' : ShortComplex C} {hS : S.ShortExact} [Projective S.X₁] [Projective S.X₂] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] [HasProjectiveResolutions C] (F : Functor C D) [F.Additive] (hS' : S'.ShortExact) [Projective S'.X₁] [Projective S'.X₂] (φ : S ⟶ S') {Z : D} (h : Limits.kernel (F.map S'.f) ⟶ Z) : CategoryStruct.comp ((F.leftDerived 1).map φ.τ₃) (CategoryStruct.comp (hS'.leftDerivedOneIsoKernel F).hom h) = CategoryStruct.comp (hS.leftDerivedOneIsoKernel F).hom (CategoryStruct.comp (Limits.kernel.map (F.map S.f) (F.map S'.f) (F.map φ.τ₁) (F.map φ.τ₂) ⋯) h)

The identification of L₁F(M) with the kernel of F(P₁) ⟶ F(P₀) is natural in maps of projective presentations.

@[simp]

theorem CategoryTheory.NatTrans.leftDerived_add {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] {F G : Functor C D} [F.Additive] [G.Additive] (α β : F ⟶ G) (n : ℕ) : leftDerived (α + β) n = leftDerived α n + leftDerived β n

The natural transformation between left derived functors induced by a natural transformation is additive in it.

theorem CategoryTheory.Functor.isZero_leftDerived_succ {C : Type u} [Category.{v, u} C] [Abelian C] [HasProjectiveResolutions C] {D : Type u_1} [Category.{v_1, u_1} D] [Abelian D] (F : Functor C D) [F.Additive] [F.PreservesHomology] (X : C) (q : ℕ) : Limits.IsZero ((F.leftDerived (q + 1)).obj X)

An exact additive functor has no positive left derived functors.