Left-derived functors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the left-derived functors F.left_derived n : C ⥤ D for any additive functor F
out of a category with projective resolutions.
The definition is
projective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n
that is, we pick a projective resolution (thought of as an object of the homotopy category),
we apply F objectwise, and compute n-th homology.
We show that these left-derived functors can be calculated on objects using any choice of projective resolution, and on morphisms by any choice of lift to a chain map between chosen projective resolutions.
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.
Implementation #
We don't assume the categories involved are abelian (just preadditive, and have equalizers, cokernels, and image maps), or that the functors are right exact. None of these assumptions are needed yet.
It is often convenient, of course, to work with [abelian C] [enough_projectives C] [abelian D]
which (assuming the results from category_theory.abelian.projective) are enough to
provide all the typeclass hypotheses assumed here.
noncomputable
def
category_theory.functor.left_derived
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
(F : C ⥤ D)
[F.additive]
(n : ℕ) :
C ⥤ D
The left derived functors of an additive functor.
noncomputable
def
category_theory.functor.left_derived_obj_iso
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X : C}
(P : category_theory.ProjectiveResolution X) :
(F.left_derived n).obj X ≅ (homology_functor D (complex_shape.down ℕ) n).obj ((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex)
We can compute a left derived functor using a chosen projective resolution.
Equations
- F.left_derived_obj_iso n P = (homotopy_category.homology_functor D (complex_shape.down ℕ) n).map_iso (homotopy_category.iso_of_homotopy_equiv (F.map_homotopy_equiv (category_theory.functor.left_derived_obj_iso._proof_1.some.homotopy_equiv P))) ≪≫ (homotopy_category.homology_factors D (complex_shape.down ℕ) n).app ((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex)
@[simp]
theorem
category_theory.functor.left_derived_obj_iso_hom
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X : C}
(P : category_theory.ProjectiveResolution X) :
(F.left_derived_obj_iso n P).hom = (homotopy_category.homology_functor D (complex_shape.down ℕ) n).map ((homotopy_category.quotient D (complex_shape.down ℕ)).map ((F.map_homological_complex (complex_shape.down ℕ)).map (category_theory.functor.left_derived_obj_iso._proof_1.some.homotopy_equiv P).hom))
@[simp]
theorem
category_theory.functor.left_derived_obj_iso_inv
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X : C}
(P : category_theory.ProjectiveResolution X) :
(F.left_derived_obj_iso n P).inv = (homotopy_category.homology_functor D (complex_shape.down ℕ) n).map ((homotopy_category.quotient D (complex_shape.down ℕ)).map ((F.map_homological_complex (complex_shape.down ℕ)).map (category_theory.functor.left_derived_obj_iso._proof_1.some.homotopy_equiv P).inv))
@[simp]
theorem
category_theory.functor.left_derived_obj_projective_zero_inv
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
[category_theory.limits.has_zero_object D]
(F : C ⥤ D)
[F.additive]
(X : C)
[category_theory.projective X] :
(F.left_derived_obj_projective_zero X).inv = (chain_complex.homology_functor_0_single₀ D).inv.app (F.obj X) ≫ homology.map _ _ (homological_complex.hom.sq_to ((chain_complex.single₀_map_homological_complex F).inv.app X) 0) (homological_complex.hom.sq_from ((chain_complex.single₀_map_homological_complex F).inv.app X) 0) _ ≫ (homotopy_category.homology_functor D (complex_shape.down ℕ) 0).map ((homotopy_category.quotient D (complex_shape.down ℕ)).map ((F.map_homological_complex (complex_shape.down ℕ)).map (category_theory.functor.left_derived_obj_iso._proof_1.some.homotopy_equiv (category_theory.ProjectiveResolution.self X)).inv))
noncomputable
def
category_theory.functor.left_derived_obj_projective_zero
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
[category_theory.limits.has_zero_object D]
(F : C ⥤ D)
[F.additive]
(X : C)
[category_theory.projective X] :
(F.left_derived 0).obj X ≅ F.obj X
The 0-th derived functor of F on a projective object X is just F.obj X.
Equations
@[simp]
theorem
category_theory.functor.left_derived_obj_projective_zero_hom
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
[category_theory.limits.has_zero_object D]
(F : C ⥤ D)
[F.additive]
(X : C)
[category_theory.projective X] :
(F.left_derived_obj_projective_zero X).hom = (homotopy_category.homology_functor D (complex_shape.down ℕ) 0).map ((homotopy_category.quotient D (complex_shape.down ℕ)).map ((F.map_homological_complex (complex_shape.down ℕ)).map (category_theory.functor.left_derived_obj_iso._proof_1.some.homotopy_equiv (category_theory.ProjectiveResolution.self X)).hom)) ≫ homology.map _ _ (homological_complex.hom.sq_to ((chain_complex.single₀_map_homological_complex F).hom.app X) 0) (homological_complex.hom.sq_from ((chain_complex.single₀_map_homological_complex F).hom.app X) 0) _ ≫ (chain_complex.homology_functor_0_single₀ D).hom.app (F.obj X)
noncomputable
def
category_theory.functor.left_derived_obj_projective_succ
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
[category_theory.limits.has_zero_object D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
(X : C)
[category_theory.projective X] :
(F.left_derived (n + 1)).obj X ≅ 0
The higher derived functors vanish on projective objects.
Equations
- F.left_derived_obj_projective_succ n X = F.left_derived_obj_iso (n + 1) (category_theory.ProjectiveResolution.self X) ≪≫ (homology_functor D (complex_shape.down ℕ) (n + 1)).map_iso ((chain_complex.single₀_map_homological_complex F).app X) ≪≫ (chain_complex.homology_functor_succ_single₀ D n).app (F.obj X) ≪≫ _.iso_zero
@[simp]
theorem
category_theory.functor.left_derived_obj_projective_succ_inv
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
[category_theory.limits.has_zero_object D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
(X : C)
[category_theory.projective X] :
(F.left_derived_obj_projective_succ n X).inv = _.iso_zero.inv ≫ (chain_complex.homology_functor_succ_single₀ D n).inv.app (F.obj X) ≫ homology.map _ _ (homological_complex.hom.sq_to ((chain_complex.single₀_map_homological_complex F).inv.app X) (n + 1)) (homological_complex.hom.sq_from ((chain_complex.single₀_map_homological_complex F).inv.app X) (n + 1)) _ ≫ (homotopy_category.homology_functor D (complex_shape.down ℕ) (n + 1)).map ((homotopy_category.quotient D (complex_shape.down ℕ)).map ((F.map_homological_complex (complex_shape.down ℕ)).map (category_theory.functor.left_derived_obj_iso._proof_1.some.homotopy_equiv (category_theory.ProjectiveResolution.self X)).inv))
theorem
category_theory.functor.left_derived_map_eq
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X Y : C}
(f : X ⟶ Y)
{P : category_theory.ProjectiveResolution X}
{Q : category_theory.ProjectiveResolution Y}
(g : P.complex ⟶ Q.complex)
(w : g ≫ Q.π = P.π ≫ (chain_complex.single₀ C).map f) :
(F.left_derived n).map f = (F.left_derived_obj_iso n P).hom ≫ (homology_functor D (complex_shape.down ℕ) n).map ((F.map_homological_complex (complex_shape.down ℕ)).map g) ≫ (F.left_derived_obj_iso n Q).inv
We can compute a left derived functor on a morphism using a lift of that morphism to a chain map between chosen projective resolutions.
@[simp]
theorem
category_theory.nat_trans.left_derived_app
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
{F G : C ⥤ D}
[F.additive]
[G.additive]
(α : F ⟶ G)
(n : ℕ)
(X : C) :
(category_theory.nat_trans.left_derived α n).app X = (homotopy_category.homology_functor D (complex_shape.down ℕ) n).map ((homotopy_category.quotient D (complex_shape.down ℕ)).map ((category_theory.nat_trans.map_homological_complex α (complex_shape.down ℕ)).app ((category_theory.projective_resolutions C).obj X).as))
noncomputable
def
category_theory.nat_trans.left_derived
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
{F G : C ⥤ D}
[F.additive]
[G.additive]
(α : F ⟶ G)
(n : ℕ) :
F.left_derived n ⟶ G.left_derived n
The natural transformation between left-derived functors induced by a natural transformation.
@[simp]
theorem
category_theory.nat_trans.left_derived_id
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
(F : C ⥤ D)
[F.additive]
(n : ℕ) :
category_theory.nat_trans.left_derived (𝟙 F) n = 𝟙 (F.left_derived n)
@[simp, nolint]
theorem
category_theory.nat_trans.left_derived_comp
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
{F G H : C ⥤ D}
[F.additive]
[G.additive]
[H.additive]
(α : F ⟶ G)
(β : G ⟶ H)
(n : ℕ) :
theorem
category_theory.nat_trans.left_derived_eq
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.preadditive C]
[category_theory.limits.has_zero_object C]
[category_theory.limits.has_equalizers C]
[category_theory.limits.has_images C]
[category_theory.has_projective_resolutions C]
[category_theory.preadditive D]
[category_theory.limits.has_equalizers D]
[category_theory.limits.has_cokernels D]
[category_theory.limits.has_images D]
[category_theory.limits.has_image_maps D]
{F G : C ⥤ D}
[F.additive]
[G.additive]
(α : F ⟶ G)
(n : ℕ)
{X : C}
(P : category_theory.ProjectiveResolution X) :
(category_theory.nat_trans.left_derived α n).app X = (F.left_derived_obj_iso n P).hom ≫ (homology_functor D (complex_shape.down ℕ) n).map ((category_theory.nat_trans.map_homological_complex α (complex_shape.down ℕ)).app P.complex) ≫ (G.left_derived_obj_iso n P).inv
A component of the natural transformation between left-derived functors can be computed using a chosen projective resolution.