Skip to main content
added 75 characters in body
Source Link
Todd Trimble
  • 53.3k
  • 6
  • 205
  • 322

As for the question on prominent display, you've answered it yourself (in other words, no, you did not make a mistake).

However, I don't understand why such an equation "must" be added to the definition of binoidal category; I don't think it should be added at all! I am guessing that your problem is not so much with the notion of binoidal category, as it is with an alleged incompleteness of the notion of premonoidal category.

Here's how I see it. Let $\otimes$ denote the non-cartesian symmetric monoidal product on the 1-category $Cat$. A binoidal category is then a category $C$ equipped with a "magma" structure

$$m: C \otimes C \to C.$$

The definition of premonoidal category then involves a (central) natural transformation $\alpha$ between two functors shown below:

$$[(C \otimes C) \otimes C \stackrel{m \otimes 1_C}{\to} C \otimes C \stackrel{m}{\to} C] \stackrel{\alpha}{\Rightarrow} [(C \otimes C) \otimes C \stackrel{\text{assoc}}{\to} C \otimes (C \otimes C) \stackrel{1_C \otimes m}{\to} C \otimes C \stackrel{m}{\to} C]$$

Now, given $f: x \to x'$ in $C$, there is a well-formed morphism

$$(f \otimes y) \otimes z: (x \otimes y) \otimes z \to (x' \otimes y) \otimes z$$

in $(C \otimes C) \otimes C$. The associativity of the monoidal category $(Cat, \otimes)$ is a functor that takes this morphism to a morphism

$$f \otimes (y \otimes z): x \otimes (y \otimes z) \to x' \otimes (y \otimes z)$$

in $C \otimes (C \otimes C)$. It looks like the thing you are asking about has to do with the application of the natural isomorphism $\alpha$ to $(f \otimes y) \otimes z$ in the triple tensor power of $C$. The other instances contained in your query box on the nLab article would be handled similarly; they all devolve on the non-cartesian symmetric monoidal structure on $Cat$.

P.S.: Who is the mathematician displayed in your avatar/icon?

As for the question on prominent display, you've answered it yourself (in other words, no, you did not make a mistake).

However, I don't understand why such an equation "must" be added to the definition of binoidal category; I don't think it should be added at all! I am guessing that your problem is not so much with the notion of binoidal category, as it is with an alleged incompleteness of the notion of premonoidal category.

Here's how I see it. Let $\otimes$ denote the non-cartesian symmetric monoidal product on the 1-category $Cat$. A binoidal category is then a category $C$ equipped with a "magma" structure

$$m: C \otimes C \to C.$$

The definition of premonoidal category then involves a (central) natural transformation $\alpha$ between two functors shown below:

$$[(C \otimes C) \otimes C \stackrel{m \otimes 1_C}{\to} C \otimes C \stackrel{m}{\to} C] \stackrel{\alpha}{\Rightarrow} [(C \otimes C) \otimes C \stackrel{\text{assoc}}{\to} C \otimes (C \otimes C) \stackrel{1_C \otimes m}{\to} C \otimes C \stackrel{m}{\to} C]$$

Now, given $f: x \to x'$ in $C$, there is a well-formed morphism

$$(f \otimes y) \otimes z: (x \otimes y) \otimes z \to (x' \otimes y) \otimes z$$

in $(C \otimes C) \otimes C$. The associativity of the monoidal category $(Cat, \otimes)$ is a functor that takes this morphism to a morphism

$$f \otimes (y \otimes z): x \otimes (y \otimes z) \to x' \otimes (y \otimes z)$$

in $C \otimes (C \otimes C)$. It looks like the thing you are asking about has to do with the application of the natural isomorphism $\alpha$ to $(f \otimes y) \otimes z$ in the triple tensor power of $C$. The other instances contained in your query box on the nLab article would be handled similarly; they all devolve on the non-cartesian symmetric monoidal structure on $Cat$.

As for the question on prominent display, you've answered it yourself (in other words, no, you did not make a mistake).

However, I don't understand why such an equation "must" be added to the definition of binoidal category; I don't think it should be added at all! I am guessing that your problem is not so much with the notion of binoidal category, as it is with an alleged incompleteness of the notion of premonoidal category.

Here's how I see it. Let $\otimes$ denote the non-cartesian symmetric monoidal product on the 1-category $Cat$. A binoidal category is then a category $C$ equipped with a "magma" structure

$$m: C \otimes C \to C.$$

The definition of premonoidal category then involves a (central) natural transformation $\alpha$ between two functors shown below:

$$[(C \otimes C) \otimes C \stackrel{m \otimes 1_C}{\to} C \otimes C \stackrel{m}{\to} C] \stackrel{\alpha}{\Rightarrow} [(C \otimes C) \otimes C \stackrel{\text{assoc}}{\to} C \otimes (C \otimes C) \stackrel{1_C \otimes m}{\to} C \otimes C \stackrel{m}{\to} C]$$

Now, given $f: x \to x'$ in $C$, there is a well-formed morphism

$$(f \otimes y) \otimes z: (x \otimes y) \otimes z \to (x' \otimes y) \otimes z$$

in $(C \otimes C) \otimes C$. The associativity of the monoidal category $(Cat, \otimes)$ is a functor that takes this morphism to a morphism

$$f \otimes (y \otimes z): x \otimes (y \otimes z) \to x' \otimes (y \otimes z)$$

in $C \otimes (C \otimes C)$. It looks like the thing you are asking about has to do with the application of the natural isomorphism $\alpha$ to $(f \otimes y) \otimes z$ in the triple tensor power of $C$. The other instances contained in your query box on the nLab article would be handled similarly; they all devolve on the non-cartesian symmetric monoidal structure on $Cat$.

P.S.: Who is the mathematician displayed in your avatar/icon?

Source Link
Todd Trimble
  • 53.3k
  • 6
  • 205
  • 322

As for the question on prominent display, you've answered it yourself (in other words, no, you did not make a mistake).

However, I don't understand why such an equation "must" be added to the definition of binoidal category; I don't think it should be added at all! I am guessing that your problem is not so much with the notion of binoidal category, as it is with an alleged incompleteness of the notion of premonoidal category.

Here's how I see it. Let $\otimes$ denote the non-cartesian symmetric monoidal product on the 1-category $Cat$. A binoidal category is then a category $C$ equipped with a "magma" structure

$$m: C \otimes C \to C.$$

The definition of premonoidal category then involves a (central) natural transformation $\alpha$ between two functors shown below:

$$[(C \otimes C) \otimes C \stackrel{m \otimes 1_C}{\to} C \otimes C \stackrel{m}{\to} C] \stackrel{\alpha}{\Rightarrow} [(C \otimes C) \otimes C \stackrel{\text{assoc}}{\to} C \otimes (C \otimes C) \stackrel{1_C \otimes m}{\to} C \otimes C \stackrel{m}{\to} C]$$

Now, given $f: x \to x'$ in $C$, there is a well-formed morphism

$$(f \otimes y) \otimes z: (x \otimes y) \otimes z \to (x' \otimes y) \otimes z$$

in $(C \otimes C) \otimes C$. The associativity of the monoidal category $(Cat, \otimes)$ is a functor that takes this morphism to a morphism

$$f \otimes (y \otimes z): x \otimes (y \otimes z) \to x' \otimes (y \otimes z)$$

in $C \otimes (C \otimes C)$. It looks like the thing you are asking about has to do with the application of the natural isomorphism $\alpha$ to $(f \otimes y) \otimes z$ in the triple tensor power of $C$. The other instances contained in your query box on the nLab article would be handled similarly; they all devolve on the non-cartesian symmetric monoidal structure on $Cat$.