Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Merged by Bors] - feat(CategoryTheory): transport Kan extensions via equivalences #12785

Closed
wants to merge 6 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented May 9, 2024

In this PR, it is shown that left/right Kan extensions of functors F : C ⥤ H along a functor L : C ⥤ D are compatible with changing the functors F and L by isomorphic functors, by the precomposition with an equivalence G : C' ⥤ C, and postcomposition with an equivalence D ⥤ D'.


Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label May 9, 2024
@erdOne
Copy link
Member

erdOne commented May 18, 2024

LGTM, but maybe @dagurtomas can give it a look as well?

@dagurtomas
Copy link
Collaborator

Thanks for the ping. I'll take a look but I don't have time until tomorrow evening

Copy link
Collaborator

@dagurtomas dagurtomas left a comment

Choose a reason for hiding this comment

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

I just suggested a minor generalisation, otherwise LGTM.

@dagurtomas dagurtomas added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels May 19, 2024
@joelriou joelriou added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 20, 2024
@erdOne
Copy link
Member

erdOne commented May 24, 2024

Thanks! (and thanks Dagur!)
maintainer merge

Copy link

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

@riccardobrasca
Copy link
Member

This is great, thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels May 24, 2024
mathlib-bors bot pushed a commit that referenced this pull request May 24, 2024
In this PR, it is shown that left/right Kan extensions of functors `F : C ⥤ H` along a functor `L : C ⥤ D` are compatible with changing the functors `F` and `L` by isomorphic functors, by the precomposition with an equivalence `G : C' ⥤ C`, and postcomposition with an equivalence `D ⥤ D'`.
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented May 24, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory): transport Kan extensions via equivalences [Merged by Bors] - feat(CategoryTheory): transport Kan extensions via equivalences May 24, 2024
@mathlib-bors mathlib-bors bot closed this May 24, 2024
@mathlib-bors mathlib-bors bot deleted the functor-kan-extension-equivalences branch May 24, 2024 09:47
grunweg pushed a commit that referenced this pull request May 24, 2024
In this PR, it is shown that left/right Kan extensions of functors `F : C ⥤ H` along a functor `L : C ⥤ D` are compatible with changing the functors `F` and `L` by isomorphic functors, by the precomposition with an equivalence `G : C' ⥤ C`, and postcomposition with an equivalence `D ⥤ D'`.
callesonne pushed a commit that referenced this pull request Jun 4, 2024
In this PR, it is shown that left/right Kan extensions of functors `F : C ⥤ H` along a functor `L : C ⥤ D` are compatible with changing the functors `F` and `L` by isomorphic functors, by the precomposition with an equivalence `G : C' ⥤ C`, and postcomposition with an equivalence `D ⥤ D'`.
js2357 pushed a commit that referenced this pull request Jun 18, 2024
In this PR, it is shown that left/right Kan extensions of functors `F : C ⥤ H` along a functor `L : C ⥤ D` are compatible with changing the functors `F` and `L` by isomorphic functors, by the precomposition with an equivalence `G : C' ⥤ C`, and postcomposition with an equivalence `D ⥤ D'`.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
maintainer-merge ready-to-merge This PR has been sent to bors. t-category-theory Category theory
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants