def AdjustedResolutions.IsAdjustedToFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (M : C) : Prop

An object M is adjusted to an additive functor F if all higher right derived functors of F vanish on M: RⁱF(M) = 0 for i > 0. Such objects (e.g. injectives, or F-acyclic objects) can be used in place of injective resolutions when computing RF.

structure AdjustedResolutions.Resolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (M : C) : Type (max u v)

A resolution of an object M in an abelian category: a cochain complex K• together with a quasi-isomorphism M[0] → K• from the complex concentrated in degree zero.

• cocomplex : CochainComplex C ℕ
• hasHomology (i : ℕ) : HomologicalComplex.HasHomology self.cocomplex i
• ι : (CochainComplex.single₀ C).obj M ⟶ self.cocomplex
• quasiIso : QuasiIso self.ι

def AdjustedResolutions.InjectiveResolution.toResolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {M : C} (I : CategoryTheory.InjectiveResolution M) : Resolution M

Every injective resolution is in particular a resolution.

theorem AdjustedResolutions.injective_isAdjustedToFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (M : C) [CategoryTheory.Injective M] : IsAdjustedToFunctor F M

Any injective object is adjusted to every additive functor: RⁱF(M) = 0 for i > 0 when M is injective.

theorem AdjustedResolutions.injRes_objects_adjusted {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] {M : C} (I : CategoryTheory.InjectiveResolution M) (n : ℕ) : IsAdjustedToFunctor F (I.cocomplex.X n)

Every object in an injective resolution is adjusted to any additive functor F.

theorem AdjustedResolutions.prop43_canonical_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {M : C} (K : Resolution M) : Nonempty ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K.cocomplex) ⟶ (F.rightDerived n).obj M)

Canonical map from the homology of F(K•) to the right derived functor RⁿF(M) for any resolution K• → M.

theorem AdjustedResolutions.prop43_adjusted_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions C] {D : Type u_1} [CategoryTheory.Category.{u_2, u_1} D] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] (n : ℕ) {M : C} (K : Resolution M) (hadj : ∀ (i : ℕ), IsAdjustedToFunctor F (K.cocomplex.X i)) : Nonempty ((HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj K.cocomplex) ≅ (F.rightDerived n).obj M)

Proposition 43: if every term of a resolution K• → M is F-adjusted, then RⁿF(M) may be computed as Hⁿ(F(K•)) — i.e., adjusted resolutions compute derived functors.

noncomputable def AdjustedResolutions.prop43_injective_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions 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} (I : CategoryTheory.InjectiveResolution X) : (F.rightDerived n).obj X ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex)

Specialization of Prop 43 to an injective resolution: RⁿF(X) ≃ Hⁿ(F(I•)).

noncomputable def AdjustedResolutions.prop43_resolution_uniqueness {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasInjectiveResolutions 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} (I J : CategoryTheory.InjectiveResolution X) : (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj I.cocomplex) ≅ (HomologicalComplex.homologyFunctor D (ComplexShape.up ℕ) n).obj ((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj J.cocomplex)

Independence of the choice of injective resolution: two injective resolutions of X give canonically isomorphic computations of RⁿF(X).