Skip to content

feat(CategoryTheory/Monoidal): left action of monoidal categories#25499

Closed
robin-carlier wants to merge 5 commits intomasterfrom
robin-carlier/monoidal_left_actions_1
Closed

feat(CategoryTheory/Monoidal): left action of monoidal categories#25499
robin-carlier wants to merge 5 commits intomasterfrom
robin-carlier/monoidal_left_actions_1

Conversation

@robin-carlier
Copy link
Copy Markdown
Contributor

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

Define (left) actions of a monoidal category on a category: a MonoidalLeftAction of a monoidal category C on a category D consists of an action bifunctor - ⊙ - : C ⥤ D ⥤ D, equipped with structural natural isomorphisms (- ⊗ -) ⊙ - ≅ - ⊙ - ⊙ - and 𝟙_ C ⊙ - ≅ -, subject to coherence conditions.

The code in this PR is parallel to the existing code for monoidal category.

We provide a battery of basic simp lemmas to ease working with this type class, and show that every monoidal category acts on itself via its tensor product.

The code is put in a new subdirectory CategoryTheory/Monoidal/Action.

Future wok on the subject includes

  • Providing a constructor for MonoidalLeftAction taking a monoidal functor from C to D ⥤ D, where the latter has the "composition" monoidal structure.
  • Constructing the action of C ⥤ C on C.
  • Extending the notion of module objects internal to a monoidal category to allow the Mon_ object to be in C, and the module to be in D where D has a monoidal left action of C.
  • Using the two previous points, show that given a monad M, there is an equivalence of categories between Algebra M and modules in C over the monoid M.toMon : Mon_ (C ⥤ C)̀.

Open in Gitpod

@robin-carlier robin-carlier added awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory labels Jun 5, 2025
@github-actions
Copy link
Copy Markdown

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

PR summary a77c6db5a6

Import changes for modified files

No significant changes to the import graph

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

Declarations diff

+ MonoidalLeftAction
+ MonoidalLeftActionStruct
+ actionAssocNatIso
+ actionHomLeft_action
+ actionHomRight_comp
+ actionHomRight_hom_inv
+ actionHomRight_hom_inv'
+ actionHomRight_inv_hom
+ actionHomRight_inv_hom'
+ actionHom_def'
+ actionHom_id
+ actionLeft
+ actionRight
+ actionUnitNatIso
+ action_assoc
+ action_exchange
+ comp_actionHomLeft
+ curriedAction
+ hom_inv_actionHomLeft
+ hom_inv_actionHomLeft'
+ id_actionHom
+ inv_hom_actionHomLeft
+ inv_hom_actionHomLeft'
+ selfAction
+ tensor_actionHomRight
+ unit_actionHomRight

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).

@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 5, 2025
@github-actions github-actions bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jun 6, 2025
@robin-carlier robin-carlier mentioned this pull request Jun 6, 2025
Closed
1 task
@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 Jun 6, 2025
@robin-carlier robin-carlier mentioned this pull request Jun 12, 2025
Closed
@robin-carlier
Copy link
Copy Markdown
Contributor Author

robin-carlier commented Jun 12, 2025

This PR has been migrated to a fork-based workflow: #25761

@YaelDillies YaelDillies deleted the robin-carlier/monoidal_left_actions_1 branch August 15, 2025 16:44
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

t-category-theory Category theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@robin-carlier