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: Dual Day Convolution?

Max New (Mar 24 2022 at 17:21):

I was working with the Day convolution of presheaves, specifically where my base category is the free monoid from a set X. I noticed that in addition to the Day convolution (forgive my type theoretic notation for coends/ends):

$(P \otimes Q)w = \sum_{w_1w_2 = w} P w_1 \times Q w_2$
with unit
$I w = w = \epsilon$

you can define a dual

$(P || Q)w = \prod_{w_1w_2 = w} P w_1 + Q w_2$
with unit a
$O w = w \neq \epsilon$

I was hoping this would provide a linearly distributive category structure, but I think it doesn't. It looks like a kind of "constructive negation" of the tensor but it didn't match anything from Shulman's affine constructive logic afaict.

Anyway is this a well known structure?

Mike Shulman (Mar 24 2022 at 17:23):

Is $\parallel$ even associative?

Mike Shulman (Mar 24 2022 at 17:23):

The associativity of $\otimes$ depends on the distributivity of $\times$ over $\sum$...

Max New (Mar 24 2022 at 17:50):

Hm I thought it was but looking at it in more detail I think not? Is it possible it gives a (non-symmetric) polycategory that is not representable or is that ruled out too?

Mike Shulman (Mar 24 2022 at 17:53):

BTW I think your formulas should have $P w_1$ and $Q w_2$?

Mike Shulman (Mar 24 2022 at 17:55):

So the explicit definition of the putative polycategory structure would I guess be that a morphism $(P_1,\dots,P_m) \to (Q_1,\dots, Q_n)$ consists of, for each equation $v_1 + \cdots + v_m = w_1 + \cdots + w_n$, a morphism $P_1 v_1 \times \cdots \times P_m v_m \to Q_1 w_1 + \cdots + Q_n w_n$?

Mike Shulman (Mar 24 2022 at 17:57):

If the monoid is trivial, then this would be essentially trying to define a polycategory structure on $\rm Set$ with $\times$ and $+$ as the product and coproduct. It's known that that doesn't work to make a linearly distributive category, even though in that case $+$ is associative. I'd have to look back at the argument to be positive that you can't get a nonrepresentable polycategory either, but it seems unlikely to me.

Jacques Carette (Mar 25 2022 at 13:36):

Somewhat related: Brent Yorgey's thesis has a nice leisurely exposition (sections 4.2 and 5.1 specifically) of what Day Convolution specializes to for different choices of the two monoidal structures involved. His work is also quite influenced by type theory, so it should be a comfortable read for @Max New .