endofunctorMonoidalCategory is "wrong"

Stream: mathlib4

[Robin Carlier]

In #25499, I introduced monoidal left actions of a monoidal category on a category. I followed the reference here. The data of a monoidal left action of C on D consists on a bifunctor - ⊙ - : C ⥤ D ⥤ D, along with a natural isomorphism (x ⊗ y) ⊙ z ≅ x ⊙ y ⊙ z, and natural isomorphism 𝟙_ C ⊙ x ≅ x, these isomorphism satisfy compatibility conditions that are like the pentagon and triangle axioms for monoidal categories. A monoidal category C acts on itself via the tensor product, etc. So far, everything seems pretty moral.

There is a second point of view on such objects (which is in fact the definition in the reference I gave): they are monoidal functors C ⥤ D ⥤ D, where D ⥤ D has the "composition" monoidal structure. Also, for every (not necessarily monoidal) category C there is a left action of C ⥤ C (again with composition monoidal structure) on C, corresponding to the identity monoidal functor from C ⥤ C to itself, the "action" being evaluation.

This must be very straightforward to prove, right? Well, turns out it’s not. The issue is that for mathlib's docs#CategoryTheory.endofunctorMonoidalCategory the tensor product of F and G is F ⋙ G, rather than G ⋙ F, this is an artifact of mathlib's choice to have composition reversed up. Hence, (F ⊗ G) ⊙ x is G.obj (F.obj x), while F ⊙ G ⊙ x is F.obj (G.obj x).

This can be "corrected" if we use the monoidal opposite of C ⥤ C instead of C ⥤ C. But suddenly, the story in the first (edit: and second) paragraph don’t look as nice.
I would advocate refactoring docs#CategoryTheory.endofunctorMonoidalCategory to make its tensor product be F ⊗ G := G ⋙ F. Note that this should also not impact the equivalence we have between monoids in the endofunctor categories and monads: for this equivalence, we’re tensoring a functor with itself, so order doesn’t matter!

[Joël Riou]

Robin Carlier said:

This can be "corrected" if we use the monoidal opposite of C ⥤ C instead of C ⥤ C. But suddenly, the story in the first paragraph doesn’t look as nice.
I would advocate refactoring docs#CategoryTheory.endofunctorMonoidalCategory to make its tensor product be F ⊗ G := G ⋙ F. Note that this should also not impact the equivalence we have between monoids in the endofunctor categories and monads: for this equivalence, we’re tensoring a functor with itself, so order doesn’t matter!

I should warn you that if you try this, you would have to refactor basically all the theory of shift functors that is used in the context of triangulated categories.
The easier fix would be to use docs#CategoryTheory.MonoidalOpposite

[Robin Carlier]

Also, a compelling argument for the refactor is that when we think of a monad T as a monoid in the category of endofunctors, then the modules in C over that monoids are the T-algebras. I think I can still prove that with the current Mathlib’s definitions T-algebras are modules over some monoid in the monoidal opposite of C ⥤ C through some general equivalence between Mon_ C and Mon_ Cᴹᵒᵖ, but this would make the statement pointlessly complicated IMO.

[Robin Carlier]

Joël Riou said:

Robin Carlier said:

This can be "corrected" if we use the monoidal opposite of C ⥤ C instead of C ⥤ C. But suddenly, the story in the first paragraph doesn’t look as nice.
I would advocate refactoring docs#CategoryTheory.endofunctorMonoidalCategory to make its tensor product be F ⊗ G := G ⋙ F. Note that this should also not impact the equivalence we have between monoids in the endofunctor categories and monads: for this equivalence, we’re tensoring a functor with itself, so order doesn’t matter!

I should warn you that if you try this, you would have to refactor basically all the theory of shift functors that is used in the context of triangulated categories.
The easier fix would be to use docs#CategoryTheory.MonoidalOpposite

To be fair, not having C ⥤ C acting on C via evaluation "directly" feels so silly that I would almost take the time to refactor the shifts.

