feat(Algebra/Homology): the functor F.rightDerivedFunctorPlus is triangulated

[joelriou]

We also show that when F : C ⥤ D is an additive functor between abelian categories (with enough injectives in C), then the functor F.rightDerivedFunctorPlus which is $$RF : D^+(C) \Rightarrow D^+(D)$$ can be thought not only as a derived functor of the functor induced by F on the bounded below homotopy category, but also as a derived functor of the functor induced by F on the category of bounded below cochain complexes. All the functors and natural transformations that are involved in these constructions are shown to commute with shifts.

---

• depends on: feat(Algebra/Homology/DerivedCategory): the bounded below derived category is also a localization of a category of cochain complexes #43240
• depends on: feat(Algebra/Homology): the bijection of Ext-groups that is induced by an adjunction between exact functors #43086
• depends on: [Merged by Bors] - feat(Algebra/Homology): pseudofunctorial behaviour of Functor.mapDerivedCategory #43089
• depends on: [Merged by Bors] - chore(Algebra/Homology): unexpose HomologicalComplexUpToQuasiIso.Qh #43103
• depends on: [Merged by Bors] - feat(Algebra/Homology): the right derived functor RF : D^+(C) ⥤ D^+(D) #40863
• depends on: [Merged by Bors] - feat(Algebra/Homology/Embedding): various results about truncations #40885
• depends on: [Merged by Bors] - feat(Algebra/Homology): existence of injective resolutions for cochain complexes #40887
• depends on: [Merged by Bors] - feat(CategoryTheory/Shift): left composition with a shift sequence #40888
• depends on: [Merged by Bors] - feat(Algebra/Homology): homological complexes in full subcategories #40892
• depends on: [Merged by Bors] - feat(Algebra/Homology): more on the functoriality of categories of homological complexes #40895
• depends on: [Merged by Bors] - feat(Algebra/Homology): bounded derived categories #40923
• depends on: [Merged by Bors] - feat(Algebra/Homology): the bounded below derived category #40944
• depends on: [Merged by Bors] - feat(CategoryTheory/Localization): small additions #40884
• depends on: [Merged by Bors] - feat(Algebra/Homology): applying an additive functor to the homotopy (co)fiber #40924
• depends on: [Merged by Bors] - feat(Algebra/Homology): the injective derivability structure #41000
• depends on: [Merged by Bors] - feat(Algebra/Homology): the injective derivability structure on the homotopy category #41063
• depends on: feat(CategoryTheory): triangulated derived functors using derivability structures #39128
• depends on: feat(CategoryTheory): pointwise left derived functors using derivability structures #43237
• depends on: [Merged by Bors] - feat(CategoryTheory): right Kan extensions and Guitart exact squares #43063
• depends on: [Merged by Bors] - feat(CategoryTheory/Functor/Derived): derived functors are triangulated #39126
• depends on: [Merged by Bors] - feat(CategoryTheory): the right derived functor commutes with the shift #39117

[github-actions]

PR summary 8af419eb45

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus	1692	1699	+7 (+0.41%)

Import changes for all files

Files	Import difference
Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives	3
Mathlib.Algebra.Homology.DerivedCategory.RightDerivedFunctorPlus	7
Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseLeftDerived (new file)	691
Mathlib.CategoryTheory.Localization.DerivabilityStructure.DerivesTriangulated (new file)	1197
Mathlib.Algebra.Homology.DerivedCategory.Ext.MapAdjunction (new file)	1458

---

Declarations diff (regex)

