Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: category theory

Topic: compact closed and biproducts

Christian Williams (Feb 17 2022 at 18:37):

What is this called? Reference?

The category of sets and relations has two monoidal structures, product and sum. product is compact closed (relations $A\times B\to C$ are equivalent to relations $A\to B\times C$) and sum is a biproduct (the inclusions $A\to A+B$ and $B\to A+B$ give coproduct, and their converses give product).

As in ordinary sets and functions, we still have $A\times (B+C)\simeq (A\times B)+(A\times C)$. So this is a very nice structure, and I've been trying to find a reference for what it's called. It seems related to star autonomy, but in Rel one can't express product in terms of sum or vice versa.

Many $\mathbb{V}\mathrm{Prof}$ have this structure, so I want to be able to say exactly what it is.

Christian Williams (Feb 17 2022 at 18:44):

well, I guess we have $A\times B = \sum_A B$. but that seems to be on a different level of abstraction...

Christian Williams (Feb 17 2022 at 18:49):

(Rel more than just a category, really an equipment, but I think it's enough for this question.)

John Baez (Feb 17 2022 at 19:33):

Part of this structure goes by the somewhat unfortunate name [[cartesian bicategory]].

John Baez (Feb 17 2022 at 19:36):

But this just captures the $\times$ part of the story, not the $+$.

Christian Williams (Feb 17 2022 at 19:37):

ah yes, thanks, this is helpful.

Christian Williams (Feb 17 2022 at 19:43):

I think categories of relations often, if not always, have "sums" as biproducts; is that right? If so I'm surprised they didn't include it in the definition (or maybe it follows, so they don't mention it). Biproducts are intertwined with the whole idea of a matrix.

I know cartesian bicategories, allegories etc has plenty of literature, so I imagine the structure has been defined. I'll look into it.

Christian Williams (Feb 17 2022 at 19:57):

okay, so in Cartesian Bicategories I Section 5 they define an abelian bicategory to be a bicategory $\mathbb{B}$ such that both $\mathbb{B}$ and $\mathbb{B}^{co}$ are (cartesian) bicategories of relations.

Christian Williams (Feb 17 2022 at 19:59):

they then give a very nice characterization theorem: "bicategories of relations of abelian categories are precisely the abelian bicategories with tabulations".

Christian Williams (Feb 17 2022 at 20:01):

this is very interesting. but Set isn't abelian, because it's not Ab-enriched... hm.

Christian Williams (Feb 17 2022 at 20:10):

by the way if you read that paper, "biproduct" means 2-categorical product, not the way I'm using it here. they sneak in coproducts by mentioning $\mathbb{B}^{co}$. I want to figure out what this perspective means for just plain Rel.

Evan Patterson (Feb 17 2022 at 22:41):

Hi Christian, here are some of the categorical structures involved, which you may already be aware of:

• the sum in Rel is a biproduct
• the (set-theoretic) product in Rel is a symmetric monoidal product
• together, the product and sum in Rel form a distributive monoidal category

Distributive monoidal categories are intermediate in the hierarchy of distributive structures on monoidal categories, being more general than distributive categories and less general than rig categories.

Evan Patterson (Feb 17 2022 at 22:50):

It is sort of surprising, given that Rel is the prototypical example of a bicategory of relations, that the literature on cartesian bicategories/bicategories of relations talks more about the "abelian" case, of which LinRel is a prime example, rather than the distributive one. In Sec 9 of my partly expository paper on bicategories of relations, I suggest a definition of "distributive bicategory of relations," inspired by some cryptic remarks by Carboni and Walters and the related concept of a distributive allegory.

Christian Williams (Feb 18 2022 at 02:56):

yes, thanks Evan this is very helpful.

now that I've come to care so much about relations, it's like I'm seeing your paper for the first time . great stuff; I need to absorb all of this.

Christian Williams (Feb 18 2022 at 02:59):

Several important properties are implicit in the definition. As the name suggests, the distributive law holds automatically in a distributive bicategry of relations. In fact, if (C, , I) is any compact closed category and  is the coproduct, then C is a distributive monoidal category [Jay93]. Moreover, it can be shown that intersections distribute over unions in a distributive bicategory of relations. Also, the coproduct in a distributive bicategry of relations is automatically a biproduct, by the symmetry of a dagger category. (Alternatively, products or coproducts in a compact closed category are always biproducts [Hou08].)

Christian Williams (Feb 18 2022 at 03:00):

This is exactly the insight I was looking for. Thanks for explaining it clearly. I need to work out the proofs myself.

Christian Williams (Feb 18 2022 at 03:02):

distributive-relations.png

Christian Williams (Feb 18 2022 at 03:04):

distributve-rel.png

Christian Williams (Feb 18 2022 at 03:16):

So, many $\mathbb{V}\mathrm{Mod}$ are "(compact) distributive framed bicategories" (though I believe this concept has not yet been defined). very rich structure.

Christian Williams (Feb 18 2022 at 03:59):

I always want to better understand how concepts "arise" or "form", by looking for what definitions are the simplest.

Rel is so rich, yet it can be defined in a few words: it's the free sum completion (15.21) of Bool.

Christian Williams (Feb 18 2022 at 04:00):

Bool is the simplest thing in the world: $0\to 1$. Yet it is a cosmos: closed, complete and cocomplete.

Christian Williams (Feb 18 2022 at 04:02):

I wonder if we can understand Rel completely by understanding how sum completion turns the logic of Bool into that of Rel.

Christian Williams (Feb 18 2022 at 04:05):

In certain parts of category theory, one might get the impression that products are more fundamental than sums. (I.e. the very definition of limit and colimit.)

But what is a set? It's a sum of points. And what is $A\times B$? It's $\sum_A B$.

Christian Williams (Feb 18 2022 at 04:07):

In Rel we can see a conceptual asymmetry between them which is not apparent in Set.

Christian Williams (Feb 18 2022 at 04:10):

In Rel, sum of sets is coproduct, and by converse relation it is also product. It has both universal properties.

Christian Williams (Feb 18 2022 at 04:13):

Where did this converse come from? Sums also form another monoidal structure $A\times B:= \sum_A B$ which is symmetric and comonoidal. Rather than any universal property, this one is compact closed - we "swap directions" by swapping variables, a data abstraction which we can copy, swap, and delete.

Christian Williams (Feb 18 2022 at 04:14):

(This is somewhat loose; just painting a picture.)

Mike Shulman (Feb 18 2022 at 05:11):

Since you mentioned $\ast$-autonomy, maybe I'll point out that Rel is indeed a model of multiplicative-additive linear logic, in which the tensor product (cartesian product of sets) is both the multiplicative conjunction $\otimes$ and the multiplicative disjunction $⅋$, while the biproduct (coproduct of sets) is both the additive conjunction $\&$ and the additive disjunction $\oplus$. Indeed, any compact closed category is $\ast$-autonomous, hence models multiplicative linear logic with $\otimes = ⅋$, and if it has categorical products and coproducts then they model the additives.

Christian Williams (Feb 18 2022 at 05:14):

yes, thanks. I need to better understand proof nets.

Robin Piedeleu (Feb 18 2022 at 09:17):

I haven't read this whole thread, but perhaps another piece of the puzzle is the fact that, if a compact closed category has categorical products (in your case, the disjoint union of sets) and the monoidal product preserves them, then the products are also biproducts. This can be found in the following paper by Robin Houston: https://arxiv.org/pdf/math/0604542.pdf

Robin Piedeleu (Feb 18 2022 at 09:19):

(This is kind of neat, even if not very surprising, given the duality that defines compact closed categories.)