CategoryTheory.InjectiveResolution.desc_commutes

theorem CategoryTheory.InjectiveResolution.desc_commutes : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C} (f : Z ⟶ Y) (I : CategoryTheory.InjectiveResolution Y) (J : CategoryTheory.InjectiveResolution Z), CategoryTheory.CategoryStruct.comp J.ι (CategoryTheory.InjectiveResolution.desc f I J) = CategoryTheory.CategoryStruct.comp ((CochainComplex.single₀ C).map f) I.ι

This theorem states that for any two objects `Y` and `Z` in an abelian category `C` and a morphism `f` from `Z` to `Y`, the resolution maps intertwine the descent of the morphism `f` and the morphism itself. More concretely, if `I` is an injective resolution of `Y` and `J` is an injective resolution of `Z`, then the composition of `J.ι` and the descent of `f` from `I` to `J` is equal to the composition of `f` mapped through the functor `CochainComplex.single₀ C` and `I.ι`. In other words, the diagram commutes in the category of cochain complexes.

More concisely: Given abelian categories `C`, objects `Y` and `Z`, and injective resolutions `I` of `Y` and `J` of `Z`, the diagram commutes in the category of cochain complexes between `CochainComplex.single₀ C(J.ι, I.ι)` and `J.ι ∘ f ∘ I.ι`, where `f` is a morphism from `Z` to `Y`.