Skip to content

[Merged by Bors] - chore(CategoryTheory/Adjunction): dualize some of the API for reflective functors#13948

Closed
dagurtomas wants to merge 8 commits intomasterfrom
dagur/Coreflective
Closed

[Merged by Bors] - chore(CategoryTheory/Adjunction): dualize some of the API for reflective functors#13948
dagurtomas wants to merge 8 commits intomasterfrom
dagur/Coreflective

Conversation

@dagurtomas
Copy link
Copy Markdown
Contributor

@dagurtomas dagurtomas commented Jun 19, 2024

Open in Gitpod

@github-actions
Copy link
Copy Markdown

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

PR summary 604ab5be88

Import changes

No significant changes to the import graph

Declarations diff

+ Coreflective
+ Coreflective.comp
+ Functor.essImage.counit_isIso
+ Functor.fullyFaithfulOfCoreflective
+ _root_.CategoryTheory.mem_essImage_of_unit_isIso
+ coreflector
+ coreflectorAdjunction
+ counit_obj_eq_map_counit
+ instance [Coreflective j] : (coreflector j).IsRightAdjoint := ⟨_, ⟨coreflectorAdjunction j⟩⟩
+ instance [Coreflective j] : j.IsLeftAdjoint := ⟨_, ⟨coreflectorAdjunction j⟩⟩
+ mem_essImage_of_counit_isIso
+ mem_essImage_of_counit_isSplitEpi

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>

@dagurtomas dagurtomas mentioned this pull request Jun 19, 2024
Closed
2 tasks
joelriou
joelriou reviewed Jun 19, 2024
View reviewed changes
@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 19, 2024
dagurtomas
dagurtomas commented Jun 19, 2024
View reviewed changes
@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 19, 2024
dagurtomas
dagurtomas commented Jun 19, 2024
View reviewed changes
dagurtomas
dagurtomas commented Jun 19, 2024
View reviewed changes
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 19, 2024
@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 19, 2024
dagurtomas
dagurtomas commented Jun 19, 2024
View reviewed changes
@dagurtomas dagurtomas added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 19, 2024
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 19, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 19, 2024

Thanks!

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jun 19, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 19, 2024
@dagurtomas
chore(CategoryTheory/Adjunction): dualize some of the API for reflect…
feba708 
…ive functors (#13948)
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 19, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore(CategoryTheory/Adjunction): dualize some of the API for reflective functors [Merged by Bors] - chore(CategoryTheory/Adjunction): dualize some of the API for reflective functors Jun 19, 2024
@mathlib-bors mathlib-bors bot closed this Jun 19, 2024
@mathlib-bors mathlib-bors bot deleted the dagur/Coreflective branch June 19, 2024 18:36
AntoineChambert-Loir pushed a commit that referenced this pull request Jun 20, 2024
@dagurtomas @AntoineChambert-Loir
chore(CategoryTheory/Adjunction): dualize some of the API for reflect…
196f9d4 
…ive functors (#13948)
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@dagurtomas @kbuzzard
chore(CategoryTheory/Adjunction): dualize some of the API for reflect…
12eca28 
…ive functors (#13948)
dagurtomas added a commit that referenced this pull request Jul 2, 2024
@dagurtomas
chore(CategoryTheory/Adjunction): dualize some of the API for reflect…
5ddc601 
…ive functors (#13948)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@joelriou joelriou joelriou left review comments

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.

2 participants

@dagurtomas @joelriou