MulAction vs Action

Stream: mathlib4

[Yiming Xu]

I am recently trying to formalize something about group action, namely I want to prove the category of right actions is cartesian closed, by constructing it an exponential.

I found two descriptions of group actions, one is the MulAction stuff as in mathlib. One is Action as described here:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/RepresentationTheory/Action/Limits.html#Action.instHasFiniteProducts
seems to be developed particularly for representation theory.

Another one is more "traditional" one, called MulAction, in here:
https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Group/Action/Defs.html#MulAction

It seems to me that everything category-related are only developed for Action, but not for MulAction. So are they disconnected? Do I have to make a choice when working with group actions? Or, are they "identified" in some sense by some theorems or some systematic method to transfer from one to the other?

I will work with right actions, but the default is for left action. To use MulAction, I should consider MulOpposite M. What should I do if I use Action?

[Yury G. Kudryashov]

See docs#Action.ofMulAction

[Yiming Xu]

I see. Thanks a lot!

[Yiming Xu]

It seems that there is no lemma on transferring the opposite action stuff in some sense.

[Yury G. Kudryashov]

There is Action.instMulAction