Skip to main content
MathOverflow

Return to Answer

minor correction and remark
Source Link
LorenzoPerticone
LorenzoPerticone
  • 613
  • 3
  • 12

This might not be the right approach, but here's my take on the question:

If $(\mathcal{C}, \otimes, I, \dots)$ is a (strict, for the sake of readability) monoidal category, we can endow $[\mathcal{C}, \mathcal{C}]$ with two different monoidal structures:

  1. The "usual" monoidal structure, where $\circ$ is the product and $\mathbf{1}_\mathcal{C}$ is the unit. This is the monoidal category whose monoids are called monads. Notice how this doesn't actually use the fact that $\mathcal{C}$ is endowed with a monoidal structure.

  2. The "other" (I sometimes refer to it as "pointwise") monoidal structure has "pointwise $\otimes$" (let's call it $\boxtimes$) as product, and $\Delta_I$ (the constant functor on the unit object of $\mathcal{C}$) as monoidal units. In this category, monoids are related to what Haskell programmers call "alternative" functors, but without the part about being "applicative" and with one additional property. This can be further generalized to the case of functors $\mathcal{B} \to \mathcal{C}$ where $\mathcal{B}$ is not required to be monoidal, and everything that follows should work just fine (but I won't venture there).

Let me elaborate on the latter, since the former is (probably) already well-known to most haskell programmers here (other than being significantly less relevant):

First we'll need to properly define $\boxtimes$: if we fix functors $\mathcal{F}, \mathcal{G} : \mathcal{C} \to \mathcal{C}$ we can define $(\mathcal{F} \boxtimes \mathcal{G}) (a) := \mathcal{F}(a) \otimes \mathcal{G}(a)$ (the definition for morphisms is analogous). This, together with $\Delta_I$ as a unit, defines a monoidal category: all axioms (and further properties, such as symmetry and strictness) follow trivially from the monoidal structure on $\mathcal{C}$.

Now, monoids in this monoidal category are what haskell programmers call "alternative" functors, but that's not all: they are so in a functorial way, meaning that if $f : a \to b : \mathcal{C}$ and $\mathcal{M}$ is a monoid in $([\mathcal{C}, \mathcal{C}], \boxtimes, \Delta_I)$ then $\mathcal{M}(f)$ is a morphism of monoids. To see this, note how this diagram needs to commute in a pointwise fashion, and the same applies to this other diagram too. We're in the strict case, but nothing significant changes in the general one (except that you need to keep track of the coherence laws).

