Skip to content

[Merged by Bors] - feat(CategoryTheory/Functor): pointwise right derived functors#26036

Closed
joelriou wants to merge 21 commits intoleanprover-community:masterfrom
joelriou:jriou-pointwise-right-derived-functor
Closed

[Merged by Bors] - feat(CategoryTheory/Functor): pointwise right derived functors#26036
joelriou wants to merge 21 commits intoleanprover-community:masterfrom
joelriou:jriou-pointwise-right-derived-functor

Conversation

@joelriou
Copy link
Copy Markdown
Contributor

@joelriou joelriou commented Jun 17, 2025 •
edited
Loading

This PR introduces pointwise right derived functors as particular cases of pointwise left Kan extensions.

This PR continues the work from #22490.

Original PR: #22490

@joelriou
Copy link
Copy Markdown
Contributor Author

joelriou commented Jun 17, 2025

Comments from Original PR #22490

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

@github-actions (2025-03-03 09:13 UTC):

PR summary d9d3b4ca93

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

Declarations diff

+ HasPointwiseRightDerivedFunctor
+ HasPointwiseRightDerivedFunctorAt
+ LeftExtension.isPointwiseLeftKanExtensionOfIsIso
+ hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor
+ hasPointwiseRightDerivedFunctorAt_iff
+ hasPointwiseRightDerivedFunctorAt_iff_of_mem
+ hasPointwiseRightDerivedFunctor_of_inverts
+ hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor
+ isPointwiseLeftKanExtensionAtOfIso
+ isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor
+ isPointwiseLeftKanExtensionOfIso

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

This was referenced Jun 17, 2025
Closed
Closed
Closed
@github-actions github-actions bot added the t-category-theory Category theory label Jun 17, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 17, 2025 •
edited
Loading

PR summary 6981c4c19c

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

Declarations diff

+ HasPointwiseRightDerivedFunctor
+ HasPointwiseRightDerivedFunctorAt
+ HasPointwiseRightDerivedFunctorAt.hasColimit
+ LeftExtension.isPointwiseLeftKanExtensionOfIsIsoOfIsLocalization
+ hasPointwiseLeftKanExtension_of_hasPointwiseRightDerivedFunctor
+ hasPointwiseRightDerivedFunctorAt_iff
+ hasPointwiseRightDerivedFunctorAt_iff_of_mem
+ hasPointwiseRightDerivedFunctor_of_inverts
+ hasRightDerivedFunctor_of_hasPointwiseRightDerivedFunctor
+ isPointwiseLeftKanExtensionAtOfIsoOfIsLocalization
+ isPointwiseLeftKanExtensionOfHasPointwiseRightDerivedFunctor
+ isPointwiseLeftKanExtensionOfIsoOfIsLocalization

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 mentioned this pull request Jun 24, 2025
Closed
2 tasks
@robin-carlier robin-carlier self-assigned this Jul 20, 2025
robin-carlier
robin-carlier reviewed Jul 31, 2025
View reviewed changes
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
@robin-carlier robin-carlier added the awaiting-author A reviewer has asked the author a question or requested changes. label Jul 31, 2025
@joelriou joelriou removed the awaiting-author A reviewer has asked the author a question or requested changes. label Aug 1, 2025
robin-carlier
robin-carlier reviewed Aug 1, 2025
View reviewed changes
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier left a comment •
edited
Loading

Choose a reason for hiding this comment

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

Thanks! Here are two hidden by […] exact if you want. The have became haveI for proper inlining in the resulting terms, but all this is up to you.

Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
Comment thread Mathlib/CategoryTheory/Functor/Derived/PointwiseRightDerived.lean Outdated
@robin-carlier
Copy link
Copy Markdown
Contributor

robin-carlier commented Aug 1, 2025

It seems I did something wrong...

maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Aug 1, 2025

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

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

riccardobrasca commented Aug 13, 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 Aug 13, 2025
mathlib-bors bot pushed a commit that referenced this pull request Aug 13, 2025
@joelriou
feat(CategoryTheory/Functor): pointwise right derived functors (#26036)
a287803 
This PR introduces pointwise right derived functors as particular cases of pointwise left Kan extensions.



Co-authored-by: Joël Riou <[email protected]>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Aug 13, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Functor): pointwise right derived functors [Merged by Bors] - feat(CategoryTheory/Functor): pointwise right derived functors Aug 13, 2025
@mathlib-bors mathlib-bors bot closed this Aug 13, 2025
Paul-Lez pushed a commit to Paul-Lez/mathlib4 that referenced this pull request Aug 23, 2025
@joelriou @Paul-Lez
feat(CategoryTheory/Functor): pointwise right derived functors (leanp…
cc7a9ab 
…rover-community#26036)

This PR introduces pointwise right derived functors as particular cases of pointwise left Kan extensions.



Co-authored-by: Joël Riou <[email protected]>
pechersky pushed a commit to pechersky/mathlib4 that referenced this pull request Aug 25, 2025
@joelriou @pechersky
feat(CategoryTheory/Functor): pointwise right derived functors (leanp…
b2c3c35 
…rover-community#26036)

This PR introduces pointwise right derived functors as particular cases of pointwise left Kan extensions.



Co-authored-by: Joël Riou <[email protected]>
@joelriou joelriou mentioned this pull request Nov 8, 2025
Closed
3 tasks
@joelriou joelriou mentioned this pull request Dec 17, 2025
Closed
mathlib-bors bot pushed a commit that referenced this pull request Dec 19, 2025
@joelriou
feat(CategoryTheory): pointwise left derived functors (#33006)
d0055cf 
The notion of pointwise left derived functor is introduced in this PR. The content of the new file was obtained by dualizing the corresponding file for pointwise right derived functors (introduced in #26036).
YuvalFilmus pushed a commit to YuvalFilmus/mathlib4 that referenced this pull request Dec 19, 2025
@joelriou @YuvalFilmus
feat(CategoryTheory): pointwise left derived functors (leanprover-com…
924c9a1 
…munity#33006)

The notion of pointwise left derived functor is introduced in this PR. The content of the new file was obtained by dualizing the corresponding file for pointwise right derived functors (introduced in leanprover-community#26036).
goliath-klein pushed a commit to PrParadoxy/mathlib4 that referenced this pull request Jan 24, 2026
@joelriou @goliath-klein
feat(CategoryTheory): pointwise left derived functors (leanprover-com…
c3f672a 
…munity#33006)

The notion of pointwise left derived functor is introduced in this PR. The content of the new file was obtained by dualizing the corresponding file for pointwise right derived functors (introduced in leanprover-community#26036).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@robin-carlier robin-carlier robin-carlier left review comments

Assignees

@robin-carlier robin-carlier

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.

3 participants

@joelriou @robin-carlier @riccardobrasca