Skip to content

[Merged by Bors] - feat: add unitor functor for product of categories#13663

Closed
onriv wants to merge 11 commits intomasterfrom
onriv/category_product_unitor
Closed

[Merged by Bors] - feat: add unitor functor for product of categories#13663
onriv wants to merge 11 commits intomasterfrom
onriv/category_product_unitor

Conversation

@onriv
Copy link
Copy Markdown
Contributor

@onriv onriv commented Jun 9, 2024

left and right unitor functors for product of categories

Open in Gitpod

The implementation is copying from the same file for the associator. I am not sure if the category "1" , i.e., Discrete Punit should take universe parameter or not, and if it should have some notation like U+1D7CF 𝟏 or something else.

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Jun 9, 2024
@github-actions
Copy link
Copy Markdown

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

PR summary 9f3684242a

Import changes

No significant changes to the import graph

Declarations diff

+ leftInverseUnitor
+ leftUnitor
+ leftUnitorEquivalence
+ leftUnitor_isEquivalence
+ rightInverseUnitor
+ rightUnitor
+ rightUnitorEquivalence
+ rightUnitor_isEquivalence

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>

@erdOne
Copy link
Copy Markdown
Member

erdOne commented Jun 9, 2024

Thanks for the contribution! If you think this PR is ready for review please add the "awaiting-review" label. While you're at it, adding the "t-category-theory" tag also helps the discoverability of the PR. Also see this page for more info.

@onriv
Copy link
Copy Markdown
Contributor Author

onriv commented Jun 9, 2024

@erdOne Thank you for the reply! Yeah I added the two tags and reading the doc now.

joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
joelriou
joelriou reviewed Jun 9, 2024
View reviewed changes
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 9, 2024

As the file is named Associator.lean, could you move the new code to a new file Unitor.lean.

@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 9, 2024
@onriv
Copy link
Copy Markdown
Contributor Author

onriv commented Jun 10, 2024

@joelriou Thank you for the suggestion! New code moved to a new file Unitor.lean.

@onriv onriv added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 10, 2024
joelriou
joelriou reviewed Jun 10, 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 10, 2024
@onriv onriv added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 10, 2024
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 10, 2024

You may have to update the root file Mathlib.lean so that all files (including the new one) are imported.

@joelriou joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 10, 2024
@onriv
Copy link
Copy Markdown
Contributor Author

onriv commented Jun 10, 2024

@joelriou Thanks for the reminding! Mathlib.lean updated too. It's kind of weird that the ci pipline failed now though

@onriv onriv force-pushed the onriv/category_product_unitor branch from 1dffc8e to e0140c0 Compare June 15, 2024 11:54
joelriou
joelriou reviewed Jun 17, 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 17, 2024
@onriv onriv force-pushed the onriv/category_product_unitor branch from e0140c0 to 5d00bfe Compare June 18, 2024 14:38
@onriv onriv added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 19, 2024
joelriou
joelriou reviewed Jun 20, 2024
View reviewed changes
Mathlib/CategoryTheory/Products/Unitor.lean Outdated

/-- The left unitor functor `1 × C ⥤ C` -/
@[simps]
def leftUnitor : Discrete (PUnit: Type w) × C ⥤ C where
Copy link
Copy Markdown
Contributor

@joelriou joelriou Jun 20, 2024

Choose a reason for hiding this comment

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

And similarly below:

Suggested change
def leftUnitor : Discrete (PUnit: Type w) × C ⥤ C where
def leftUnitor : Discrete (PUnit : Type w) × C ⥤ C where

Copy link
Copy Markdown
Contributor Author

@onriv onriv Jun 23, 2024

Choose a reason for hiding this comment

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

Thanks! Codestyle change with space before column now

@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jun 23, 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 23, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jun 23, 2024
@onriv
feat: add unitor functor for product of categories (#13663)
1616f72 
left and right unitor functors for product of categories



Co-authored-by: Shanghe Chen <shanghechen@outlook.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jun 23, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: add unitor functor for product of categories [Merged by Bors] - feat: add unitor functor for product of categories Jun 23, 2024
@mathlib-bors mathlib-bors bot closed this Jun 23, 2024
@mathlib-bors mathlib-bors bot deleted the onriv/category_product_unitor branch June 23, 2024 16:49
kbuzzard pushed a commit that referenced this pull request Jun 26, 2024
@onriv @kbuzzard
feat: add unitor functor for product of categories (#13663)
72a943b 
left and right unitor functors for product of categories



Co-authored-by: Shanghe Chen <shanghechen@outlook.com>
dagurtomas pushed a commit that referenced this pull request Jul 2, 2024
@onriv @dagurtomas
feat: add unitor functor for product of categories (#13663)
cee5df1 
left and right unitor functors for product of categories



Co-authored-by: Shanghe Chen <shanghechen@outlook.com>
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

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! 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.

3 participants

@onriv @erdOne @joelriou