Okay, great. I moved this remark out of the “Definition” section where I didn’t think it exactly belonged.

]]>I added to distributive monoidal category a modified claim (remark 1) and proof.

]]>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 thought my reasoning worked (where $y = x$) since $\hom(x, x)$ is inhabited. No?

]]>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.

]]>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$.

]]>Also: changed.

]]>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?

]]>It’s worth noting though that in the case where $\oplus$ is the categorical coproduct, that $0 \otimes x \cong 0$ comes for free.

]]>(And indeed, Laplaza includes them.)

]]>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?

]]>concerning the discussion here: notice that an entry *rig category* had once been created, already.