Left vs right closed monoidal categories

Stream: mathlib4

[Brendan Seamas Murphy]

In the docstring for CategoryTheory.MonoidalClosed it says that this is defining right monoidal closed categories. But the definition of right closed on wikipedia (and I think on the nlab, if I'm reading it right) would say we've defined a left closed category, because Closed X carries the data of a right adjoint for the left tensoring X ⊗ -. Is this a case where mathematical terminology is inconsistent, and some sources swap the meaning of left and right closed, or is it an error of the doc string?

[Brendan Seamas Murphy]

(I would like to implement separate left and right closed monoidal category classes, and it seems worth figuring this out first)

[Johan Commelin]

cc @Yuma Mizuno

[Yuma Mizuno]

I'm not sure which one (defined for X ⊗ - or - ⊗ X) should be called the left closed, but I think it's reasonable to change the current mathlib version to "left", which is at least consistent with Wikipedia.

Perhaps @Scott Morrison has some ideas?

[Kim Morrison]

I think I choose this name based on having the opposite reading of nlab than Brendan's. They call (- \otimes X) left tensoring. It is of course fairly arbitrary.

[Brendan Seamas Murphy]

Ah, on reread you're right. That is frustrating. I'm not sure what the right choice is, but I guess I don't like it if we use a convention based off (- \otimes X) meaning "left tensoring" when in mathlib tensorLeft X is X \otimes -

[Kim Morrison]

I'm pretty sure the literature is largely inconsistent here. Internal consistency will suffice for us.