Right-derived functors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We define the right-derived functors F.right_derived n : C ⥤ D for any additive functor F
out of a category with injective resolutions.
The definition is
injective_resolutions C ⋙ F.map_homotopy_category _ ⋙ homotopy_category.homology_functor D _ n
that is, we pick an injective resolution (thought of as an object of the homotopy category),
we apply F objectwise, and compute n-th homology.
We show that these right-derived functors can be calculated on objects using any choice of injective resolution, and on morphisms by any choice of lift to a cochain map between chosen injective resolutions.
Similarly we define natural transformations between right-derived functors coming from natural transformations between the original additive functors, and show how to compute the components.
Main results #
category_theory.functor.right_derived_obj_injective_zero: the0-th derived functor ofFon an injective objectXis isomorphic toF.obj X.category_theory.functor.right_derived_obj_injective_succ: injective objects have no higher right derived functor.category_theory.nat_trans.right_derived: the natural isomorphism between right derived functors induced by natural transformation.
Now, we assume preserves_finite_limits F, then
category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono: iffis mono andexact f g, thenexact (F.map f) (F.map g).category_theory.abelian.functor.right_derived_zero_iso_self: if there are enough injectives, then there is a natural isomorphism(F.right_derived 0) ≅ F.
noncomputable
def
category_theory.functor.right_derived
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ) :
C ⥤ D
The right derived functors of an additive functor.
@[simp]
theorem
category_theory.functor.right_derived_obj_iso_hom
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X : C}
(P : category_theory.InjectiveResolution X) :
(F.right_derived_obj_iso n P).hom = (homotopy_category.homology_functor D (complex_shape.up ℕ) n).map ((homotopy_category.quotient D (complex_shape.up ℕ)).map ((F.map_homological_complex (complex_shape.up ℕ)).map (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv P).hom))
@[simp]
theorem
category_theory.functor.right_derived_obj_iso_inv
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X : C}
(P : category_theory.InjectiveResolution X) :
(F.right_derived_obj_iso n P).inv = (homotopy_category.homology_functor D (complex_shape.up ℕ) n).map ((homotopy_category.quotient D (complex_shape.up ℕ)).map ((F.map_homological_complex (complex_shape.up ℕ)).map (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv P).inv))
noncomputable
def
category_theory.functor.right_derived_obj_iso
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X : C}
(P : category_theory.InjectiveResolution X) :
(F.right_derived n).obj X ≅ (homology_functor D (complex_shape.up ℕ) n).obj ((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex)
We can compute a right derived functor using a chosen injective resolution.
Equations
- F.right_derived_obj_iso n P = (homotopy_category.homology_functor D (complex_shape.up ℕ) n).map_iso (homotopy_category.iso_of_homotopy_equiv (F.map_homotopy_equiv (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv P))) ≪≫ (homotopy_category.homology_factors D (complex_shape.up ℕ) n).app ((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex)
@[simp]
theorem
category_theory.functor.right_derived_obj_injective_zero_hom
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(X : C)
[category_theory.injective X] :
(F.right_derived_obj_injective_zero X).hom = (homotopy_category.homology_functor D (complex_shape.up ℕ) 0).map ((homotopy_category.quotient D (complex_shape.up ℕ)).map ((F.map_homological_complex (complex_shape.up ℕ)).map (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv (category_theory.InjectiveResolution.self X)).hom)) ≫ homology.map _ _ (homological_complex.hom.sq_to ((cochain_complex.single₀_map_homological_complex F).hom.app X) 0) (homological_complex.hom.sq_from ((cochain_complex.single₀_map_homological_complex F).hom.app X) 0) _ ≫ (cochain_complex.homology_functor_0_single₀ D).hom.app (F.obj X)
@[simp]
theorem
category_theory.functor.right_derived_obj_injective_zero_inv
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(X : C)
[category_theory.injective X] :
(F.right_derived_obj_injective_zero X).inv = (cochain_complex.homology_functor_0_single₀ D).inv.app (F.obj X) ≫ homology.map _ _ (homological_complex.hom.sq_to ((cochain_complex.single₀_map_homological_complex F).inv.app X) 0) (homological_complex.hom.sq_from ((cochain_complex.single₀_map_homological_complex F).inv.app X) 0) _ ≫ (homotopy_category.homology_functor D (complex_shape.up ℕ) 0).map ((homotopy_category.quotient D (complex_shape.up ℕ)).map ((F.map_homological_complex (complex_shape.up ℕ)).map (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv (category_theory.InjectiveResolution.self X)).inv))
noncomputable
def
category_theory.functor.right_derived_obj_injective_zero
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(X : C)
[category_theory.injective X] :
(F.right_derived 0).obj X ≅ F.obj X
The 0-th derived functor of F on an injective object X is just F.obj X.
Equations
noncomputable
def
category_theory.functor.right_derived_obj_injective_succ
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
(X : C)
[category_theory.injective X] :
(F.right_derived (n + 1)).obj X ≅ 0
The higher derived functors vanish on injective objects.
Equations
- F.right_derived_obj_injective_succ n X = F.right_derived_obj_iso (n + 1) (category_theory.InjectiveResolution.self X) ≪≫ (homology_functor D (complex_shape.up ℕ) (n + 1)).map_iso ((cochain_complex.single₀_map_homological_complex F).app X) ≪≫ (cochain_complex.homology_functor_succ_single₀ D n).app (F.obj X) ≪≫ _.iso_zero
@[simp]
theorem
category_theory.functor.right_derived_obj_injective_succ_inv
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
(X : C)
[category_theory.injective X] :
(F.right_derived_obj_injective_succ n X).inv = _.iso_zero.inv ≫ (cochain_complex.homology_functor_succ_single₀ D n).inv.app (F.obj X) ≫ homology.map _ _ (homological_complex.hom.sq_to ((cochain_complex.single₀_map_homological_complex F).inv.app X) (n + 1)) (homological_complex.hom.sq_from ((cochain_complex.single₀_map_homological_complex F).inv.app X) (n + 1)) _ ≫ (homotopy_category.homology_functor D (complex_shape.up ℕ) (n + 1)).map ((homotopy_category.quotient D (complex_shape.up ℕ)).map ((F.map_homological_complex (complex_shape.up ℕ)).map (category_theory.functor.right_derived_obj_iso._proof_14.some.homotopy_equiv (category_theory.InjectiveResolution.self X)).inv))
theorem
category_theory.functor.right_derived_map_eq
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ)
{X Y : C}
(f : Y ⟶ X)
{P : category_theory.InjectiveResolution X}
{Q : category_theory.InjectiveResolution Y}
(g : Q.cocomplex ⟶ P.cocomplex)
(w : Q.ι ≫ g = (cochain_complex.single₀ C).map f ≫ P.ι) :
(F.right_derived n).map f = (F.right_derived_obj_iso n Q).hom ≫ (homology_functor D (complex_shape.up ℕ) n).map ((F.map_homological_complex (complex_shape.up ℕ)).map g) ≫ (F.right_derived_obj_iso n P).inv
We can compute a right derived functor on a morphism using a descent of that morphism to a cochain map between chosen injective resolutions.
noncomputable
def
category_theory.nat_trans.right_derived
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
{F G : C ⥤ D}
[F.additive]
[G.additive]
(α : F ⟶ G)
(n : ℕ) :
F.right_derived n ⟶ G.right_derived n
The natural transformation between right-derived functors induced by a natural transformation.
@[simp]
theorem
category_theory.nat_trans.right_derived_app
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
{F G : C ⥤ D}
[F.additive]
[G.additive]
(α : F ⟶ G)
(n : ℕ)
(X : C) :
(category_theory.nat_trans.right_derived α n).app X = (homotopy_category.homology_functor D (complex_shape.up ℕ) n).map ((homotopy_category.quotient D (complex_shape.up ℕ)).map ((category_theory.nat_trans.map_homological_complex α (complex_shape.up ℕ)).app ((category_theory.injective_resolutions C).obj X).as))
@[simp]
theorem
category_theory.nat_trans.right_derived_id
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
(F : C ⥤ D)
[F.additive]
(n : ℕ) :
category_theory.nat_trans.right_derived (𝟙 F) n = 𝟙 (F.right_derived n)
@[simp, nolint]
theorem
category_theory.nat_trans.right_derived_comp
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
{F G H : C ⥤ D}
[F.additive]
[G.additive]
[H.additive]
(α : F ⟶ G)
(β : G ⟶ H)
(n : ℕ) :
theorem
category_theory.nat_trans.right_derived_eq
{C : Type u}
[category_theory.category C]
{D : Type u_1}
[category_theory.category D]
[category_theory.abelian C]
[category_theory.has_injective_resolutions C]
[category_theory.abelian D]
{F G : C ⥤ D}
[F.additive]
[G.additive]
(α : F ⟶ G)
(n : ℕ)
{X : C}
(P : category_theory.InjectiveResolution X) :
(category_theory.nat_trans.right_derived α n).app X = (F.right_derived_obj_iso n P).hom ≫ (homology_functor D (complex_shape.up ℕ) n).map ((category_theory.nat_trans.map_homological_complex α (complex_shape.up ℕ)).app P.cocomplex) ≫ (G.right_derived_obj_iso n P).inv
A component of the natural transformation between right-derived functors can be computed using a chosen injective resolution.
theorem
category_theory.abelian.functor.preserves_exact_of_preserves_finite_limits_of_mono
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
{X Y Z : C}
{f : X ⟶ Y}
{g : Y ⟶ Z}
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.limits.preserves_finite_limits F]
[category_theory.mono f]
(ex : category_theory.exact f g) :
category_theory.exact (F.map f) (F.map g)
If preserves_finite_limits F and mono f, then exact (F.map f) (F.map g) if
exact f g.
theorem
category_theory.abelian.functor.exact_of_map_injective_resolution
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
{X : C}
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
(P : category_theory.InjectiveResolution X)
[category_theory.limits.preserves_finite_limits F] :
category_theory.exact (F.map (P.ι.f 0)) (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_from 0)
noncomputable
def
category_theory.abelian.functor.right_derived_zero_to_self_app
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
[category_theory.limits.preserves_finite_limits F]
{X : C}
(P : category_theory.InjectiveResolution X) :
(F.right_derived 0).obj X ⟶ F.obj X
Given P : InjectiveResolution X, a morphism (F.right_derived 0).obj X ⟶ F.obj X given
preserves_finite_limits F.
Equations
- category_theory.abelian.functor.right_derived_zero_to_self_app F P = (F.right_derived_obj_iso 0 P).hom ≫ (homology_iso_kernel_desc (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_to 0) (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_from 0) _).hom ≫ category_theory.limits.kernel.map (category_theory.limits.cokernel.desc (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_to 0) (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_from 0) _) (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_from 0) (category_theory.limits.cokernel.desc (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_to 0) (𝟙 (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).X 0)) _) (𝟙 (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).X_next 0)) _ ≫ (category_theory.as_iso (category_theory.limits.kernel.lift (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_from 0) (F.map (P.ι.f 0)) _)).inv
noncomputable
def
category_theory.abelian.functor.right_derived_zero_to_self_app_inv
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
{X : C}
(P : category_theory.InjectiveResolution X) :
F.obj X ⟶ (F.right_derived 0).obj X
Given P : InjectiveResolution X, a morphism F.obj X ⟶ (F.right_derived 0).obj X.
Equations
- category_theory.abelian.functor.right_derived_zero_to_self_app_inv F P = homology.lift (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_to 0) (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_from 0) _ (F.map (P.ι.f 0) ≫ category_theory.limits.cokernel.π (((F.map_homological_complex (complex_shape.up ℕ)).obj P.cocomplex).d_to 0)) _ ≫ (F.right_derived_obj_iso 0 P).inv
theorem
category_theory.abelian.functor.right_derived_zero_to_self_app_comp_inv
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
[category_theory.limits.preserves_finite_limits F]
{X : C}
(P : category_theory.InjectiveResolution X) :
theorem
category_theory.abelian.functor.right_derived_zero_to_self_app_inv_comp
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
[category_theory.limits.preserves_finite_limits F]
{X : C}
(P : category_theory.InjectiveResolution X) :
noncomputable
def
category_theory.abelian.functor.right_derived_zero_to_self_app_iso
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
[category_theory.limits.preserves_finite_limits F]
{X : C}
(P : category_theory.InjectiveResolution X) :
(F.right_derived 0).obj X ≅ F.obj X
Given P : InjectiveResolution X, the isomorphism (F.right_derived 0).obj X ≅ F.obj X if
preserves_finite_limits F.
theorem
category_theory.abelian.functor.right_derived_zero_to_self_natural
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
{X Y : C}
(f : X ⟶ Y)
(P : category_theory.InjectiveResolution X)
(Q : category_theory.InjectiveResolution Y) :
Given P : InjectiveResolution X and Q : InjectiveResolution Y and a morphism f : X ⟶ Y,
naturality of the square given by right_derived_zero_to_self_natural.
noncomputable
def
category_theory.abelian.functor.right_derived_zero_iso_self
{C : Type u}
[category_theory.category C]
{D : Type u}
[category_theory.category D]
(F : C ⥤ D)
[category_theory.abelian C]
[category_theory.abelian D]
[F.additive]
[category_theory.enough_injectives C]
[category_theory.limits.preserves_finite_limits F] :
F.right_derived 0 ≅ F
Given preserves_finite_limits F, the natural isomorphism (F.right_derived 0) ≅ F.