Functoriality of the injective-resolution presentation of Ext

Mathlib identifies Ext X Y n with cohomology classes of degree n from X to a chosen injective resolution of Y, through InjectiveResolution.extEquivCohomologyClass, but records no compatibility of that identification with a morphism in the second variable.

That compatibility is what a comparison theorem needs when the target sheaf varies — and in particular it is what makes a scalar action visible on Ext: multiplication by a scalar is an endomorphism of the sheaf, and the resolution presentation must carry it to the corresponding endomorphism of the resolution.

The identification is post-composition with the augmentation R.ι', so the proof is the associativity of composition in SmallShiftedHom, once cohomology classes are equipped with their own post-composition.

noncomputable def CategoryTheory.InjectiveResolution.descHom {C : Type u} [Category.{v, u} C] [Abelian C] {Y Y' : C} (φ : Y ⟶ Y') (R : InjectiveResolution Y) (R' : InjectiveResolution Y') : R.Hom R' φ

The canonical lift of a morphism to chosen injective resolutions.

InjectiveResolution.desc produces the map of ℕ-indexed resolutions; this packages it with its degree-zero commutation, so that Hom.hom' and Hom.ι'_comp_hom' supply the lifted chain map and the square it satisfies.

Equations

• CategoryTheory.InjectiveResolution.descHom φ R R' = { hom := CategoryTheory.InjectiveResolution.desc φ R' R, ι_f_zero_comp_hom_f_zero := ⋯ }

@[simp]

theorem CategoryTheory.InjectiveResolution.descHom_hom {C : Type u} [Category.{v, u} C] [Abelian C] {Y Y' : C} (φ : Y ⟶ Y') (R : InjectiveResolution Y) (R' : InjectiveResolution Y') : (descHom φ R R').hom = desc φ R' R

The underlying map of resolutions is Mathlib's desc; this is stated so that later rewrites never need to unfold descHom.

theorem CategoryTheory.InjectiveResolution.extEquivCohomologyClass_naturality {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {X Y Y' : C} {n : ℕ} (R : InjectiveResolution Y) (R' : InjectiveResolution Y') (φ : Y ⟶ Y') (Φ : R.cochainComplex ⟶ R'.cochainComplex) (hΦ : CategoryStruct.comp R.ι' Φ = CategoryStruct.comp ((CochainComplex.singleFunctor C 0).map φ) R'.ι') (α : Abelian.Ext X Y n) : R'.extEquivCohomologyClass (α.comp (Abelian.Ext.mk₀ φ) ⋯) = (CochainComplex.HomComplex.CohomologyClass.postcomp Φ) (R.extEquivCohomologyClass α)

The injective-resolution presentation of Ext is compatible with a morphism in the second variable, once that morphism is lifted to the resolutions.

The lift is an explicit hypothesis rather than a chosen descent: the Proj lane passes its comparison data positionally, and a chosen lift would reintroduce exactly the ambiguity that convention exists to remove. InjectiveResolution.Hom.hom' supplies hΦ for the canonical lift of φ.