feat(CategoryTheory): the left derived functor commutes with the shift

[joelriou]

This dualized the result in #39117.

---

• depends on: feat(CategoryTheory): the right derived functor commutes with the shift #39117

[github-actions]

PR summary c9f4f1b787

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Functor.Derived.LeftDerived	463	467	+4 (+0.86%)
Mathlib.CategoryTheory.Functor.Derived.RightDerived	463	467	+4 (+0.86%)

Import changes for all files

Files	Import difference
3 files Mathlib.CategoryTheory.Functor.Derived.Adjunction Mathlib.CategoryTheory.Functor.Derived.LeftDerived Mathlib.CategoryTheory.Functor.Derived.RightDerived	4
Mathlib.CategoryTheory.Functor.Derived.LeftDerivedCommShift (new file) Mathlib.CategoryTheory.Functor.Derived.RightDerivedCommShift (new file)	502

---

Declarations diff

+ comp_map_commShiftIso_hom_app
+ instance (g : G) : (W.shiftLocalizerMorphism g).IsLocalizedEquivalence
+ instance (α : F ⟶ L ⋙ F') (G : H ⥤ H') [G.IsEquivalence] [F'.IsLeftKanExtension α] :
+ instance (β : L ⋙ F' ⟶ F) (G : H ⥤ H') [G.IsEquivalence] [F'.IsRightKanExtension β] :
+ instance [G.IsEquivalence] : (LeftExtension.postcompose₂ L F G).IsEquivalence := by
+ instance [G.IsEquivalence] : (RightExtension.postcompose₂ L F G).IsEquivalence := by
+ instance [HasLeftDerivedFunctor F W] :
+ instance [HasRightDerivedFunctor F W] :
+ isLeftDerivedFunctor_iff_precomp
+ isLeftKanExtension_iff_precomp_equivalence
+ isLeftKanExtension_postcompose₂_iff
+ isRightDerivedFunctor_iff_precomp
+ isRightKanExtension_iff_precomp_equivalence
+ isRightKanExtension_postcompose₂_iff
+ map_commShiftIso_hom_app_comp
++ commShift
++ instance (G : H ⥤ H') [G.IsEquivalence] :
++ natTrans_commShift
++ postcomposeShiftNatTrans
++ precomposeShiftNatTrans
++++ instance :

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.

---

No changes to strong technical debt.

No changes to weak technical debt.

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(CategoryTheory): the right derived functor commutes with the shift #39117
  By Dependent Issues (🤖). Happy coding!