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: learning: questions

Topic: Funny tensor product

John Wiegley (Aug 30 2022 at 18:13):

I'm trying to define the funny tensor product in Coq, and the idea of "separately functorial" that distinguishes it from the cartesian product. However, I'm stuck on how to concretely define morphisms in the category C □ D. Mark Weber describes this using generators and relations, but I'm having difficulty translating this characterization into a type of morphisms. Can anyone offer further hints or guidance?

Mike Shulman (Aug 30 2022 at 18:21):

In type theory, an object described using generators and relations can either be a higher inductive type or (under conditions or assumptions that make this valid) the quotient of an inductive type. What approach are you taking to quotients in Coq?

Mike Shulman (Aug 30 2022 at 18:23):

It might be possible to describe the morphisms in $C\mathbin{\Box} D$ as a purely inductive type without any quotients in some cases, but I would expect you need at least some assumption like decidability of the identity morphisms in $C$ and $D$.

John Wiegley (Aug 30 2022 at 18:27):

I suppose a first question before answering that would be: Is generators+relations the only way to define the morphisms of this category?

John Wiegley (Aug 30 2022 at 18:35):

I'm looking for a definition that is constructive, and can be computable, like the morphisms in the regular product category. As I understand it, it's just this difference in functoriality that should matter. Is it accurate to say that?

Mike Shulman (Aug 30 2022 at 18:35):

I intended to address that point in my second comment. I believe that generators and relations is most likely the only constructive way to do it. Classically, or if identity morphisms are decidable, I would conjecture you can probably define the morphisms to be zigzags of nonidentity morphisms that alternate being from $C$ and $D$.

Tobias Schmude (Aug 30 2022 at 18:37):

Why zigzags? Shouldn't they go in the same direction, just alternating between both components?
Or do I misunderstand?

Mike Shulman (Aug 30 2022 at 18:41):

Sorry, I didn't mean zigzags in the sense of "forwards and backwards" but in the sense of "rightwards and downwards". I'm thinking of the objects of $C \mathbin{\Box} D$ as in a grid, with $C$ running left to right and $D$ running up to down. Then the morphisms of $C\times D$ are arbitrary southeasterly diagonals ("as the crow flies") while the morphisms of $C \mathbin{\Box} D$ have to alternate between going due east and due south ("taxicab paths").

Tobias Schmude (Aug 30 2022 at 18:46):

That's a great intuition! Mine was having the component morphisms on two parallel lines, then there are no zig-zags.

Mike Shulman (Aug 30 2022 at 18:49):

Glad you like it. Anyway, the generators-and-relations description says, in particular, that if you have such a zigzag that goes right by some morphism of $C$, then down by an identity morphism in $D$, then right by another morphism of $C$, that's the same as omitting the identity morphism and composing the two morphisms in $C$. If identity morphisms are decidable, then you may be able to eliminate this quotient and obtain a canonical form for morphisms of $C \mathbin{\Box} D$ by requiring all the morphisms in the zigzag to be nonidentities (with the zero-length zigzag being the identity morphism), but constructively without decidable identities it seems to me the quotient is unavoidable.

John Wiegley (Aug 30 2022 at 18:52):

Thank you for the clarification, Mike! I will have to try with quotients then.