Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(category_theory/adjunction): the Special Adjoint Functor Theorem #15987

Closed
wants to merge 15 commits into from
Closed

[Merged by Bors] - feat(category_theory/adjunction): the Special Adjoint Functor Theorem #15987

wants to merge 15 commits into from

Conversation

TwoFX
Copy link
Member

@TwoFX TwoFX commented Aug 10, 2022 •
edited by github-actions bot
Loading

@TwoFX TwoFX added the t-category-theory Category theory label Aug 10, 2022
@TwoFX TwoFX changed the title feature(category_theory/adjunction): the Special Adjoint Functor Theorem feat(category_theory/adjunction): the Special Adjoint Functor Theorem Aug 10, 2022
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 10, 2022
@TwoFX TwoFX mentioned this pull request Aug 10, 2022
Closed
5 tasks
@b-mehta
Copy link
Collaborator

b-mehta commented Aug 11, 2022

I just saw the branch name, nice! :D

@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 27, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

@TwoFX TwoFX added the awaiting-review The author would like community review of the PR label Aug 27, 2022
@jcommelin
Copy link
Member

Thanks 🎉

bors merge

@github-actions github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 30, 2022
bors bot pushed a commit that referenced this pull request Aug 30, 2022
@TwoFX
feat(category_theory/adjunction): the Special Adjoint Functor Theorem (…
c82fab8 
…#15987)
@bors
Copy link

bors bot commented Aug 30, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/adjunction): the Special Adjoint Functor Theorem [Merged by Bors] - feat(category_theory/adjunction): the Special Adjoint Functor Theorem Aug 30, 2022
@bors bors bot closed this Aug 30, 2022
@bors bors bot deleted the 🧃 branch August 30, 2022 09:26
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-category-theory Category theory
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@TwoFX @b-mehta @mathlib-dependent-issues-bot @jcommelin