I guess yet an other option is to add notations and names for actions of Cᴹᵒᵖ, but then we’re probably close to @Kevin Buzzard's favorite conundrum about left and right actions.

[Robin Carlier]

Robin Carlier said:

Also, a compelling argument for the refactor is that when we think of a monad T as a monoid in the category of endofunctors, then the modules in C over that monoids are the T-algebras. I think I can still prove that with the current Mathlib’s definitions T-algebras are modules over some monoid in the monoidal opposite of C ⥤ C through some general equivalence between Mon_ C and Mon_ Cᴹᵒᵖ, but this would make the statement pointlessly complicated IMO.

(Note also that this equivalence with algebras is important: once we will have monoidal bar constructions on monoids, this kind of statements should be used to obtain "monadic" bar constructions, and here I believe we want the action to have good definitional properties, which I’m not sure we will have by using opposites.)

[Joël Riou]

If you change the monoidal structure on endofunctors, the best solution may be to replace monoidal functors Discrete A ⥤ C ⥤ C in the definition of shifts by Discrete A ⥤ (C ⥤ C)ᴹᵒᵖ. As I have made the API of shifts mostly separated from that of monoidal functors, this should require only small changes to the more lowlevel shift files.

[Robin Carlier]

Well, would’t that be a compelling reasons to use MonoidalLeftAction (Discrete A) C in shifts? That would of course need to go deeper that what you suggest but this would feel more "moral", no? Or do you really prefer to have things use as little general monoidal category theory as possible? Silly me, this is a right action if we change the composition order.

[Robin Carlier]

Looking at it with everything reversed, it now looks weird that the whiskerLeft of endofunctorMonoidalCategory is the whiskerRight, and whiskerRight is the whisker left, and the horizontal composition is also "reversed".

So I guess maybe I was overly optimistic on how everything would looks better with everything reversed and I apologize for calling an immediate refactor a bit quickly.

The question boils down to how much we want to align with the non-mathlib litterature.

Do we prefer something that is something which is "in line" with the litterature, in which case we must reverse this strucure because what we call "the composition monoidal structure", is what everyone else would call its opposite. Or do we want something that is more coherent with mathlib’s choice, and keep things as is?

The last option is to just redefine left actions to be in sync with monoidal functors to endofunctors, and then we have (x ⊗ y) ⊙ z ≅ y ⊙ x ⊙ z and we tell people to "just get over to it" the same way we tell them to get used to the reverse composition order. With this, we still get a nice evaluation left action. It’s also the easiest refactor since left actions aren’t even merged.

I see pros and cons for every single of these options. So I’ll wait for more feedback from maintainers.
Perhaps @Kim Morrison considered this when introducing this monoidal structure back in 2020?

[Robin Carlier]

After thinking a bit more about this, I think the best course of action is the following:

• Keep endoFunctorMonoidalCategory as is, however, add to its docstring that it is the monoidal opposite of what is usually considered in the literature under this name.
• Introduce right actions, with their set of notations and lemmas (this one is already done at #25840)
• Prove left actions correspond to monoidal functors _ ⥤ (_ ⥤ _)ᴹᵒᵖ, and that right actions correspond to monoidal functors _ ⥤ (_ ⥤ _).
• Endofunctors acts on the right on the base category, and document in the docstring that it is because of the fact that endofunctors are monoidal opposite to the construction used in the literature.
• Quality of life and also WIP: various constructors/equivalences between left/right actions and right/left ᴹᵒᵖ actions.

[Robin Carlier]

Optionally, when all this is done, I guess shifts could be refactored as right actions? this would be completely cosmetic and it would bring nothing more than some satisfaction of making it fit in a general framework, and perhaps remove some code duplication?

[Robin Carlier]

Also, I suppose the plan above should also include defining (internal) right modules, with an equivalence with usual (left) modules over the monoidal opposite of the algebra, through the equivalence Mon_ C ≌ Mon_ Cᴹᵒᵖ defined in #25854.

[Robin Carlier]

Points 3 and 4 in list above are now at #25875

[Robin Carlier]

Last point is at #25860