A more abstract (but equivalent) formulation is that each object $\mathcal{M} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ naturally defines a functor $\hat{\mathcal{M}} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, and this point of view leads to the observation that this actually defines a functor $(\hat{-}) : \mathbf{Mon}([\mathcal{C}, \mathcal{C}]) \to [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$.

What this amounts to is just that a "monoidal" natural transformation $\nu : \mathcal{M} \to \mathcal{N} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ between monoid object in this "pointwise" monoidal category of (endo)functors also defines a natural transformation $\hat{\nu} : \hat{\mathcal{M}} \to \hat{\mathcal{N}} : [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$: the argument is similar but you need to look at the diagrams for morphisms of monoids.

Things are not over yet: it seems that $(\hat{-})$ is actually an equivalence of categories! You can convince yourself of this if you squint hard enough, and the argument is roughly "brute force":

Let's construct a strict inverse to $(\hat{-})$, call it $(\tilde{-})$: take $\mathcal{F} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, compose it with the forgetful functor $\mathbf{U} : \mathbf{Mon}(\mathcal{C}) \to \mathcal{C}$. We'll now use the "forgotten structure" on $\mathcal{F}$ to endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$: to do this, notice how the monoid structure on $\mathcal{F}(a)$ (for $a : \mathcal{C}$) needs to be such that each morphism $\mathcal{F}(f) : \mathcal{F}(a) \to \mathcal{F}(b)$ is a morphism of monoids: this amounts to saying that the correspondences $a \mapsto \mathbf{m}^{\mathcal{F}(a)}$ and $a \mapsto \mathbf{e}^{\mathcal{F}(a)}$ are natural in $a$ and hence natural transformations (its now trivial to check that these endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$).

We now need to check that $(\hat{-}) \circ (\tilde{-}) = \mathbf{1}_{[\mathcal{C}, \mathbf{Mon}(\mathcal{C})]}$ and $(\tilde{-} \circ \hat{-}) = \mathbf{1}_{\mathbf{Mon}([\mathcal{C}, \mathcal{C}])}$: they should both be long and trivial computations, and I'll (boldly) omit them.

Edit: this can probably be "merged" to the other answer by Andrej Bauer to give a more complete answer

This might not be the right approach, but here's my take on the question:

If $(\mathcal{C}, \otimes, I, \dots)$ is a (strict, for the sake of readability) monoidal category, we can endow $[\mathcal{C}, \mathcal{C}]$ with two different monoidal structures:

  1. The "usual" monoidal structure, where $\circ$ is the product and $\mathbf{1}_\mathcal{C}$ is the unit. This is the monoidal category whose monoids are called monads. Notice how this doesn't actually use the fact that $\mathcal{C}$ is endowed with a monoidal structure.

  2. The "other" (I sometimes refer to it as "pointwise") monoidal structure has "pointwise $\otimes$" (let's call it $\boxtimes$) as product, and $\Delta_I$ (the constant functor on the unit object of $\mathcal{C}$) as monoidal units. In this category, monoids are what Haskell programmers call "alternative" functors, but with one additional property. This can be further generalized to the case of functors $\mathcal{B} \to \mathcal{C}$ where $\mathcal{B}$ is not required to be monoidal, and everything that follows should work just fine (but I won't venture there).

Let me elaborate on the latter, since the former is (probably) already well-known to most haskell programmers here (other than being significantly less relevant):

First we'll need to properly define $\boxtimes$: if we fix functors $\mathcal{F}, \mathcal{G} : \mathcal{C} \to \mathcal{C}$ we can define $(\mathcal{F} \boxtimes \mathcal{G}) (a) := \mathcal{F}(a) \otimes \mathcal{G}(a)$ (the definition for morphisms is analogous). This, together with $\Delta_I$ as a unit, defines a monoidal category: all axioms (and further properties, such as symmetry and strictness) follow trivially from the monoidal structure on $\mathcal{C}$.

Now, monoids in this monoidal category are what haskell programmers call "alternative" functors, but that's not all: they are so in a functorial way, meaning that if $f : a \to b : \mathcal{C}$ and $\mathcal{M}$ is a monoid in $([\mathcal{C}, \mathcal{C}], \boxtimes, \Delta_I)$ then $\mathcal{M}(f)$ is a morphism of monoids. To see this, note how this diagram needs to commute in a pointwise fashion, and the same applies to this other diagram too. We're in the strict case, but nothing significant changes in the general one (except that you need to keep track of the coherence laws).

A more abstract (but equivalent) formulation is that each object $\mathcal{M} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ naturally defines a functor $\hat{\mathcal{M}} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, and this point of view leads to the observation that this actually defines a functor $(\hat{-}) : \mathbf{Mon}([\mathcal{C}, \mathcal{C}]) \to [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$.

What this amounts to is just that a "monoidal" natural transformation $\nu : \mathcal{M} \to \mathcal{N} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ between monoid object in this "pointwise" monoidal category of (endo)functors also defines a natural transformation $\hat{\nu} : \hat{\mathcal{M}} \to \hat{\mathcal{N}} : [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$: the argument is similar but you need to look at the diagrams for morphisms of monoids.

Things are not over yet: it seems that $(\hat{-})$ is actually an equivalence of categories! You can convince yourself of this if you squint hard enough, and the argument is roughly "brute force":

Let's construct a strict inverse to $(\hat{-})$, call it $(\tilde{-})$: take $\mathcal{F} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, compose it with the forgetful functor $\mathbf{U} : \mathbf{Mon}(\mathcal{C}) \to \mathcal{C}$. We'll now use the "forgotten structure" on $\mathcal{F}$ to endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$: to do this, notice how the monoid structure on $\mathcal{F}(a)$ (for $a : \mathcal{C}$) needs to be such that each morphism $\mathcal{F}(f) : \mathcal{F}(a) \to \mathcal{F}(b)$ is a morphism of monoids: this amounts to saying that the correspondences $a \mapsto \mathbf{m}^{\mathcal{F}(a)}$ and $a \mapsto \mathbf{e}^{\mathcal{F}(a)}$ are natural in $a$ and hence natural transformations (its now trivial to check that these endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$).

We now need to check that $(\hat{-}) \circ (\tilde{-}) = \mathbf{1}_{[\mathcal{C}, \mathbf{Mon}(\mathcal{C})]}$ and $(\tilde{-} \circ \hat{-}) = \mathbf{1}_{\mathbf{Mon}([\mathcal{C}, \mathcal{C}])}$: they should both be long and trivial computations, and I'll (boldly) omit them.

This might not be the right approach, but here's my take on the question:

If $(\mathcal{C}, \otimes, I, \dots)$ is a (strict, for the sake of readability) monoidal category, we can endow $[\mathcal{C}, \mathcal{C}]$ with two different monoidal structures:

  1. The "usual" monoidal structure, where $\circ$ is the product and $\mathbf{1}_\mathcal{C}$ is the unit. This is the monoidal category whose monoids are called monads. Notice how this doesn't actually use the fact that $\mathcal{C}$ is endowed with a monoidal structure.

  2. The "other" (I sometimes refer to it as "pointwise") monoidal structure has "pointwise $\otimes$" (let's call it $\boxtimes$) as product, and $\Delta_I$ (the constant functor on the unit object of $\mathcal{C}$) as monoidal units. In this category, monoids are related to what Haskell programmers call "alternative" functors, but without the part about being "applicative" and with one additional property. This can be further generalized to the case of functors $\mathcal{B} \to \mathcal{C}$ where $\mathcal{B}$ is not required to be monoidal, and everything that follows should work just fine (but I won't venture there).

Let me elaborate on the latter, since the former is (probably) already well-known to most haskell programmers here (other than being significantly less relevant):

First we'll need to properly define $\boxtimes$: if we fix functors $\mathcal{F}, \mathcal{G} : \mathcal{C} \to \mathcal{C}$ we can define $(\mathcal{F} \boxtimes \mathcal{G}) (a) := \mathcal{F}(a) \otimes \mathcal{G}(a)$ (the definition for morphisms is analogous). This, together with $\Delta_I$ as a unit, defines a monoidal category: all axioms (and further properties, such as symmetry and strictness) follow trivially from the monoidal structure on $\mathcal{C}$.

Now, monoids in this monoidal category are what haskell programmers call "alternative" functors, but that's not all: they are so in a functorial way, meaning that if $f : a \to b : \mathcal{C}$ and $\mathcal{M}$ is a monoid in $([\mathcal{C}, \mathcal{C}], \boxtimes, \Delta_I)$ then $\mathcal{M}(f)$ is a morphism of monoids. To see this, note how this diagram needs to commute in a pointwise fashion, and the same applies to this other diagram too. We're in the strict case, but nothing significant changes in the general one (except that you need to keep track of the coherence laws).

A more abstract (but equivalent) formulation is that each object $\mathcal{M} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ naturally defines a functor $\hat{\mathcal{M}} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, and this point of view leads to the observation that this actually defines a functor $(\hat{-}) : \mathbf{Mon}([\mathcal{C}, \mathcal{C}]) \to [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$.

What this amounts to is just that a "monoidal" natural transformation $\nu : \mathcal{M} \to \mathcal{N} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ between monoid object in this "pointwise" monoidal category of (endo)functors also defines a natural transformation $\hat{\nu} : \hat{\mathcal{M}} \to \hat{\mathcal{N}} : [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$: the argument is similar but you need to look at the diagrams for morphisms of monoids.

Things are not over yet: it seems that $(\hat{-})$ is actually an equivalence of categories! You can convince yourself of this if you squint hard enough, and the argument is roughly "brute force":

Let's construct a strict inverse to $(\hat{-})$, call it $(\tilde{-})$: take $\mathcal{F} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, compose it with the forgetful functor $\mathbf{U} : \mathbf{Mon}(\mathcal{C}) \to \mathcal{C}$. We'll now use the "forgotten structure" on $\mathcal{F}$ to endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$: to do this, notice how the monoid structure on $\mathcal{F}(a)$ (for $a : \mathcal{C}$) needs to be such that each morphism $\mathcal{F}(f) : \mathcal{F}(a) \to \mathcal{F}(b)$ is a morphism of monoids: this amounts to saying that the correspondences $a \mapsto \mathbf{m}^{\mathcal{F}(a)}$ and $a \mapsto \mathbf{e}^{\mathcal{F}(a)}$ are natural in $a$ and hence natural transformations (its now trivial to check that these endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$).

We now need to check that $(\hat{-}) \circ (\tilde{-}) = \mathbf{1}_{[\mathcal{C}, \mathbf{Mon}(\mathcal{C})]}$ and $(\tilde{-} \circ \hat{-}) = \mathbf{1}_{\mathbf{Mon}([\mathcal{C}, \mathcal{C}])}$: they should both be long and trivial computations, and I'll (boldly) omit them.

Edit: this can probably be "merged" to the other answer by Andrej Bauer to give a more complete answer

Source Link
LorenzoPerticone
LorenzoPerticone
  • 613
  • 3
  • 12

This might not be the right approach, but here's my take on the question:

If $(\mathcal{C}, \otimes, I, \dots)$ is a (strict, for the sake of readability) monoidal category, we can endow $[\mathcal{C}, \mathcal{C}]$ with two different monoidal structures:

  1. The "usual" monoidal structure, where $\circ$ is the product and $\mathbf{1}_\mathcal{C}$ is the unit. This is the monoidal category whose monoids are called monads. Notice how this doesn't actually use the fact that $\mathcal{C}$ is endowed with a monoidal structure.

  2. The "other" (I sometimes refer to it as "pointwise") monoidal structure has "pointwise $\otimes$" (let's call it $\boxtimes$) as product, and $\Delta_I$ (the constant functor on the unit object of $\mathcal{C}$) as monoidal units. In this category, monoids are what Haskell programmers call "alternative" functors, but with one additional property. This can be further generalized to the case of functors $\mathcal{B} \to \mathcal{C}$ where $\mathcal{B}$ is not required to be monoidal, and everything that follows should work just fine (but I won't venture there).

Let me elaborate on the latter, since the former is (probably) already well-known to most haskell programmers here (other than being significantly less relevant):

First we'll need to properly define $\boxtimes$: if we fix functors $\mathcal{F}, \mathcal{G} : \mathcal{C} \to \mathcal{C}$ we can define $(\mathcal{F} \boxtimes \mathcal{G}) (a) := \mathcal{F}(a) \otimes \mathcal{G}(a)$ (the definition for morphisms is analogous). This, together with $\Delta_I$ as a unit, defines a monoidal category: all axioms (and further properties, such as symmetry and strictness) follow trivially from the monoidal structure on $\mathcal{C}$.

Now, monoids in this monoidal category are what haskell programmers call "alternative" functors, but that's not all: they are so in a functorial way, meaning that if $f : a \to b : \mathcal{C}$ and $\mathcal{M}$ is a monoid in $([\mathcal{C}, \mathcal{C}], \boxtimes, \Delta_I)$ then $\mathcal{M}(f)$ is a morphism of monoids. To see this, note how this diagram needs to commute in a pointwise fashion, and the same applies to this other diagram too. We're in the strict case, but nothing significant changes in the general one (except that you need to keep track of the coherence laws).

A more abstract (but equivalent) formulation is that each object $\mathcal{M} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ naturally defines a functor $\hat{\mathcal{M}} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, and this point of view leads to the observation that this actually defines a functor $(\hat{-}) : \mathbf{Mon}([\mathcal{C}, \mathcal{C}]) \to [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$.

What this amounts to is just that a "monoidal" natural transformation $\nu : \mathcal{M} \to \mathcal{N} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ between monoid object in this "pointwise" monoidal category of (endo)functors also defines a natural transformation $\hat{\nu} : \hat{\mathcal{M}} \to \hat{\mathcal{N}} : [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$: the argument is similar but you need to look at the diagrams for morphisms of monoids.

Things are not over yet: it seems that $(\hat{-})$ is actually an equivalence of categories! You can convince yourself of this if you squint hard enough, and the argument is roughly "brute force":

Let's construct a strict inverse to $(\hat{-})$, call it $(\tilde{-})$: take $\mathcal{F} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, compose it with the forgetful functor $\mathbf{U} : \mathbf{Mon}(\mathcal{C}) \to \mathcal{C}$. We'll now use the "forgotten structure" on $\mathcal{F}$ to endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$: to do this, notice how the monoid structure on $\mathcal{F}(a)$ (for $a : \mathcal{C}$) needs to be such that each morphism $\mathcal{F}(f) : \mathcal{F}(a) \to \mathcal{F}(b)$ is a morphism of monoids: this amounts to saying that the correspondences $a \mapsto \mathbf{m}^{\mathcal{F}(a)}$ and $a \mapsto \mathbf{e}^{\mathcal{F}(a)}$ are natural in $a$ and hence natural transformations (its now trivial to check that these endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$).

We now need to check that $(\hat{-}) \circ (\tilde{-}) = \mathbf{1}_{[\mathcal{C}, \mathbf{Mon}(\mathcal{C})]}$ and $(\tilde{-} \circ \hat{-}) = \mathbf{1}_{\mathbf{Mon}([\mathcal{C}, \mathcal{C}])}$: they should both be long and trivial computations, and I'll (boldly) omit them.