Skip to content

[Merged by Bors] - feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites#25860

Closed
robin-carlier wants to merge 49 commits intoleanprover-community:masterfrom
robin-carlier:monoidal-actions-mop
Closed

[Merged by Bors] - feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites#25860
robin-carlier wants to merge 49 commits intoleanprover-community:masterfrom
robin-carlier:monoidal-actions-mop

Conversation

@robin-carlier
Copy link
Copy Markdown
Contributor

@robin-carlier robin-carlier commented Jun 14, 2025 •
edited
Loading

Given a monoidal category C and a category D, we prove that a left (resp. right) Cᴹᵒᵖ-action on D gives a right (resp. left) C-action on D. Conversely, we show that left/right C-actions gives right/left Cᴹᵒᵖ-actions.

Open in Gitpod

@robin-carlier
monoidal actions 1
929b40b
@robin-carlier
docstrings + simpnf
6eb3589
@robin-carlier
notations + simps!
a9a08ba
@robin-carlier
Merge branch 'master' into robin-carlier/monoidal_left_actions_1
7ae8cf3
@robin-carlier
Merge branch 'master' into robin-carlier/monoidal_left_actions_1
a77c6db
@robin-carlier
Merge branch 'master' into robin-carlier/monoidal_left_actions_1
865b8ba
@robin-carlier
new notations
6cb2a06
@robin-carlier
new notations in docstrings
5568ab6
@robin-carlier
more forgotten notation in docstring
6cc1509
@robin-carlier
add a line break
11e0765
@robin-carlier
golf + remove duplicate
85ff8ef
@robin-carlier
minor style
5fdcc27
@robin-carlier
right actions
d6644ee
@robin-carlier
IsIso instances
b6a8746
@robin-carlier
right actions
da805b7
@robin-carlier
inv lemmas
a6ff2fa
@robin-carlier
isos
231687d
@robin-carlier
name
4a8ed24
@robin-carlier
wip
4af2213
@robin-carlier
Merge branch 'robin-carlier/monoidal_left_actions_1' into monoidal-ri…
723c0a7 
…ght-actions
@robin-carlier
Merge branch 'monoidal-right-actions' into monoidal-actions-mop
8add8fd
@robin-carlier
mopposites
6295f3f
@robin-carlier
update docstring
c81ac3a
@robin-carlier
docstrings + some extra lemma.
d897684
@github-actions github-actions bot added the t-category-theory Category theory label Jun 14, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented Jun 14, 2025 •
edited
Loading

PR summary 84910edb50

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.CategoryTheory.Monoidal.Action.Opposites (new file) 434

Declarations diff

+ leftActionOfMonoidalOppositeRightAction
+ monoidalOppositeLeftAction
+ monoidalOppositeLeftAction_actionAssocIso_mop_mop
+ monoidalOppositeLeftAction_actionHomLeft_mop
+ monoidalOppositeLeftAction_actionHom_mop_mop
+ monoidalOppositeLeftAction_actionObj_mop
+ monoidalOppositeLeftAction_actionRight_mop
+ monoidalOppositeRightAction
+ monoidalOppositeRightAction_actionAssocIso_mop_mop
+ monoidalOppositeRightAction_actionHomRight_mop
+ monoidalOppositeRightAction_actionHom_mop_mop
+ monoidalOppositeRightAction_actionObj_mop
+ monoidalOppositeRightAction_actionRight_mop
+ rightActionOfMonoidalOppositeLeftAction

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@robin-carlier robin-carlier mentioned this pull request Jun 14, 2025
Closed
1 task
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 14, 2025
@robin-carlier robin-carlier mentioned this pull request Jun 17, 2025
Open
@mathlib4-dependent-issues-bot mathlib4-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jun 22, 2025
@mathlib4-dependent-issues-bot
Copy link
Copy Markdown
Collaborator

mathlib4-dependent-issues-bot commented Jun 22, 2025

This PR/issue depends on:

@robin-carlier robin-carlier added the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 23, 2025
@github-actions github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label Jun 23, 2025
@leanprover-community-bot-assistant
Copy link
Copy Markdown
Collaborator

leanprover-community-bot-assistant commented Jul 5, 2025

This pull request has conflicts, please merge master and resolve them.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025
@github-actions github-actions bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jul 5, 2025
@joelriou
Copy link
Copy Markdown
Contributor

joelriou commented Jul 5, 2025

Thanks!

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Jul 5, 2025
mathlib-bors bot pushed a commit that referenced this pull request Jul 5, 2025
@robin-carlier
feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites (#…
aff540e 
…25860)

Given a monoidal category `C` and a category `D`, we prove that a left (resp. right) `Cᴹᵒᵖ`-action on `D` gives a right (resp. left) `C`-action on `D`. Conversely, we show that left/right `C`-actions gives right/left `Cᴹᵒᵖ`-actions.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Jul 5, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites [Merged by Bors] - feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites Jul 5, 2025
@mathlib-bors mathlib-bors bot closed this Jul 5, 2025
joelriou pushed a commit to joelriou/mathlib4 that referenced this pull request Jul 7, 2025
@robin-carlier @joelriou
feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites (l…
25fad4e 
…eanprover-community#25860)

Given a monoidal category `C` and a category `D`, we prove that a left (resp. right) `Cᴹᵒᵖ`-action on `D` gives a right (resp. left) `C`-action on `D`. Conversely, we show that left/right `C`-actions gives right/left `Cᴹᵒᵖ`-actions.
callesonne pushed a commit to callesonne/mathlib4 that referenced this pull request Jul 24, 2025
@robin-carlier @callesonne
feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites (l…
5b01beb 
…eanprover-community#25860)

Given a monoidal category `C` and a category `D`, we prove that a left (resp. right) `Cᴹᵒᵖ`-action on `D` gives a right (resp. left) `C`-action on `D`. Conversely, we show that left/right `C`-actions gives right/left `Cᴹᵒᵖ`-actions.
hrmacbeth pushed a commit to szqzs/mathlib4 that referenced this pull request Jul 28, 2025
@robin-carlier @hrmacbeth
feat(CategoryTheory/Monoidal/Action): Action of monoidal opposites (l…
c3e399e 
…eanprover-community#25860)

Given a monoidal category `C` and a category `D`, we prove that a left (resp. right) `Cᴹᵒᵖ`-action on `D` gives a right (resp. left) `C`-action on `D`. Conversely, we show that left/right `C`-actions gives right/left `Cᴹᵒᵖ`-actions.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

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.

4 participants

@robin-carlier @mathlib4-dependent-issues-bot @leanprover-community-bot-assistant @joelriou