3
$\begingroup$

I am missing something to prove that the initial algebra $A^*=\mu x. Fx$ of the functor $FX=I+A \otimes X $ is the free monoid in a monoidal category.

Here's one start

enter image description here

enter image description here

Summing up I can build 2 arrows in blue like so

enter image description here then by going through the $-\otimes A \dashv -^A $ adjunction I get and algebra for $A^{*A^*}$ so I get an arrow from $A^*$ by initiality

enter image description here

So I get $m$ coming back through the adjunction and $e= \delta . inl$ as given. So, I have a monoid $(A^*,m,e)$, and I can put A things in it, that's a good start.

enter image description here

Now, take a monoid $(G,e,m)$, a function f from A to G, the paper claims the initial algebra verifies the universal property

enter image description here

and that

enter image description here

But I am not sure how to prove that the universal property is verified :

enter image description here

Any reference or tips appreciated


The solution given in diagram enter image description here

$\endgroup$

1 Answer 1

3
$\begingroup$

In the right upper part of the diagram, you can reduce $F(\mathsf{free} f) \circ \mathsf{inr}$ to $\mathsf{id} \otimes \mathsf{free} f : A \otimes A^{*} \to A \otimes G$.

You end up with $(\mathsf{id} \otimes \mathsf{free} f) \circ (\mathsf{id} \otimes e)$, which is $\mathsf{id} \otimes e_G$. There you can swap the order with $f \otimes \mathsf{id}$ (a.k.a. $- \otimes -$ functoriality) to apply $(G, m_G, e_G)$'s right identity law.

For the uniqueness part, I think you can use the initiality of $A^{*}$.

$\endgroup$
1
  • $\begingroup$ awesome...... thank you ! $\endgroup$
    – nicolas
    Jan 14, 2016 at 18:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .