structure DerivedFunctorsDefs.CohomDeltaFunctor (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (D : Type u_1) [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] : Type (max (max (max u u_1) u_2) v)

A cohomological δ-functor (Definition 43, Lecture 22–23): a sequence of additive functors T n : C ⥤ D together with connecting morphisms δ and the long-exact-sequence and naturality data attached to each short exact sequence in C.

• T : ℕ → CategoryTheory.Functor C D
• additive (n : ℕ) : (self.T n).Additive
• leftExact : CategoryTheory.Limits.PreservesFiniteLimits (self.T 0)
• δ (n : ℕ) (S : CategoryTheory.ShortComplex C) : S.ShortExact → ((self.T n).obj S.X₃ ⟶ (self.T (n + 1)).obj S.X₁)
• exact_middle (n : ℕ) (S : CategoryTheory.ShortComplex C) : S.ShortExact → { X₁ := (self.T n).obj S.X₁, X₂ := (self.T n).obj S.X₂, X₃ := (self.T n).obj S.X₃, f := (self.T n).map S.f, g := (self.T n).map S.g, zero := ⋯ }.Exact
• comp_δ_zero (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) : CategoryTheory.CategoryStruct.comp ((self.T n).map S.g) (self.δ n S hS) = 0
• δ_comp_zero (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) : CategoryTheory.CategoryStruct.comp (self.δ n S hS) ((self.T (n + 1)).map S.f) = 0
• exact_right (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) : { X₁ := (self.T n).obj S.X₂, X₂ := (self.T n).obj S.X₃, X₃ := (self.T (n + 1)).obj S.X₁, f := (self.T n).map S.g, g := self.δ n S hS, zero := ⋯ }.Exact
• exact_left (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) : { X₁ := (self.T n).obj S.X₃, X₂ := (self.T (n + 1)).obj S.X₁, X₃ := (self.T (n + 1)).obj S.X₂, f := self.δ n S hS, g := (self.T (n + 1)).map S.f, zero := ⋯ }.Exact
• δ_natural (n : ℕ) (S S' : CategoryTheory.ShortComplex C) (hS : S.ShortExact) (hS' : S'.ShortExact) (φ : S ⟶ S') : CategoryTheory.CategoryStruct.comp ((self.T n).map φ.τ₃) (self.δ n S' hS') = CategoryTheory.CategoryStruct.comp (self.δ n S hS) ((self.T (n + 1)).map φ.τ₁)

structure DerivedFunctorsDefs.CohomDeltaFunctor.Morphism {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F G : CohomDeltaFunctor C D) : Type (max u u_2)

A morphism of cohomological δ-functors F ⟶ G is a sequence of natural transformations η n : F.T n ⟶ G.T n compatible with the connecting maps δ of F and G.

• η (n : ℕ) : F.T n ⟶ G.T n
• comm_δ (n : ℕ) (S : CategoryTheory.ShortComplex C) (hS : S.ShortExact) : CategoryTheory.CategoryStruct.comp ((self.η n).app S.X₃) (G.δ n S hS) = CategoryTheory.CategoryStruct.comp (F.δ n S hS) ((self.η (n + 1)).app S.X₁)

structure DerivedFunctorsDefs.CohomDeltaFunctor.IsUniversal {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CohomDeltaFunctor C D) : Prop

The universal property defining a derived functor (Definition 44–45, Lecture 22–23): a δ-functor F is universal if every degree-zero natural transformation F.T 0 ⟶ G.T 0 extends uniquely to a morphism of δ-functors.

• extend (G : CohomDeltaFunctor C D) (η₀ : F.T 0 ⟶ G.T 0) : ∃ (m : F.Morphism G), m.η 0 = η₀
• unique (G : CohomDeltaFunctor C D) (m₁ m₂ : F.Morphism G) : m₁.η 0 = m₂.η 0 → ∀ (n : ℕ), m₁.η n = m₂.η n

noncomputable def DerivedFunctorsDefs.rightDerivedFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) : CategoryTheory.Functor C D

The n-th right derived functor of an additive functor F : C ⥤ D.

noncomputable def DerivedFunctorsDefs.rightDerivedNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Abelian D] {F G : CategoryTheory.Functor C D} [F.Additive] [G.Additive] (α : F ⟶ G) (n : ℕ) : rightDerivedFunctor F n ⟶ rightDerivedFunctor G n

The induced natural transformation between n-th right derived functors from a natural transformation F ⟶ G.

noncomputable def DerivedFunctorsDefs.rightDerivedZeroIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] : rightDerivedFunctor F 0 ≅ F

For a left-exact additive functor, the zeroth right derived functor is naturally isomorphic to the functor itself.

theorem DerivedFunctorsDefs.rightDerived_injective_vanishing {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Injective X] : CategoryTheory.Limits.IsZero ((rightDerivedFunctor F (n + 1)).obj X)

Right derived functors in positive degree vanish on injective objects.

noncomputable def DerivedFunctorsDefs.toRightDerivedZero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_2} [CategoryTheory.Category.{u_3, u_2} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : F ⟶ rightDerivedFunctor F 0

The canonical natural transformation from F to its zeroth right derived functor.