instance
leftDerived_additive
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.Abelian C]
[CategoryTheory.HasProjectiveResolutions C]
{D : Type u_1}
[CategoryTheory.Category.{u_2, u_1} D]
[CategoryTheory.Abelian D]
(F : CategoryTheory.Functor C D)
[F.Additive]
(n : ℕ)
:
(F.leftDerived n).Additive
instance
lemma_23_77
(R : Type u)
[CommRing R]
(n : ℕ)
(M : ModuleCat R)
:
((CategoryTheory.Tor (ModuleCat R) n).obj M).Additive