Monad and identity element

129 Views Asked by At

There are 2 natural transformation are introduced in the monad definition: $$ \mu: T^2 \to T $$ $$ \eta: I \to T $$

The following conditions have to be satisfied: $$ \mu \circ \mu T = \mu \circ T \mu$$ $$ \mu \circ \eta T = \mu \circ T \eta$$ The first one is used for monoid associativity and the second one for identity presence proofs.

From other hand the $\mu$ definition gives us a binary operation $T \otimes T \equiv \otimes(T,T) \equiv \mu(T \cdot T)$ (monoidal product). The operation can be defined as $$T \otimes T = T.$$ I.e. from the definition we already have $T$ as the identity element. I am confusing why do we need the additional one ($ \mu \circ \eta T = \mu \circ T \eta$) to define the identity presence? May be I miss something critical?

EDITION AFTER ASKING: First of all the question is incorrect and can confuse the readers. The following incorrect statements were made:

  1. Natural transformation $\mu$ was declared as monoidal product. Really the monoidal product in the case is the functor composition but not the natural transformation.
  2. The 1. lead to incorrect interpretation for $\mu$ acting on the pair $T,T$ aka $\mu(T^2) = T$. Really if we have a morphism $f_1: a \to b$ and $f_2: a \to b$ then assuming $f_1(a) = b, f_2(a)=b$ leads to incorrect conclusion (that I made) about equality $f_1 = f_2$.
1

There are 1 best solutions below

1
On BEST ANSWER

First, the identity laws are $\mu \circ \eta_T = id_T = \mu \circ T\eta$.

Next, thinking of $\mu$ as a binary operation is an unusual (but doable!) thing. Even taking that view though, what you wrote doesn't make much sense. Making an analogy to a normal, set-theoretic monoid, say addition on $\mathbb N$, we can show where you went wrong. $+:\mathbb N^2\to\mathbb N$. You then say something like we can define some operation via $\mathbb N\otimes\mathbb N=\mathbb N+\mathbb N$ or maybe $=+(\mathbb N\times\mathbb N)$ or something. This part of the question doesn't make any sense. It's both not clear how this defines a binary operation nor is it clear what you even intend $\mu(T\cdot T)$ to mean. The closest thing notationally for $\mu(T\cdot T)$ to mean would be $\mu_{T^2}$ which is not the same sort of thing as $T$ so $T\otimes T=T$ wouldn't make sense, let alone be true.

Thinking of $\mu$ as a kind of binary operator doesn't seem like a thing that is commonly done, but it can be done and is kind of nice. We can make a strict monoidal category whose objects are endofunctors on some given category and whose arrows are natural transformations. The monoidal structure is simply the composition of functors with unit $Id$. Every monoidal category gives rise to a multicategory where, e.g., a multi-arrow $(F,G,H)\to K$ corresponds to an arrow $F\otimes G\otimes H\to K$ in the monoidal category. (To remove the restriction to endofunctors we can instead consider virtual double categories.)

From the above perspective, $\mu$ is a multi-arrow $\mu : (T,T)\to T$ and $\eta : ()\to T$. The monad laws are then basically the monoid laws. $\mu\circ_2(\mu,id_T)=\mu\circ_2(id_T,\mu)$ and $\mu\circ_2(\eta,id_T)=id_T=\mu\circ_2(id_T,\eta)$. This can be made even clearer if we take a doctrinal view via the doctrine of monoidal categories. Then we get $\mu(x,\mu(y,z))=\mu(\mu(x,y),z)$ and $\mu(\eta(),x)=x=\mu(x,\eta())$ which looks exactly like the normal laws for monoids with $\eta$ as the unit.