+ Functor.mapHomotopyCategoryFactors_hom_app
+ QCompιIso
+ _root_.CochainComplex.Plus.localizerMorphism_derives_mapCochainComplexPlus
+ commShiftLift
+ commShift_liftCompιIso_hom
+ extEquiv
+ extEquiv_mk₀
+ extEquiv_mk₀_counit_app
+ extEquiv_naturality_left
+ extEquiv_naturality_left₀
+ extEquiv_naturality_right
+ extEquiv_naturality_right₀
+ extEquiv_symm_mk₀
+ extEquiv_symm_mk₀_unit_app
+ extEquiv_symm_naturality_left
+ extEquiv_symm_naturality_left₀
+ extEquiv_symm_naturality_right
+ extEquiv_symm_naturality_right₀
+ extLinearEquiv
+ hasPointwiseLeftDerivedFunctor
+ hasPointwiseLeftDerivedFunctorAt_iff_of_isLeftDerivabilityStructure
+ hasPointwiseLeftDerivedFunctor_iff_of_isLeftDerivabilityStructure
+ instance (K : CochainComplex.Plus (InjectiveObject C)) :
+ instance : (HomotopyCategory.Plus.quotient C ⋙ Qh).IsLocalization
+ instance : (Q (C := C)).CommShift ℤ := ObjectProperty.commShiftLift ..
+ instance : (Qh : _ ⥤ Plus C).CommShift ℤ
+ instance : (quotient C).CommShift ℤ := ObjectProperty.commShiftLift ..
+ instance : F.mapCochainComplexPlus.CommShift ℤ
+ instance : F.rightDerivedFunctorPlus.CommShift ℤ
+ instance : F.rightDerivedFunctorPlus.IsRightDerivedFunctor
+ instance : F.rightDerivedFunctorPlus.IsTriangulated
+ instance : IsIso (Φ.leftDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂) := by
+ instance : NatTrans.CommShift (QCompιIso C).hom ℤ
+ instance : NatTrans.CommShift (QhCompιIsoιCompQh C).hom ℤ
+ instance : NatTrans.CommShift (quotientCompQhIso C).hom ℤ
+ instance : NatTrans.CommShift (quotientCompιIso C).hom ℤ
+ instance : NatTrans.CommShift F.mapCochainComplexPlusCompι.hom ℤ
+ instance : NatTrans.CommShift F.mapHomotopyCategoryPlusCompι.hom ℤ
+ instance : NatTrans.CommShift F.quotientCompMapHomotopyCategoryPlusIso.hom ℤ
+ instance : NatTrans.CommShift F.rightDerivedFunctorPlusUnit ℤ := by
+ instance : NatTrans.CommShift F.rightDerivedFunctorPlusUnith ℤ
+ instance : Q.IsLocalization (CochainComplex.Plus.quasiIso C)
+ isIso'
+ isIso_iff_of_isLeftDerivabilityStructure
+ isLeftDerivedFunctor_iff_isIso
+ isLeftDerivedFunctor_of_isIso
+ isTriangulated_of_isLeftDerivedFunctor
+ isTriangulated_of_isRightDerivedFunctor
+ leftDerivedFunctorComparison
+ leftDerivedFunctorComparison_fac
+ leftDerivedFunctorComparison_fac_app
+ mapHomotopyCategoryPlusCompι
+ of_comp_faithful
+ of_comp_of_reflectsIsomorphisms
+ quasiIso_iff
+ quasiIso_map_quotient_eq_quasiIso
+ quotientCompMapHomotopyCategoryPlusIso
+ quotientCompQhIso
+ rightDerivedFunctorPlusUnith
+ whiskerRight_quotientCompMapHomotopyCategoryPlusIso_hom_ι
+ whiskerRight_quotientCompQhIso_hom_ι
- instance : (Qh : _ ⥤ Plus C).CommShift ℤ := by
-- instance [F.CommShift A] :

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

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

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 8af419e).

• +85 new declarations
• −4 removed declarations

