Zeroth left derived functors #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
If F : C ⥤ D is an additive right exact functor between abelian categories, where C has enough
projectives, we provide the natural isomorphism F.left_derived 0 ≅ F.
Main definitions #
category_theory.abelian.functor.left_derived_zero_iso_self: the natural isomorphism(F.left_derived 0) ≅ F.
Main results #
preserves_exact_of_preserves_finite_colimits_of_epi: ifpreserves_finite_colimits Fandepi g, thenexact (F.map f) (F.map g)ifexact f g.
theorem
category_theory.abelian.functor.preserves_exact_of_preserves_finite_colimits_of_epi
{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_colimits F]
[category_theory.epi g]
(ex : category_theory.exact f g) :
category_theory.exact (F.map f) (F.map g)
If preserves_finite_colimits F and epi g, then exact (F.map f) (F.map g) if
exact f g.
theorem
category_theory.abelian.functor.exact_of_map_projective_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.ProjectiveResolution X)
[category_theory.limits.preserves_finite_colimits F] :
category_theory.exact (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_to 0) (F.map (P.π.f 0))
@[nolint]
noncomputable
def
category_theory.abelian.functor.left_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_projectives C]
{X : C}
(P : category_theory.ProjectiveResolution X) :
(F.left_derived 0).obj X ⟶ F.obj X
Given P : ProjectiveResolution X, a morphism (F.left_derived 0).obj X ⟶ F.obj X.
Equations
- category_theory.abelian.functor.left_derived_zero_to_self_app F P = (F.left_derived_obj_iso 0 P).hom ≫ homology.desc' (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_to 0) (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_from 0) _ (category_theory.limits.kernel.ι (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_from 0) ≫ F.map (P.π.f 0)) _
noncomputable
def
category_theory.abelian.functor.left_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_projectives C]
[category_theory.limits.preserves_finite_colimits F]
{X : C}
(P : category_theory.ProjectiveResolution X) :
F.obj X ⟶ (F.left_derived 0).obj X
Given P : ProjectiveResolution X, a morphism F.obj X ⟶ (F.left_derived 0).obj X given
preserves_finite_colimits F.
Equations
- category_theory.abelian.functor.left_derived_zero_to_self_app_inv F P = (category_theory.as_iso (category_theory.limits.cokernel.desc (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_to 0) (F.map (P.π.f 0)) _)).inv ≫ category_theory.limits.cokernel.map (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_to 0) (category_theory.limits.kernel.lift (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_from 0) (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_to 0) _) (𝟙 (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).X_prev 0)) (category_theory.limits.kernel.lift (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_from 0) (𝟙 (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).X 0)) _) _ ≫ (homology_iso_cokernel_lift (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_to 0) (((F.map_homological_complex (complex_shape.down ℕ)).obj P.complex).d_from 0) _).inv ≫ (F.left_derived_obj_iso 0 P).inv
theorem
category_theory.abelian.functor.left_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_projectives C]
[category_theory.limits.preserves_finite_colimits F]
{X : C}
(P : category_theory.ProjectiveResolution X) :
theorem
category_theory.abelian.functor.left_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_projectives C]
[category_theory.limits.preserves_finite_colimits F]
{X : C}
(P : category_theory.ProjectiveResolution X) :
noncomputable
def
category_theory.abelian.functor.left_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_projectives C]
[category_theory.limits.preserves_finite_colimits F]
{X : C}
(P : category_theory.ProjectiveResolution X) :
(F.left_derived 0).obj X ≅ F.obj X
Given P : ProjectiveResolution X, the isomorphism (F.left_derived 0).obj X ≅ F.obj X if
preserves_finite_colimits F.
theorem
category_theory.abelian.functor.left_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_projectives C]
{X Y : C}
(f : X ⟶ Y)
(P : category_theory.ProjectiveResolution X)
(Q : category_theory.ProjectiveResolution Y) :
Given P : ProjectiveResolution X and Q : ProjectiveResolution Y and a morphism f : X ⟶ Y,
naturality of the square given by `left_derived_zero_to_self_obj_hom.
noncomputable
def
category_theory.abelian.functor.left_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_projectives C]
[category_theory.limits.preserves_finite_colimits F] :
F.left_derived 0 ≅ F
Given preserves_finite_colimits F, the natural isomorphism (F.left_derived 0) ≅ F.