Skip to content

[Merged by Bors] - feat(CategoryTheory): deriving functors using a right derivability structure#31400

Closed
joelriou wants to merge 25 commits intoleanprover-community:masterfrom
joelriou:jriou-derivability-structure-right-derives
Closed

[Merged by Bors] - feat(CategoryTheory): deriving functors using a right derivability structure#31400
joelriou wants to merge 25 commits intoleanprover-community:masterfrom
joelriou:jriou-derivability-structure-right-derives

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Nov 8, 2025 •
edited
Loading

We develop the API for derived functors following the existence theorem obtained in #26374. If Φ is a localizer morphism, we introduce a predicate Φ.Derives F for a functor F saying that Φ.functor ⋙ F inverts the given class of morphisms, and in case Φ is a right derivability structure, we show that F admits a right derived functor, and we obtain a recognition lemma for this derived functor.

(In the future, this will be applied to the injective/projective/flat derivability structures.)

Open in Gitpod

joelriou added 21 commits March 2, 2025 23:05
@joelriou
feat(CategoryTheory/Functor): more API for pointwise Kan extensions
5fd2ea0
@joelriou
fix
00d0b33
@joelriou
hasPointwiseRightDerivedFunctor_of_inverts
67d0b6f
@joelriou
docstrings
c430ddb
@joelriou
wip
a15edbb
@joelriou
feat: existence of right derived functors
563e1b9
@joelriou
wip
40ce537
@joelriou
fix
9bc2879
@joelriou
Merge remote-tracking branch 'origin/fix-haslimitofiso' into jriou-de…
6313417 
…rivability-structure-pointwise
@joelriou
Merge remote-tracking branch 'origin' into jriou-kan-extension-pointw…
a175b17 
…ise-more-api
@joelriou
fix
2c05585
@joelriou
Merge remote-tracking branch 'origin' into jriou-derivability-structu…
9d58cd9 
…re-pointwise
@joelriou
Merge remote-tracking branch 'origin' into jriou-kan-extension-pointw…
de410bf 
…ise-more-api
@joelriou
Merge remote-tracking branch 'origin/jriou-kan-extension-pointwise-mo…
481fab3 
…re-api' into jriou-pointwise-right-derived-functor
@joelriou
Merge remote-tracking branch 'origin/jriou-pointwise-right-derived-fu…
9ff71c6 
…nctor' into jriou-derivability-structure-pointwise
@joelriou
Merge remote-tracking branch 'origin' into jriou-derivability-structu…
4d50419 
…re-pointwise
@joelriou
feat(CategoryTheory): deriving functors using a right derivability st…
fa1a86a 
…ructure
@joelriou
Merge remote-tracking branch 'origin' into jriou-derivability-structu…
5e87ba6 
…re-right-derives
@joelriou
Merge remote-tracking branch 'origin' into jriou-derivability-structu…
32df3bc 
…re-right-derives
@joelriou
Merge remote-tracking branch 'origin/master' into jriou-derivability-…
8f37e4d 
…structure-right-derives
@joelriou
Merge remote-tracking branch 'origin/master' into jriou-derivability-…
2b0c00d 
…structure-right-derives
@joelriou joelriou added WIP Work in progress t-category-theory Category theory labels Nov 8, 2025
@joelriou joelriou mentioned this pull request Nov 8, 2025
Closed
3 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 8, 2025 •
edited
Loading

PR summary ad50da1508

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Localization.DerivabilityStructure.Derives (new file) 691

Declarations diff

+ Derives
+ hasPointwiseRightDerivedFunctor
+ instance [L.IsLocalization W] (hF : W.IsInvertedBy F) :
+ isIso
+ isIso_iff_of_isRightDerivabilityStructure
+ isIso_of_isRightDerivedFunctor_of_inverts
+ isRightDerivedFunctor_iff_isIso
+ isRightDerivedFunctor_iff_of_inverts
+ isRightDerivedFunctor_of_inverts
+ isRightDerivedFunctor_of_isIso

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

@joelriou joelriou removed the WIP Work in progress label Nov 8, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Nov 8, 2025

This PR/issue depends on:

erdOne
erdOne reviewed Nov 15, 2025
View reviewed changes
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
Comment thread Mathlib/CategoryTheory/Localization/DerivabilityStructure/Derives.lean Outdated
Comment thread Mathlib/CategoryTheory/Localization/DerivabilityStructure/Derives.lean Outdated
@erdOne erdOne added the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 15, 2025
@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Nov 16, 2025

Thanks @erdOne for the reviews!

@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Nov 16, 2025
erdOne
erdOne reviewed Nov 16, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@erdOne erdOne left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!
maintainer merge

@github-actions
Copy link
Copy Markdown

github-actions bot commented Nov 16, 2025

🚀 Pull request has been placed on the maintainer queue by erdOne.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Nov 16, 2025
@riccardobrasca
Copy link
Copy Markdown
Member

riccardobrasca commented Nov 16, 2025

Thanks!

bors merge

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Nov 16, 2025
mathlib-bors bot pushed a commit that referenced this pull request Nov 16, 2025
@joelriou
feat(CategoryTheory): deriving functors using a right derivability st…
f17d16e 
…ructure (#31400)

We develop the API for derived functors following the existence theorem obtained in #26374. If `Φ` is a localizer morphism, we introduce a predicate `Φ.Derives F` for a functor `F` saying that `Φ.functor ⋙ F` inverts the given class of morphisms, and in case `Φ` is a right derivability structure, we show that `F` admits a right derived functor, and we obtain a recognition lemma for this derived functor.

(In the future, this will be applied to the injective/projective/flat derivability structures.)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Nov 16, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): deriving functors using a right derivability structure [Merged by Bors] - feat(CategoryTheory): deriving functors using a right derivability structure Nov 16, 2025
@mathlib-bors mathlib-bors bot closed this Nov 16, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@erdOne erdOne erdOne left review comments

Assignees

@erdOne erdOne

Labels

ready-to-merge This PR has been sent to bors. t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@joelriou @mathlib4-dependent-issues-bot @riccardobrasca @erdOne