+CategoryTheory.Adjunction.extEquiv
+CategoryTheory.Adjunction.extEquiv.congr_simp
+CategoryTheory.Adjunction.extEquiv_apply
+CategoryTheory.Adjunction.extEquiv_mk₀
+CategoryTheory.Adjunction.extEquiv_mk₀_counit_app
+CategoryTheory.Adjunction.extEquiv_naturality_left
+CategoryTheory.Adjunction.extEquiv_naturality_left₀
+CategoryTheory.Adjunction.extEquiv_naturality_right
+CategoryTheory.Adjunction.extEquiv_naturality_right₀
+CategoryTheory.Adjunction.extEquiv_symm_apply
+CategoryTheory.Adjunction.extEquiv_symm_mk₀
+CategoryTheory.Adjunction.extEquiv_symm_mk₀_unit_app
+CategoryTheory.Adjunction.extEquiv_symm_naturality_left
+CategoryTheory.Adjunction.extEquiv_symm_naturality_left₀
+CategoryTheory.Adjunction.extEquiv_symm_naturality_right
+CategoryTheory.Adjunction.extEquiv_symm_naturality_right₀
+CategoryTheory.Adjunction.extLinearEquiv
+CategoryTheory.Functor.instCommShiftPlusCochainComplexIntHomMapCochainComplexPlusCompι
+CategoryTheory.Functor.instCommShiftPlusHomotopyCategoryIntUpHomMapHomotopyCategoryPlusCompι
+CategoryTheory.Functor.instCommShiftPlusMapCochainComplexPlusInt
+CategoryTheory.Functor.instCommShiftPlusPlusHomQuotientCompMapHomotopyCategoryPlusIsoInt
+CategoryTheory.Functor.instCommShiftPlusPlusRightDerivedFunctorPlusUnitInt
+CategoryTheory.Functor.instCommShiftPlusPlusRightDerivedFunctorPlusUnithInt
+CategoryTheory.Functor.instCommShiftPlusRightDerivedFunctorPlusInt
+CategoryTheory.Functor.instIsIsoPlusAppPlusRightDerivedFunctorPlusUnitObjInjectiveObjectMapCochainComplexPlusι
+CategoryTheory.Functor.instIsRightDerivedFunctorPlusPlusRightDerivedFunctorPlusRightDerivedFunctorPlusUnithQuasiIso
+CategoryTheory.Functor.instIsTriangulatedPlusRightDerivedFunctorPlus
+CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app
-CategoryTheory.Functor.mapCochainComplexPlusCompι_hom_app_f
+CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app
-CategoryTheory.Functor.mapCochainComplexPlusCompι_inv_app_f
+CategoryTheory.Functor.mapHomotopyCategoryFactors_hom_app
+CategoryTheory.Functor.mapHomotopyCategoryPlusCompι
+CategoryTheory.Functor.mapHomotopyCategoryPlusCompι_hom_app
+CategoryTheory.Functor.mapHomotopyCategoryPlusCompι_inv_app
+CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIso
+CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIso_hom_app_hom
+CategoryTheory.Functor.quotientCompMapHomotopyCategoryPlusIso_inv_app_hom
+CategoryTheory.Functor.rightDerivedFunctorPlus.congr_simp
+CategoryTheory.Functor.rightDerivedFunctorPlusUnit_app
+CategoryTheory.Functor.rightDerivedFunctorPlusUnith
+CategoryTheory.Functor.totalLeftDerived.congr_simp
+CategoryTheory.Functor.whiskerRight_quotientCompMapHomotopyCategoryPlusIso_hom_ι
+CategoryTheory.Functor.whiskerRight_quotientCompMapHomotopyCategoryPlusIso_hom_ι_assoc
+CategoryTheory.LocalizerMorphism.Derives.hasPointwiseLeftDerivedFunctor
+CategoryTheory.LocalizerMorphism.Derives.isIso'
+CategoryTheory.LocalizerMorphism.Derives.isLeftDerivedFunctor_iff_isIso
+CategoryTheory.LocalizerMorphism.Derives.isLeftDerivedFunctor_of_isIso
+CategoryTheory.LocalizerMorphism.Derives.isTriangulated_of_isLeftDerivedFunctor
+CategoryTheory.LocalizerMorphism.Derives.isTriangulated_of_isRightDerivedFunctor
+CategoryTheory.LocalizerMorphism.hasPointwiseLeftDerivedFunctorAt_iff_of_isLeftDerivabilityStructure
+CategoryTheory.LocalizerMorphism.hasPointwiseLeftDerivedFunctor_iff_of_isLeftDerivabilityStructure
+CategoryTheory.LocalizerMorphism.instIsIsoFunctorLeftDerivedFunctorComparison
+CategoryTheory.LocalizerMorphism.isIso_iff_of_isLeftDerivabilityStructure
+CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparison
+CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparison.congr_simp
+CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparison_fac
+CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparison_fac_app
+CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparison_fac_app_assoc
+CategoryTheory.LocalizerMorphism.leftDerivedFunctorComparison_fac_assoc
+CategoryTheory.MorphismProperty.IsInvertedBy.of_comp_of_reflectsIsomorphisms
+CategoryTheory.NatTrans.CommShift.of_comp_faithful
+CategoryTheory.ObjectProperty.commShiftLift
+CategoryTheory.ObjectProperty.commShift_liftCompιIso_hom
-CategoryTheory.ObjectProperty.instCommShiftFullSubcategoryLift
-CategoryTheory.ObjectProperty.instCommShiftHomFunctorLiftCompιIso
+CochainComplex.Plus.localizerMorphism_derives_mapCochainComplexPlus
+CochainComplex.Plus.quasiIso_iff
+DerivedCategory.Plus.QCompιIso
+DerivedCategory.Plus.QCompιIso_hom_app
+DerivedCategory.Plus.QCompιIso_inv_app
+DerivedCategory.Plus.QhCompιIsoιCompQh_hom_app
+DerivedCategory.Plus.QhCompιIsoιCompQh_inv_app
+DerivedCategory.Plus.instCommShiftPlusHomFunctorQCompιIsoInt
+DerivedCategory.Plus.instCommShiftPlusHomFunctorQhCompιIsoιCompQhInt
+DerivedCategory.Plus.instCommShiftPlusHomFunctorQuotientCompQhIsoInt
+DerivedCategory.Plus.instCommShiftPlusQInt
+DerivedCategory.Plus.instIsLocalizationPlusCompPlusQuotientQhQuasiIso
+DerivedCategory.Plus.instIsLocalizationPlusQQuasiIso
+DerivedCategory.Plus.quotientCompQhIso
+DerivedCategory.Plus.quotientCompQhIso_hom_app_hom
+DerivedCategory.Plus.quotientCompQhIso_inv_app_hom
+DerivedCategory.Plus.whiskerRight_quotientCompQhIso_hom_ι
+DerivedCategory.Plus.whiskerRight_quotientCompQhIso_hom_ι_assoc
+HomotopyCategory.Plus.instCommShiftPlusIntUpHomFunctorQuotientCompιIso
+HomotopyCategory.Plus.instCommShiftPlusQuotientInt
+HomotopyCategory.Plus.quasiIso_map_quotient_eq_quasiIso
+HomotopyCategory.Plus.quotientCompιIso_hom_app
+HomotopyCategory.Plus.quotientCompιIso_inv_app

