Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
concerning the discussion here: notice that an entry rig category had once been created, already.
In a ring, the absorption/annihilation law $0\cdot x = 0$ follows from distributivity and additive inverses, since $0\cdot x + 0\cdot x = (0+0)\cdot x = 0\cdot x$ and we can cancel one copy to obtain $0\cdot x = 0$. In a rig, however, we have to assert absorption separately. So shouldn’t a rig category also include isomorphisms $x\otimes 0 \cong x \cong 0\otimes x$ as part of its structure?
(And indeed, Laplaza includes them.)
It’s worth noting though that in the case where $\oplus$ is the categorical coproduct, that $0 \otimes x \cong 0$ comes for free.
Are you saying that if we assume $\otimes$ preserves binary coproducts in each variable, then it automatically preserves initial objects in each variable as well?
Also: changed.
Yes: if we assume the natural canonical map $x \otimes y + x \otimes z \to x \otimes (y + z)$ is an isomorphism, then putting $y = 0$, $z = 1$ (the monoidal unit), we obtain a natural isomorphism
$x \otimes 0 + x \to x$whose restriction to the inclusion of $x$ is the identity $x \to x$. Let $k$ be its restriction to the inclusion of $x \otimes 0$. Then we obtain a bijection
$\hom(x, x) \stackrel{\langle 'k', id \rangle}{\to} \hom(x \otimes 0, x) \times \hom(x, x)$and this forces $\hom(x \otimes 0, x)$ to be a singleton, for any $x$.
Did you mean to say that we get a bijection
$\hom(x, y) \stackrel{\langle 'k', id \rangle}{\to} \hom(x \otimes 0, y) \times \hom(x, y)$for any $x$ and $y$, hence $hom(x\otimes 0,y)$ is a singleton? Anyway, this is nice — it should go at distributive monoidal category.
I thought my reasoning worked (where $y = x$) since $\hom(x, x)$ is inhabited. No?
My apologies: I see what Mike is saying, and now I don’t see how to prove my claim. (What happened is that I remembered a (true) statement that the claim holds in the case of cartesian monoidal categories, and thought that would generalize right away to the more general case.)
(And, in fact, it’s trivially false. For example, the coproduct $\vee$ on a join-semilattice preserves binary coproducts in each variable but not the initial object.)
I added to distributive monoidal category a modified claim (remark 1) and proof.
Okay, great. I moved this remark out of the “Definition” section where I didn’t think it exactly belonged.
1 to 12 of 12