feat(CategoryTheory): existence of right derived functors using derivability structures

[joelriou]

In this PR, we formalize an existence theorem for right derived functors which appeared in the article Structures de dérivabilité by Bruno Kahn and Georges Maltsiniotis, Adv. Math. 218 (2008).

---

• depends on: [Merged by Bors] - feat(CategoryTheory/Functor): pointwise right derived functors #26036
• depends on: feat(CategoryTheory): Guitart exact squares and Kan extensions #30382

This PR continues the work from #22508.

Original PR: #22508

[joelriou]

Comments from Original PR #22508

This section contains 1 comment(s) from the original PR, excluding bot comments.

---

@github-actions (2025-03-03 17:04 UTC):

PR summary 5d11a5f926

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.Functor.Derived.PointwiseRightDerived (new file)	474
Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (new file)	643

---

Declarations diff

+ HasPointwiseRightDerivedFunctor
+ HasPointwiseRightDerivedFunctorAt
+ LeftExtension.isPointwiseLeftKanExtensionOfIsIso
+ hasColimit_comp_iff
+ hasLimit_comp_iff
+ hasLimit_equivalence_comp
+ hasLimit_of_equivalence_comp
+ hasPointwiseLeftKanExtensionAt_iff_of_equivalence
+ hasPointwiseLeftKanExtensionAt_iff_of_iso
+ hasPointwiseLeftKanExtensionAt_iff_of_iso'
+ hasPointwiseLeftKanExtensionAt_of_equivalence
+ hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor
+ hasPointwiseRightDerivedFunctorAt_iff
+ hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure
+ hasPointwiseRightDerivedFunctorAt_iff_of_mem
+ hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure
+ hasPointwiseRightDerivedFunctor_of_inverts
+ hasPointwiseRightKanExtensionAt_iff_of_equivalence
+ hasPointwiseRightKanExtensionAt_iff_of_iso
+ hasPointwiseRightKanExtensionAt_iff_of_iso'
+ hasPointwiseRightKanExtensionAt_of_equivalence
+ hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor
+ instance :
+ isIso_comp_left_iff
+ isIso_comp_right_iff
+ isIso_α_iff_of_isRightDerivabilityStructure
+ isPointwiseLeftKanExtensionAtEquivOfIso'
+ isPointwiseLeftKanExtensionAtOfIso
+ isPointwiseLeftKanExtensionAtOfIso'
+ isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor
+ isPointwiseLeftKanExtensionOfIso
+ isPointwiseRightKanExtensionAtEquivOfIso'
+ isPointwiseRightKanExtensionAtOfIso'
+ rightDerivedFunctorComparison
+ rightDerivedFunctorComparison_fac
+ rightDerivedFunctorComparison_fac_app

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).

[github-actions]

PR summary cc0d5cbbe4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.CategoryTheory.GuitartExact.KanExtension (new file)	638
Mathlib.CategoryTheory.Localization.DerivabilityStructure.PointwiseRightDerived (new file)	679

---

Declarations diff

+ IsPointwiseLeftKanExtension.compTwoSquare
+ compTwoSquare
+ hasColimit_comp_iff
+ hasLeftKanExtension
+ hasLimit_comp_iff
+ hasPointwiseLeftKanExtension
+ hasPointwiseLeftKanExtensionAt_iff
+ hasPointwiseLeftKanExtension_iff
+ hasPointwiseRightDerivedFunctorAt_iff_of_isRightDerivabilityStructure
+ hasPointwiseRightDerivedFunctor_iff_of_isRightDerivabilityStructure
+ instance (Y : D) : Subsingleton (E.IsPointwiseLeftKanExtensionAt Y)
+ instance (Y : D) : Subsingleton (E.IsPointwiseRightKanExtensionAt Y)
+ instance : IsIso (Φ.rightDerivedFunctorComparison L₁ L₂ F F₁ α₁ F₂ α₂) := by
+ isIso_comp_left_iff
+ isIso_comp_right_iff
+ isIso_α_iff_of_isRightDerivabilityStructure
+ isPointwiseLeftKanExtensionAtCompTwoSquareEquiv
+ isPointwiseLeftKanExtensionEquivOfGuitartExact
+ isPointwiseLeftKanExtensionOfCompTwoSquare
+ nonempty_isPointwiseLeftKanExtensionAt_compTwoSquare_iff
+ rightDerivedFunctorComparison
+ rightDerivedFunctorComparison_fac
+ rightDerivedFunctorComparison_fac_app

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).

[leanprover-community-bot-assistant]

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

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - feat(CategoryTheory/Functor): pointwise right derived functors #26036
• feat(CategoryTheory): Guitart exact squares and Kan extensions #30382
  By Dependent Issues (🤖). Happy coding!