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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: dualising results in CategoryTheory.Functor.KanExtension.Adjunction #14261

Closed
wants to merge 16 commits into from
Closed

[Merged by Bors] - feat: dualising results in CategoryTheory.Functor.KanExtension.Adjunction #14261

wants to merge 16 commits into from

Conversation

joelriou
Copy link
Collaborator

@joelriou joelriou commented Jun 29, 2024 •
edited by dagurtomas
Loading

In this PR, we make a left/right synchronization of the API in the file CategoryTheory.Functor.KanExtension.Adjunction: missing definitions/lemmas for right Kan extensions are introduced.

Open in Gitpod

@joelriou joelriou added the t-category-theory Category theory label Jun 29, 2024
@github-actions GitHub Actions
Copy link

github-actions bot commented Jun 29, 2024 •
edited
Loading

PR summary 73213fe077

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+ instance (F : C ⥤ H) (X : C) [HasPointwiseLeftKanExtension L F]
+ instance (F : C ⥤ H) (X : C) [HasPointwiseRightKanExtension L F]
+ instance (F : C ⥤ H) : (L.ran.obj F).IsRightKanExtension (L.ranCounit.app F) := by
+ isIso_ranAdjunction_unit_app_iff
+ isPointwiseRightKanExtensionRanCounit
+ ran
+ ranAdjunction
+ ranAdjunction_counit
+ ranAdjunction_unit_app
+ ranCounit
+ ranCounit_app_app_ranAdjunction_unit_app_app
+ ranCounit_app_whiskerLeft_ranAdjunction_unit_app
+ reflective
+ reflective'
++ instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F]
++ instance (F : C ⥤ H) [HasPointwiseRightKanExtension L F]
- instance (F : C ⥤ H) (X : C) [HasPointwiseLeftKanExtension L F] :
-- instance (F : C ⥤ H) [HasPointwiseLeftKanExtension L F] :

You can run this locally as follows 
## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jun 29, 2024
@joelriou joelriou mentioned this pull request Jun 30, 2024
Closed
3 tasks
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 1, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-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 Jul 1, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 4, 2024
joelriou added 2 commits July 4, 2024 15:09
@joelriou
Merge remote-tracking branch 'origin' into functor-kan-extension-poin…
c1d3662 
…twise-sync-left-right
@joelriou
Merge remote-tracking branch 'origin/functor-kan-extension-pointwise-…
a7e7bd5 
…sync-left-right' into functor-kan-extension-adjunction-sync-left-right
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) labels Jul 4, 2024
@leanprover-community-mathlib4-bot
Copy link
Collaborator

This PR/issue depends on:

@dagurtomas dagurtomas added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Jul 5, 2024
@joelriou
Copy link
Collaborator Author

joelriou commented Jul 5, 2024

Thanks very much @dagurtomas for your review!

@joelriou joelriou added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jul 5, 2024
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jul 5, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2024
@joelriou
feat: dualising results in CategoryTheory.Functor.KanExtension.Adjunc…
fca0dc4 
…tion (#14261)

In this PR, we make a left/right synchronization of the API in the file `CategoryTheory.Functor.KanExtension.Adjunction`: missing definitions/lemmas for right Kan extensions are introduced.



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

mathlib-bors bot commented Jul 5, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: dualising results in CategoryTheory.Functor.KanExtension.Adjunction [Merged by Bors] - feat: dualising results in CategoryTheory.Functor.KanExtension.Adjunction Jul 5, 2024
@mathlib-bors mathlib-bors bot closed this Jul 5, 2024
@mathlib-bors mathlib-bors bot deleted the functor-kan-extension-adjunction-sync-left-right branch July 5, 2024 14:05
@adomani adomani mentioned this pull request Aug 1, 2024
Open
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@dagurtomas dagurtomas dagurtomas approved these changes

Assignees
No one assigned
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 @leanprover-community-mathlib4-bot @jcommelin @dagurtomas