Cartesian monoidal star-autonomous categories

Disclaimer: This is a crosspost (see MathStackexchange). Apologies if cross-posting is frowned upon. However, it seems that on Stackexchange there are not many people familiar with star-autonomous categories.

1. Question
Any rigid cartesian monoidal category is trivial (see here). Star-autonomity is a generalization of rigidity. Are there (non-trivial) examples of star-autonomous cartesian monoidal categories? Neither Zhen Lin's nor Martin Brandenburg's arguments for the rigid case seem to be easily adaptable to star-autonomous categories.

I use the following definition:
A monoidal category $$(C, \otimes,I)$$ carries a star-autonomous structure if there exists an equivalence of categories $$S: C^{op} \xrightarrow{\sim} C$$ with inverse $$S’$$ such that there there are bijections $$\phi_{X,Y,Z}: \operatorname{Hom}_C(X \otimes Y,SZ) \xrightarrow{\sim} \operatorname{Hom}_C(X, S(Y \otimes Z))$$ natural in $$X,Y,Z.$$

I tried the category Pos of posets and monotone maps. This category is cartesian closed. The product is the product order. The set of monotone maps between two posets becomes a poset by setting $$f \leq g \text{ for } f,g: X \rightarrow Y \text{ if } f(x)\leq g(x) \text{ for all } x\in X.$$ Does this category admit a star-autonomous structure? Is it even self-dual? If on objects one sets $$S(X):=X^{op}$$ with $$X^{op}$$ the dual poset, it is not clear to me how to define the mapping on morphisms in order to obtain a duality functor. In the category of sup-lattices such a definition is possible, but it uses the existence of joins.

• I cannot object to cross-posting ... since you waited a week to do so. It would be good to add a link to this post in the math.se post. Jun 15 at 12:07

[I'm going to assume $$S' \cong S$$, which holds in every symmetric monoidal $$*$$-autonomous category. (See e.g. Lemma 5.6 of this paper.) This applies here since cartesianness implies symmetry. Part of the proof also works with weaker assumptions, such as merely that the monoidal unit is terminal. Hat tip to Todd Trimble for indicating what this answer really should be.]

Proposition: The cartesian monoidal $$*$$-autonomous categories are exactly those that are equivalent to Boolean algebras (with $$S$$ being negation and $$\land$$ as monoidal structure).

Proof: Every Boolean algebra, considered as a posetal category, is a $$*$$-autonomous cartesian monoidal category, since both $$x \land y \le \lnot z$$ and $$x \le \lnot(y \land z)$$ are equivalent to $$x \land y \land z = \bot$$.

For the other direction, let us first show that such a category $$C$$ must be a preorder; this is also known as Joyal's Lemma.

Taking $$Z := SI$$ produces an isomorphism $$1 \cong \mathrm{Hom}_C(X \otimes Y,I) \cong \mathrm{Hom}_C(X \otimes Y,SSI) \cong \mathrm{Hom}_C(X,S(Y \otimes SI))$$ natural in $$X$$ and $$Y$$. This yields an isomorphism $$S(Y \otimes S'I) \cong I$$ natural in $$Y$$ by Yoneda, or equivalently $$Y \otimes S'I \cong SI$$. Hence the dualizing object $$SI$$ is "absorbing" for the monoidal structure, and since $$S$$ is a contravariant equivalence, we also know that it is initial.

But now $$SI \otimes SI \cong SI$$ together with initiality shows that the two product projections $$SI \otimes SI \to SI$$ are equal. Hence any two parallel morphisms $$f,g : A \to SI$$ are equal for any $$A$$. But then since $$\mathrm{Hom}_C(X,Y) \cong \mathrm{Hom}_C(X\otimes SY,SI),$$ we can conclude that any two parallel morphisms are equal, and $$C$$ is equivalent to a poset.

In the poset case, the cartesian monoidal structure must be $$\land$$, so we have a meet-semilattice, and $$S$$ is an antitone involution with $$x \land y \le Sz \quad \Longleftrightarrow \quad x \le S(y \land z).$$ But then it follows that $$C$$ is a Heyting algebra, $$Sx = (x \to \bot)$$ is negation, and every element is equal to its double negation. Therefore $$C$$ is a Boolean algebra. $$\Box$$

By the way, $$\mathbf{Pos}$$ is not contravariant equivalent to itself, for example because it has a strict initial object but not a strict terminal object.

• You can and should go further: show that a cartesian $\ast$-autonomous category is indeed equivalent to a Boolean algebra. The proof is not very difficult. Jun 16 at 22:51
• After having woken up (literally) I was just about to write "distributive lattice with appropriate negation (i.e. Boolean algebra)" – but you were faster. Nice answer, thank you.
– M.C.
Jun 17 at 5:17
• @ToddTrimble: thanks, I've added that in. I guess that this is all standard material, but I could also add more detail to the proof especially in the last paragraph if desired. Jun 17 at 8:55
• I don't think that the nLab-definition is weaker than mine. They require the monoidal category to be symmetric.
– M.C.
Jun 17 at 9:45
• Yes, that sounds like one way to do it. I now see that there's also a more expicit and more general statement in Lemma 5.6. Jun 17 at 12:29