[Merged by Bors] - feat(CategoryTheory/Monoidal/Action): monoidal right actions#25840
Closed
robin-carlier wants to merge 37 commits intoleanprover-community:masterfrom
Closed
[Merged by Bors] - feat(CategoryTheory/Monoidal/Action): monoidal right actions#25840robin-carlier wants to merge 37 commits intoleanprover-community:masterfrom
robin-carlier wants to merge 37 commits intoleanprover-community:masterfrom
Conversation
PR summary ffbf9db0c1Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
d6644ee to
da805b7
Compare
Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>
1 task
Collaborator
|
This PR/issue depends on: |
Contributor
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 22, 2025
We introduce the notion of a right action of a monoidal category `C` on a category `D`. This notion is formally conjugate to that of a left action introduced in #25761, and so are every results in this PR. Please refer to #25761 for a more detailed overview of the notion. The notion comes with its set of notations. We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.
Contributor
|
Build failed: |
Contributor
|
bors cancel You may have to merge again with master, because there are errors due to a new whitespace linter. |
Contributor
Author
|
I’ve fixed the whitespaces and merged master just in case. |
Contributor
|
Thanks! bors merge |
mathlib-bors bot
pushed a commit
that referenced
this pull request
Jun 22, 2025
We introduce the notion of a right action of a monoidal category `C` on a category `D`. This notion is formally conjugate to that of a left action introduced in #25761, and so are every results in this PR. Please refer to #25761 for a more detailed overview of the notion. The notion comes with its set of notations. We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.
Contributor
|
Pull request successfully merged into master. Build succeeded: |
Rida-Hamadani
pushed a commit
to Rida-Hamadani/mathlib4
that referenced
this pull request
Jun 24, 2025
…ver-community#25840) We introduce the notion of a right action of a monoidal category `C` on a category `D`. This notion is formally conjugate to that of a left action introduced in leanprover-community#25761, and so are every results in this PR. Please refer to leanprover-community#25761 for a more detailed overview of the notion. The notion comes with its set of notations. We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.
joelriou
pushed a commit
to joelriou/mathlib4
that referenced
this pull request
Jul 7, 2025
…ver-community#25840) We introduce the notion of a right action of a monoidal category `C` on a category `D`. This notion is formally conjugate to that of a left action introduced in leanprover-community#25761, and so are every results in this PR. Please refer to leanprover-community#25761 for a more detailed overview of the notion. The notion comes with its set of notations. We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.
callesonne
pushed a commit
to callesonne/mathlib4
that referenced
this pull request
Jul 24, 2025
…ver-community#25840) We introduce the notion of a right action of a monoidal category `C` on a category `D`. This notion is formally conjugate to that of a left action introduced in leanprover-community#25761, and so are every results in this PR. Please refer to leanprover-community#25761 for a more detailed overview of the notion. The notion comes with its set of notations. We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
We introduce the notion of a right action of a monoidal category
Con a categoryD. This notion is formally conjugate to that of a left action introduced in #25761, and so are every results in this PR. Please refer to #25761 for a more detailed overview of the notion. The notion comes with its set of notations.We show basic simp lemmas for these objects, and we show that any monoidal category acts on the right on itself.