[Merged by Bors] - feat(CategoryTheory/Monoidal): left action of monoidal categories by robin-carlier · Pull Request #25761 · leanprover-community/mathlib4

robin-carlier · 2025-06-12T08:52:44Z

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

This PR continues the work from #25499.

Original PR: #25499

github-actions · 2025-06-12T08:53:52Z

PR summary db52f0992d

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

Declarations diff

+ MonoidalLeftAction
+ MonoidalLeftActionStruct
+ actionAssocIso_inv_naturality
+ actionAssocNatIso
+ actionHomLeft_action
+ actionHomRight_comp
+ actionHomRight_hom_inv
+ actionHomRight_hom_inv'
+ actionHomRight_inv_hom
+ actionHomRight_inv_hom'
+ actionHom_def'
+ actionHom_id
+ actionLeft
+ actionRight
+ actionUnitIso_inv_naturality
+ actionUnitNatIso
+ action_exchange
+ comp_actionHomLeft
+ curriedAction
+ hom_inv_actionHomLeft
+ hom_inv_actionHomLeft'
+ id_actionHom
+ inv_actionHom
+ inv_actionHomLeft
+ inv_actionHomRight
+ inv_hom_actionHomLeft
+ inv_hom_actionHomLeft'
+ isIso_actionHom
+ isIso_actionHomLeft
+ isIso_actionHomRight
+ 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).

Mathlib/CategoryTheory/Monoidal/Action/Basic.lean

Co-authored-by: Joël Riou <37772949+joelriou@users.noreply.github.com>

Mathlib/CategoryTheory/Monoidal/Action/Basic.lean

robin-carlier · 2025-06-16T09:53:40Z

Since apparently we’re changing the notation for the tensor product of morphisms, I’ve changed the notation for actionHom from ⊙ₗ to ⊙ₗₘ.

…oidal_left_actions_1

joelriou · 2025-06-17T08:53:43Z

Thanks!

bors merge

…5761) 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)̀`.

mathlib-bors · 2025-06-17T09:02:27Z

Pull request successfully merged into master.

Build succeeded:

CI Success

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.

…anprover-community#25761) 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)̀`.

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

…anprover-community#25761) 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)̀`.

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

robin-carlier added 6 commits June 5, 2025 21:34

monoidal actions 1

929b40b

docstrings + simpnf

6eb3589

notations + simps!

a9a08ba

Merge branch 'master' into robin-carlier/monoidal_left_actions_1

7ae8cf3

Merge branch 'master' into robin-carlier/monoidal_left_actions_1

a77c6db

Merge branch 'master' into robin-carlier/monoidal_left_actions_1

865b8ba

robin-carlier added the t-category-theory Category theory label Jun 12, 2025

This was referenced Jun 12, 2025

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

Closed

refactor(CategoryTheory/Monoidal/Mod_): refactor Mod_ using MonoidalLeftAction #25545

Closed

robin-carlier mentioned this pull request Jun 12, 2025

[Merged by Bors] - refactor(CategoryTheory/Monoidal/Mod_): refactor Mod_ using MonoidalLeftAction #25762

Closed

1 task

robin-carlier added 6 commits June 13, 2025 08:19

new notations

6cb2a06

new notations in docstrings

5568ab6

more forgotten notation in docstring

6cc1509

add a line break

11e0765

golf + remove duplicate

85ff8ef

minor style

5fdcc27

robin-carlier mentioned this pull request Jun 13, 2025

[Merged by Bors] - feat(CategoryTheory/Monoidal/Action): monoidal right actions #25840

Closed

1 task

robin-carlier added 2 commits June 13, 2025 21:55

IsIso instances

b6a8746

inv lemmas

a6ff2fa

joelriou reviewed Jun 15, 2025

View reviewed changes