Zeroth left derived functors #
If F : C ⥤ D
is an additive right exact functor between abelian categories, where C
has enough
projectives, we provide the natural isomorphism F.leftDerived 0 ≅ F
.
Main definitions #
CategoryTheory.Abelian.Functor.leftDerivedZeroIsoSelf
: the natural isomorphism(F.leftDerived 0) ≅ F
.
Main results #
preserves_exact_of_PreservesFiniteColimits_of_epi
: ifPreservesFiniteColimits F
andEpi g
, thenExact (F.map f) (F.map g)
ifexact f g
.
If PreservesFiniteColimits F
and Epi g
, then Exact (F.map f) (F.map g)
if
Exact f g
.
Given P : ProjectiveResolution X
, a morphism (F.leftDerived 0).obj X ⟶ F.obj X
.
Instances For
Given P : ProjectiveResolution X
, a morphism F.obj X ⟶ (F.leftDerived 0).obj X
given
PreservesFiniteColimits F
.
Instances For
Given P : ProjectiveResolution X
, the isomorphism (F.leftDerived 0).obj X ≅ F.obj X
if
PreservesFiniteColimits F
.
Instances For
Given P : ProjectiveResolution X
and Q : ProjectiveResolution Y
and a morphism f : X ⟶ Y
,
naturality of the square given by leftDerived_zero_to_self_obj_hom
.
Given PreservesFiniteColimits F
, the natural isomorphism (F.leftDerived 0) ≅ F
.