feat(CategoryTheory): computing Ext-groups using an injective resolution

[joelriou]

Given an injective resolution R of an object Y in an abelian category, we define a constructor for elements in Ext X Y n which takes as input "cocycles" given as morphisms X ⟶ R.cocomplex.X n, and we provide API for this definition.

When the dual construction for projective resolution will be done, it will be possible to remove the old Ext API.

DRAFT

---

• depends on: [Merged by Bors] - feat(CategoryTheory): injective resolutions as cochain complexes indexed by the integers #32003
• depends on: feat(Algebra/Homology): cohomology of HomComplex and morphisms in the homotopy category #32093
• depends on: [Merged by Bors] - feat(Algebra/Homology): cohomology of HomComplex #32091
• depends on: feat(Algebra/Homology): cochains/cocycles from/to single complexes #32097
• depends on: feat(Algebra/Homology): morphisms to K-injective complexes in the derived category #31900
• depends on: [Merged by Bors] - feat(Algebra/Homology): K-injective cochain complexes #31941
• depends on: [Merged by Bors] - feat(CategoryTheory/Triangulated): right orthogonal and localization #31843

[github-actions]

PR summary c36d1388e6

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ CochainComplex.IsKInjective.Qh_map_bijective
+ CohomologyClass
+ EqUpTo
+ HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE
+ IsKInjective
+ IsKInjective.rightOrthogonal
+ Q_map_eq_of_homotopy
+ _root_.HomotopyEquiv.isKInjective
+ bijective_toSmallShiftedHom_of_isKInjective
+ coboundaries
+ cochainComplex
+ cochainComplexXIso
+ cochainComplex_d
+ comp_mk₀_id
+ descAddMonoidHom
+ descAddMonoidHom_cohomologyClass
+ equivHomShift
+ equivOfIsKInjective
+ equiv_mk₀Inv
+ equiv_toSmallShiftedHom_mk
+ exists_iso_singleFunctor_obj_of_isGE_of_isLE
+ extEquivCohomologyClass
+ extMk
+ extMk_surjective
+ extendSingleIso
+ extendSingleIso_hom_f
+ extendSingleIso_inv_f
+ extend_single_d
+ fromSingleEquiv
+ fromSingleMk_v
+ fromSingleMk_v_eq_zero
+ fromSingleMk_zero
+ homAddEquiv
+ homologyAddEquiv
+ instance (L : CochainComplex C ℤ) [hL : L.IsKInjective] (n : ℤ) :
+ instance (X : CochainComplex C ℕ) :
+ instance (n : ℤ) : Injective (R.cochainComplex.X n) := by
+ instance : AddCommGroup (CohomologyClass K L n)
+ instance : QuasiIso R.ι' := by dsimp [ι']; infer_instance
+ instance : R.cochainComplex.IsKInjective := isKInjective_of_injective _ 0
+ instance : R.cochainComplex.IsLE 0 := by
+ instance [HasExt.{w} C] (K L : CochainComplex C ℤ)
+ instance [HasExt.{w} C] (X Y : C) (a b : ℤ) [HasDerivedCategory.{w'} C] :
+ instance [∀ j, K.HasHomology j] [∀ j, L.HasHomology j] [QuasiIso φ] :
+ isKInjective_iff_of_iso
+ isKInjective_iff_rightOrthogonal
+ isKInjective_of_injective
+ isKInjective_of_injective_aux
+ isKInjective_of_iso
+ isKInjective_shift_iff
+ isKernel
+ isLocal_trW
+ isSupported_iff_of_quasiIso
+ leftHomologyData
+ leftHomologyData'
+ limitSequence
+ limitSequence_eqUpTo
+ mk
+ mkAddMonoidHom
+ mk_add
+ mk_eq_zero_iff
+ mk_neg
+ mk_sub
+ mk_surjective
+ mk_zero
+ mk₀Inv
+ mk₀Inv_comp_mk₀
+ mk₀_comp_mk₀Inv
+ mk₀_id_comp
+ postcompEquiv
+ precompEquiv
+ quotient_map_eq_zero_iff
+ quotient_obj_mem_subcategoryAcyclic_iff_acyclic
+ rightOrthogonal.map_bijective_of_isTriangulated
+ rightShiftAddEquiv
+ sequence
+ sequence_eqUpTo
+ single
+ singleFunctor_obj_d
+ single_v
+ single_v_eq_zero
+ single_v_eq_zero'
+ single_zero
+ toCochainAddMonoidHom
+ toHom
+ toHom_bijective
+ toHom_mk
+ toHom_mk_eq_zero_iff
+ toSingleMk_v
+ toSingleMk_v_eq_zero
+ toSingleMk_zero
+ toSmallShiftedHom
+ toSmallShiftedHom_mk
+ δ_fromSingleMk
+ δ_single
+ δ_toSingleMk
+ ι'
+ ι'_f_zero
++ fromSingleMk
++ fromSingleMk_surjective
++ instance : R.cochainComplex.IsStrictlyGE 0 := by
++ toSingleMk

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory): injective resolutions as cochain complexes indexed by the integers #32003
• feat(Algebra/Homology): cohomology of HomComplex and morphisms in the homotopy category #32093
• [Merged by Bors] - feat(Algebra/Homology): cohomology of HomComplex #32091
• feat(Algebra/Homology): cochains/cocycles from/to single complexes #32097
• feat(Algebra/Homology): morphisms to K-injective complexes in the derived category #31900
• [Merged by Bors] - feat(Algebra/Homology): K-injective cochain complexes #31941
• [Merged by Bors] - feat(CategoryTheory/Triangulated): right orthogonal and localization #31843
  By Dependent Issues (🤖). Happy coding!

[mathlib4-merge-conflict-bot]

This pull request has conflicts, please merge master and resolve them.