---

Increase in strong tech debt: (relative, absolute) = (1.95, 0.00)

Current number	Change	Type (strong)
backward.defeqAttrib.useBackward	4277	1
backward.isDefEq.respectTransparency	4799	1
backward.isDefEq.respectTransparency.types	2483	3

Increase in weak tech debt: (relative, absolute) = (3.00, 0.00)

Current number	Change	Type (weak)
exposed public sections	5041	3

Current commit 8af419eb45
Reference commit 2fbace17aa

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.py 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).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(Algebra/Homology/DerivedCategory): the bounded below derived category is also a localization of a category of cochain complexes #43240
• feat(Algebra/Homology): the bijection of Ext-groups that is induced by an adjunction between exact functors #43086
• [Merged by Bors] - feat(Algebra/Homology): pseudofunctorial behaviour of Functor.mapDerivedCategory #43089
• [Merged by Bors] - chore(Algebra/Homology): unexpose HomologicalComplexUpToQuasiIso.Qh #43103
• [Merged by Bors] - feat(Algebra/Homology): the right derived functor RF : D^+(C) ⥤ D^+(D) #40863
• [Merged by Bors] - feat(Algebra/Homology/Embedding): various results about truncations #40885
• [Merged by Bors] - feat(Algebra/Homology): existence of injective resolutions for cochain complexes #40887
• [Merged by Bors] - feat(CategoryTheory/Shift): left composition with a shift sequence #40888
• [Merged by Bors] - feat(Algebra/Homology): homological complexes in full subcategories #40892
• [Merged by Bors] - feat(Algebra/Homology): more on the functoriality of categories of homological complexes #40895
• [Merged by Bors] - feat(Algebra/Homology): bounded derived categories #40923
• [Merged by Bors] - feat(Algebra/Homology): the bounded below derived category #40944
• [Merged by Bors] - feat(CategoryTheory/Localization): small additions #40884
• [Merged by Bors] - feat(Algebra/Homology): applying an additive functor to the homotopy (co)fiber #40924
• [Merged by Bors] - feat(Algebra/Homology): the injective derivability structure #41000
• [Merged by Bors] - feat(Algebra/Homology): the injective derivability structure on the homotopy category #41063
• feat(CategoryTheory): triangulated derived functors using derivability structures #39128
• feat(CategoryTheory): pointwise left derived functors using derivability structures #43237
• [Merged by Bors] - feat(CategoryTheory): right Kan extensions and Guitart exact squares #43063
• [Merged by Bors] - feat(CategoryTheory/Functor/Derived): derived functors are triangulated #39126
• [Merged by Bors] - feat(CategoryTheory): the right derived functor commutes with the shift #39117
  By Dependent Issues (🤖). Happy coding!