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: Dependent external tensor product

Callan McGill (Nov 08 2022 at 04:38):

If we have a indexed monoidal category $(\mathbb{V}, \otimes)$ over a cartesian monoidal category $\mathrm{S}$ then one can construct the external tensor product (see here) where given $\mathrm{X}, \mathrm{Y} \in \mathrm{S}$, we have (something like):

$$\boxtimes : \mathbb{V}_{\mathrm{X}} \rightarrow \mathbb{V}_{\mathrm{Y}} \rightarrow \mathbb{V}_{X \times Y}$$ $$\{V_x\}_{x \in \mathrm{X}} \boxtimes \{W_y\}_{y \in \mathrm{Y}} \mapsto \{V_x \otimes W_y\}_{(x, y) \in \mathrm{X} \times \mathrm{Y}}$$

Does anyone know of any generalization where $\mathrm{Y}$ can be dependent on $\mathrm{X}$ and the target is not over the product but the dependent sum?

Mike Shulman (Nov 08 2022 at 05:01):

Well, just as $V\boxtimes W$ is defined by pulling $V$ and $W$ both back to $X\times Y$ and tensoring them there, if you have $Y\in S/X$ and $V \in \mathbb{V}_X$ with $W\in \mathbb{V}_Y$, you could just pull $V$ back along the projection $Y\to X$ and tensor it there with $W$.

Callan McGill (Nov 08 2022 at 05:12):

True! I was curious if you (or anyone else) has come across this construction in your work?

Mike Shulman (Nov 08 2022 at 05:24):

Doesn't ring any immediate bells.

Callan McGill (Nov 08 2022 at 06:14):

I was hoping it might be related to the indexed coproduct in $\mathbb{V}$, for instance that sort of one-sided pullback looks reminiscent of the projection formula.

Mike Shulman (Nov 08 2022 at 07:47):

You could push it forward again along something, but that starts to look more like the canceling tensor product rather than the external one.

Matteo Capucci (he/him) (Nov 08 2022 at 11:07):

Callan McGill said:

If we have a indexed monoidal category $(\mathbb{V}, \otimes)$ over a cartesian monoidal category $\mathrm{S}$ then one can construct the external tensor product (see here) where given $\mathrm{X}, \mathrm{Y} \in \mathrm{S}$, we have (something like):

$$\boxtimes : \mathbb{V}_{\mathrm{X}} \rightarrow \mathbb{V}_{\mathrm{Y}} \rightarrow \mathbb{V}_{X \times Y}$$ $$\{V_x\}_{x \in \mathrm{X}} \boxtimes \{W_y\}_{y \in \mathrm{Y}} \mapsto \{V_x \otimes W_y\}_{(x, y) \in \mathrm{X} \times \mathrm{Y}}$$

Does anyone know of any generalization where $\mathrm{Y}$ can be dependent on $\mathrm{X}$ and the target is not over the product but the dependent sum?

It seems like you have to consider a nested indexing then: $\mathbb V$ is not an indexed monoidal category but an indexed monoidal indexed category!
In this way you can talk about $\mathbb V_Y$ being 'dependent' on $\mathbb V_X$. I don't see a slick way to define $\boxtimes$ in this case, I mean as a known kind of structure to associate to this indexing

Matteo Capucci (he/him) (Nov 08 2022 at 11:17):

Mmh ok maybe it's easier than I thought, what about this?
image.png

Matteo Capucci (he/him) (Nov 08 2022 at 11:17):

Here I identify $\Sigma$ with the domain opfibration $\cal C^\downarrow \to C$

Matteo Capucci (he/him) (Nov 08 2022 at 11:19):

$\mathbb V$ is monoidally fibred over $\cal C$ (and its equivalent to your indexed monoidal cat with the same name)

Matteo Capucci (he/him) (Nov 08 2022 at 11:21):

Additionally, you have $\mathbb W$ which is also fibred over $\cal C^\downarrow$, so for any $Y \to X$ ($Y$ dependent over $X$) we have a category $\mathbb W_{Y \to X}$

Matteo Capucci (he/him) (Nov 08 2022 at 11:21):

Then ⅀ (I'm very happy this symbol exists in Unicode) has type

$$⅀:\mathbb W_{Y \to X} \to \mathbb V_Y$$

Matteo Capucci (he/him) (Nov 08 2022 at 11:23):

It's not exactly what you want but how do you make $\mathbb V_{Y \to X}$ typecheck otherwise?

Matteo Capucci (he/him) (Nov 08 2022 at 11:26):

Just for comparison, the external tensor product can also be presented in a similar manner: image.png

Matteo Capucci (he/him) (Nov 08 2022 at 11:27):

and of course there's no need for the bottom opfibration here image.png to be dom, it could be anything you have giving you Sigma types

Matteo Capucci (he/him) (Nov 08 2022 at 11:28):

(Like, for instance, $\times$)

Matteo Capucci (he/him) (Nov 08 2022 at 11:30):

Notice it makes sense to consider this bottom opfibration to be part of a span $\cal C \leftarrow D \to C$ where the left leg is a fibration and the right leg is an opfibration. Then you extend this up and you could make $\mathbb W$ fibered over $\mathbb V$

Matteo Capucci (he/him) (Nov 08 2022 at 11:30):

image.png

Mike Shulman (Nov 08 2022 at 16:40):

Maybe I misunderstood, but I don't think Callan suggested that $\mathbb{V}_Y$ could be dependent on $\mathbb{V}_X$, only that $Y$ could be dependent on $X$.

Matteo Capucci (he/him) (Nov 08 2022 at 18:21):

Uhm right

Matteo Capucci (he/him) (Nov 08 2022 at 18:21):

Matteo Capucci (he/him) said:

Then ⅀ (I'm very happy this symbol exists in Unicode) has type

$$⅀:\mathbb W_{Y \to X} \to \mathbb V_Y$$

So actually this is not as bad as I thought