noncomputable def rightDerivedZero_obj_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] [CategoryTheory.Limits.PreservesFiniteLimits F] (X : C) : (F.rightDerived 0).obj X ≅ F.obj X

For a left-exact additive functor F : C ⥤ D, the zeroth right derived functor of F evaluated at X is naturally isomorphic to F.obj X.

theorem rightDerived_injective_is_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) (X : C) [CategoryTheory.Injective X] (hn : 0 < n) : CategoryTheory.Limits.IsZero ((F.rightDerived n).obj X)

For an additive functor F, the positive-degree right derived functors vanish on injective objects: R^n F (X) = 0 for n > 0 and X injective.

structure ResolutionIndependence {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.EnoughInjectives C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : Prop

Placeholder statement that the right derived functors of F are independent of the chosen injective resolution.

• obj_determined (n : ℕ) (X : C) : ∃! x : (F.rightDerived n).obj X = (F.rightDerived n).obj X, True

theorem effaceable_implies_universal_uniqueness {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] (T : DerivedFunctorsDefs.CohomDeltaFunctor C D) (hT : T.IsEffaceable) (G : DerivedFunctorsDefs.CohomDeltaFunctor C D) (m₁ m₂ : T.Morphism G) : m₁.η 0 = m₂.η 0 → ∀ (n : ℕ), m₁.η n = m₂.η n

Uniqueness part of universality: any two morphisms of δ-functors out of an effaceable δ-functor T that agree in degree zero must agree in every degree.

theorem effaceable_implies_universal_existence {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] (T : DerivedFunctorsDefs.CohomDeltaFunctor C D) (hT : T.IsEffaceable) (G : DerivedFunctorsDefs.CohomDeltaFunctor C D) (η₀ : T.T 0 ⟶ G.T 0) : ∃ (m : T.Morphism G), m.η 0 = η₀

Existence part of universality: every map in degree zero out of an effaceable δ-functor T extends to a morphism of δ-functors.

theorem effaceable_implies_universal {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] (T : DerivedFunctorsDefs.CohomDeltaFunctor C D) (hT : T.IsEffaceable) : T.IsUniversal

An effaceable δ-functor is a universal δ-functor (Definition 45, Lecture 22–23): combining existence and uniqueness yields universality.