Skip to content

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

Closed
joelriou wants to merge 17 commits intomasterfrom
jriou-derivability-structure-pointwise
Closed

feat(CategoryTheory): existence of right derived functors using derivability structures#22508
joelriou wants to merge 17 commits intomasterfrom
jriou-derivability-structure-pointwise

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Mar 3, 2025 •
edited
Loading

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

Open in Gitpod

@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Mar 3, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 3, 2025 •
edited
Loading

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

@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Mar 3, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Mar 3, 2025 •
edited
Loading

This PR/issue depends on:

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 4, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 4, 2025
@joelriou joelriou mentioned this pull request Apr 10, 2025
Closed
3 tasks
@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 28, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Apr 28, 2025

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

@joelriou joelriou mentioned this pull request Apr 29, 2025
Closed
11 tasks
@joelriou joelriou mentioned this pull request Jun 13, 2025
Open
11 tasks
@joelriou joelriou mentioned this pull request Jun 24, 2025
Closed
2 tasks
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jun 24, 2025

This PR has been migrated to a fork-based workflow: #26374

@joelriou joelriou closed this Jun 24, 2025
@YaelDillies YaelDillies deleted the jriou-derivability-structure-pointwise branch August 17, 2025 11:45
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) migrated-to-fork t-category-theory Category theory WIP Work in progress

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@joelriou @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant