Canonically forming a category from a product?

61 Views Asked by At

Suppose we have a predetermined class of objects, $U$, as well as some notion on how to take the product between any two objects $P:U^2\to U$.

Given these, is there a (canonical) way of constructing a category $C$ whose objects are precisely $\text{ob}(C)=U$ and product is precisely $P$ (perhaps up to isomorphism)?

I am very new to category theory, so I'm only familiar with doing this process in reverse. That is, fixing a category, then determining the notion of a product.


If I consider a very simple example, I can do this through brute force. For example, suppose $\text{ob}(C)=\{\bot,\top\}$ and $P(a,b)=p \wedge q$, then it is not hard to show that a category whose class of morphisms is precisely $\text{hom}(C)=\{\to\}$ works, where $\to$ is the material conditional. However, this approach is no better than just guessing and checking.

1

There are 1 best solutions below

1
On BEST ANSWER

I have no idea why you would want to do this, but here is how you could: The objects are $U$. Now you use some kind of type theory to freely generate arrows and enforce relations between them. You recursively form a set of arrows starting with the symbols in $U$ according to the following rules:

  • when $x\in U$ and $y\in U$, then $p_{1,x,y}:P(x,y)\to x$ is an arrow.

  • when $x\in U$ and $y\in U$, then $p_{2,x,y}:P(x,y)\to y$ is an arrow.

  • when $x,y,z\in U$, $N:z\to x$ and $M:z\to y$ are arrows already build by the recursion, then $pair_{x,y}(M,N): z \to P(x,y)$ is an arrow.

  • when $x\in U$, then $id:x\to x$ is an arrow.

  • when $M:x\to y$ and $N:y\to z$ are arrows, then so is the string $M \circ N:x\to z$

Finally, you quotient the set of arrows by the least amount of relations which you need so that you have a category and the spans with the $p$s become products.

The arrows in your category are formal strings of symbols modulo an equivalence relation.

I want to say though that this is not what category theory is about. You treat categories like some kind of algebraic structure,when in fact you should look at them only up to equivalence. It can still be interesting to do the strict stuff though.