Object properties of homology and left derived functors #
A property closed under subobjects and quotients passes from the degree-i term of a complex
to its degree-i homology. If an additive functor sends projective objects to objects with this
property, all its left derived functors take values in the same class. In particular, tensor
closure of a Serre class implies its closure under Tor.
References #
- C. A. Weibel, An Introduction to Homological Algebra, Section 2.4.
theorem
CategoryTheory.ObjectProperty.prop_homology
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
[P.IsClosedUnderSubobjects]
[P.IsClosedUnderQuotients]
[Limits.HasZeroMorphisms C]
{ι : Type u_1}
{c : ComplexShape ι}
(K : HomologicalComplex C c)
(i : ι)
[K.HasHomology i]
(h : P (K.X i))
:
P (K.homology i)
A property closed under subobjects and quotients passes from a term of a complex to homology in the same degree, whenever that homology exists.
theorem
CategoryTheory.ObjectProperty.prop_leftDerived_obj
{C : Type u}
[Category.{v, u} C]
(P : ObjectProperty C)
[P.IsClosedUnderSubobjects]
[P.IsClosedUnderQuotients]
[Abelian C]
{D : Type u'}
[Category.{v', u'} D]
[Abelian D]
[HasProjectiveResolutions D]
(F : Functor D C)
[F.Additive]
(hF : ∀ (Y : D) [Projective Y], P (F.obj Y))
(X : D)
(n : ℕ)
:
P ((F.leftDerived n).obj X)
If an additive functor sends every projective object into a class closed under subobjects and quotients, all its left derived functors take values in that class.