1
$\begingroup$

I asked this question fourteen days ago on MathStackexchange (see here). I have not received any answers or comments until now. It seems to me that on MathStackexchange not many people are familiar with star-autonomous categories. Following Nick Champion's advice, I therefore have decided to cross-post the question on this site.

1. Question
The n-Lab article on the Chu-construction says:

"Armed with just this much knowledge, and knowledge of how star-autonomous categories behave (as categorified versions of Boolean algebras, or perhaps better Boolean rigs), the star-autonomous structure on $\operatorname{Chu}(C,d)$ can pretty much be deduced (or strongly guessed) […]."

How do star-autonomous categories behave as categorified versions of Boolean algebras or Boolean rigs? In what way is the term categorification used here?

2. Wikipedia says
One explanation might be given on wikipedia:

"A degenerate example [of a star-autonomous category] (all homsets of cardinality at most one) is given by any Boolean algebra (as a partially ordered set) made monoidal using conjunction for the tensor product and taking 0 as the dualizing object."

I suppose the internal hom of two objects $a,b$ in this category is $\neg a \lor b $, correct? The dual functor is the complement?

Edit for future readers: The quoted statement on the nLab seems to have been inaccurate. The nLab entry has now been changed to: "Armed with just this much knowledge, and knowledge of how star-autonomous categories behave (as categorified versions of linear logic), the star-autonomous structure on $\operatorname{Chu}(C,d)$ can pretty much be deduced (or strongly guessed).“

$\endgroup$

1 Answer 1

4
$\begingroup$

The starting point for decategorification is the observation that a category in which any parallel arrows are equal must necessarily be a preorder. Restricting to skeletal categories makes it a poset.

Thus, we might as well ask: what is a *-autonomous category whose underlying category is a poset?

For the specific case when the poset is a Boolean algebra, we set $A→B=A⊸B$, and $A⊢B$ means there is a morphism $A→B$. We have $A⊗X≅(A⊸X^*)^*$, which means $A⊗X=A∧B$. Most axioms of propositional logic are now straightforward to verify. In particular, we can identify the global dualizing object $⊥$: if for all objects $A$ the canonical map $A→(A⊸⊥)⊸⊥$ is an isomorphism, then $⊥$ must be the initial object, since $B⊢(A→B)$ in our case.

More generally, *-autonomous posets that are not Boolean algebras provide models for linear logic. So in the strict sense *-autonomous categories do not categorify Boolean algebras (or rigs), but rather the corresponding algebraic structure for linear logic.

$\endgroup$
7
  • $\begingroup$ Well, any compact closed category is star-autonomous. So you seem to argue that Boolean algebras are categorifications of compact closed categories rather than star-autonomous categories. $\endgroup$ Jun 12, 2022 at 16:47
  • $\begingroup$ @M.C.: It is not me who is arguing this, it is the original poster, who mentioned Boolean rigs vs Boolean algebras in this context. $\endgroup$ Jun 12, 2022 at 16:48
  • $\begingroup$ Right, but then I find their statement rather inaccurate. Thank you for the explanation by the way. $\endgroup$ Jun 12, 2022 at 16:56
  • 3
    $\begingroup$ If I think of dualization as the categorical analog of negation, then the isomorphism $(A\otimes B)^*\cong A^*\otimes B^*$ (for compact closed categories) seems to be the analog of $\neg(A\land B)\equiv (\neg A)\land(\neg B)$, which holds in no nontrivial Boolean algebras. $\endgroup$ Jun 12, 2022 at 17:26
  • 1
    $\begingroup$ I am not sure what you mean by "in our case" in the last sentence. It certainly isn't true that there is always a morphism from $B$ to $A\multimap B$ in any $*$-autonomous category, even if it is a poset. Nor is it true that the dualizing object must be initial. In general, star-autonomous posets are the proof-irrelevant semantics of classical (multiplicative) linear logic, which is more general than classical logic that corresponds to Boolean algebras. $\endgroup$ Jun 13, 2022 at 8:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.