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): presheaf is colimit of representables #4401

Closed
wants to merge 19 commits into from
Closed

[Merged by Bors] - feat(category_theory): presheaf is colimit of representables #4401

wants to merge 19 commits into from

Conversation

b-mehta
Copy link
Collaborator

@b-mehta b-mehta commented Oct 4, 2020 •
edited
Loading

Show every presheaf (on a small category) is a colimit of representables, and some related results.
Suggestions for better names more than welcome.

@b-mehta b-mehta added the WIP Work in progress label Oct 4, 2020
@b-mehta b-mehta 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 Oct 4, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 5, 2020
@jcommelin jcommelin 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 Oct 5, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 5, 2020
@b-mehta b-mehta added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Oct 10, 2020
jcommelin
jcommelin reviewed Oct 12, 2020
View reviewed changes
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
@b-mehta @jcommelin
Apply suggestions from code review
fa60eec 
Co-authored-by: Johan Commelin <johan@commelin.net>
@jcommelin
Copy link
Member

@semorrison Would you please take a look at this one? LGTM

@b-mehta
Copy link
Collaborator Author

b-mehta commented Oct 12, 2020

I don't think the names L and R are very meaningful right now, suggestions appreciated!

@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 15, 2020
@b-mehta b-mehta added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 16, 2020
jcommelin
jcommelin reviewed Oct 16, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

I think that some of the names can still be improved a bit.

src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
src/category_theory/limits/presheaf.lean Outdated Show resolved Hide resolved
b-mehta and others added 2 commits October 16, 2020 20:19
@b-mehta @jcommelin
Apply suggestions from code review
62a41a9 
Co-authored-by: Johan Commelin <johan@commelin.net>
@b-mehta
better names
acafa1e
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 20, 2020
@b-mehta
Copy link
Collaborator Author

b-mehta commented Oct 20, 2020

I explicitly defined the functor which the cocone is for, and added a comment saying that everything in the image is representable (I was working on something which uses this and I found it useful to name the functor anyway).

@b-mehta b-mehta added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 20, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 20, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 20, 2020
@jcommelin
Copy link
Member

I've never properly learned Kan extensions. Is this a Kan extension, or is it related to that? If it is a special case, I think we should point that out in a comment.

@b-mehta
Copy link
Collaborator Author

b-mehta commented Oct 20, 2020

Good point, this is exactly the Yoneda extension. I was hesitant to explicitly call it by this name since I haven't yet shown (in this PR at least) the last point in the list of properties there, but it seems like it's still the Kan extension anyway. I'll add comments for this as well as the link.

@b-mehta b-mehta added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Oct 20, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Oct 20, 2020
@b-mehta b-mehta added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Oct 20, 2020
@b-mehta b-mehta mentioned this pull request Oct 22, 2020
Closed
2 tasks
jcommelin
jcommelin approved these changes Oct 23, 2020
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

@semorrison I'm happy with this. LGTM.

@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 Oct 23, 2020
bors bot pushed a commit that referenced this pull request Oct 23, 2020
@b-mehta
feat(category_theory): presheaf is colimit of representables (#4401)
aa59039 
Show every presheaf (on a small category) is a colimit of representables, and some related results. 
Suggestions for better names more than welcome.
@bors
Copy link

bors bot commented Oct 24, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory): presheaf is colimit of representables [Merged by Bors] - feat(category_theory): presheaf is colimit of representables Oct 24, 2020
@bors bors bot closed this Oct 24, 2020
@bors bors bot deleted the colimit-representables branch October 24, 2020 00:18
bors bot pushed a commit that referenced this pull request Oct 28, 2020
@b-mehta
feat(category_theory/limits/presheaf): free cocompletion (#4740)
25df267 
Fill in the missing part of #4401, showing that the yoneda extension is unique. Also adds some basic API around #4401.
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@semorrison semorrison semorrison left review comments

@jcommelin jcommelin jcommelin approved these changes

@rwbarton rwbarton Awaiting requested review from rwbarton

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+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
3 participants
@b-mehta @jcommelin @semorrison