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(category_theory/Mon): Mon_ C has limits when C does #4133

Closed
wants to merge 24 commits into from
Closed

[Merged by Bors] - feat(category_theory/Mon): Mon_ C has limits when C does #4133

wants to merge 24 commits into from

Conversation

semorrison
Copy link
Collaborator

@semorrison semorrison commented Sep 13, 2020 •
edited

If C has limits, so does Mon_ C.

(This could potentially replace many individual constructions for concrete categories,
in particular Mon, SemiRing, Ring, and Algebra R.)

Blocked by #4112, #4132.

@semorrison
feat(category_theory): monoidal natural transformations and discrete …
716f66b 
…monoidal categories
@semorrison
oops
b8afccc
@semorrison
.
e319153
@semorrison
oops
00dfd08
@semorrison
fix
f20306a
@semorrison
Update src/category_theory/discrete_category.lean
67b9be5
@semorrison
using eq_of_hom
7e34290
@semorrison
lint
293f12e
@semorrison
Merge remote-tracking branch 'origin/master' into monoidal_nat_trans
5cd1ab6
@semorrison
err... change the definition so it is correct
11b8025
@semorrison
add something that relies on the correct definition
c861bdd
@semorrison
Merge remote-tracking branch 'origin/master' into monoidal_nat_trans
6b42962
@semorrison
feat(category_theory): lim : (J ⥤ C) ⥤ C is lax monoidal when C is a …
97ecb8b 
…monoidal category
@semorrison
lint
56dedb2
@semorrison
lint
cabf8f1
@semorrison
lint
b52a372
@semorrison
Merge branch 'monoidal_nat_trans' into Mon_limits
2609d2a
@semorrison
feat(category_theory/Mon): Mon_ C has limits when C does
7bb7843
@semorrison
fix
82738a0
@semorrison semorrison 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 Sep 13, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 14, 2020
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Sep 14, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 14, 2020
@semorrison semorrison changed the title feat(category_theory/Mon): Mon_ C has limits when C does (deps: #4112, #4132) feat(category_theory/Mon): Mon_ C has limits when C does (deps: #4132) Sep 16, 2020
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 18, 2020
@github-actions github-actions bot added merge-conflict Please `git merge origin/master` then a bot will remove this label. and removed merge-conflict Please `git merge origin/master` then a bot will remove this label. labels Sep 19, 2020
@semorrison semorrison added awaiting-review The author would like community review of the PR and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. labels Sep 19, 2020
@semorrison semorrison changed the title feat(category_theory/Mon): Mon_ C has limits when C does (deps: #4132) feat(category_theory/Mon): Mon_ C has limits when C does Sep 19, 2020
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Sep 19, 2020
jcommelin
jcommelin approved these changes Sep 19, 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.

Thanks 🎉

bors merge

@github-actions github-actions bot added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label Sep 19, 2020
bors bot pushed a commit that referenced this pull request Sep 19, 2020
@semorrison
feat(category_theory/Mon): Mon_ C has limits when C does (#4133)
02b492a 
If `C` has limits, so does `Mon_ C`.

(This could potentially replace many individual constructions for concrete categories,
in particular `Mon`, `SemiRing`, `Ring`, and `Algebra R`.)



Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Sep 19, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(category_theory/Mon): Mon_ C has limits when C does [Merged by Bors] - feat(category_theory/Mon): Mon_ C has limits when C does Sep 19, 2020
@bors bors bot closed this Sep 19, 2020
@bors bors bot deleted the Mon_limits branch September 19, 2020 19:45
@YaelDillies YaelDillies removed the awaiting-review The author would like community review of the PR label Nov 15, 2021
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@jcommelin jcommelin jcommelin approved these changes

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.

None yet
3 participants
@semorrison @jcommelin @YaelDillies