# Monoidal categories - Category Theory

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

If `F :: C -> D` is a monoidal functor, then for any monoid object `X : C, ...` in `C`, `F X : D, ...` is a monoid object in `D`

can we go further and change that "If" to an "Iff"?

what do you mean by a "monoid object?"

@Christoph Horst I haven't heard of a monoidal equivalence before. is that something different from a lax monoidal functor?

@Will A "monoid object" is basically a way of generalizing the concept of a monoid. The normal monoids we're used to are monoid objects in the monoidal category of sets and functions.

https://en.wikipedia.org/wiki/Monoid_(category_theory) if you're interested

In category theory, a branch of mathematics, a monoid (or monoid object) (M, μ, η) in a monoidal category (C, ⊗, I) is an object M together with two morphisms

but a monoidal equivalence should be something like the monoidal version of an equivalence of categories ... a pair of monoidal functors going back and forth s.t. the composite is naturally isomorphic to the identity, plus some conditions that hopefully become clear when one tries to draw the diagrams ...
pretty sure something like this exists. but it doesn't answer your question

Hmm. Well we can strengthen lax monoidal to strong monoidal or strict monoidal, I'm not sure if that works out to be the same thing as what you're suggesting

I also found the definition in my favourite CT textbook
seems to be standard :-)

can we state this in terms of adjunctions?

like, they're adjoint two ways almost it seems

(if FX has a monoid structure doesn't imply X does.)

@Ohad Kammar That's not exactly the claim

let me state it a different way

If, for every monoid object `X` in `C`, `F X` is also a monoid object (with the data of the monoid given by the appropriate applications of `F` and its laxity to the data of `X`), is `F` a monoidal functor?

@Christoph Horst I was thinking about it a bit more and it does seem remarkably close to having two adjunctions out of the given functors that are "related" in a certain way, so that the counits and units come together to form isomorphisms

@Asad Saeeduddin I don't understand what the claim is, as I don't see what monoid structure on `X` you are trying to show is a monoid.
You need two morphisms:

```e : I --> X
p : X (*) X -> X
```

In general, without knowing something about `X` or the categories I am working with, I don't have these two morphisms.
Even if I have such morphisms on `F X`:

```e' : I' --> FX
p'  : FX (*') FX --> FX
```

that doesn't mean I can find an appropriate `e` and `p` for `X`.

as I don't see what monoid structure on X you are trying to show is a monoid.

I'm not trying to show that `X` is a monoid. We already know it is the case that:

- if `F : C -> D`, `ϕ`, `ψ` is a monoidal functor
- then for every monoid object `X : C` in `C`, `F X : D` is a monoid object (with the data of the monoid object `F X` derived from the data of the monoid object `X` using `F`, `ϕ` and `ψ`)

The question is simply whether we can change that if to an iff and the statement is still true. The additional burden of proof is to switch the if and then in those bullet points and see if the resulting proposition is true.

In general, without knowing something about X or the categories I am working with

You know that:

- (C, ⨁, I, ...) and (D, ⨂, J, ...) are monoidal categories
- F is a functor from C to D
- ϕ is a natural transformation `(F _ ⨂ F _) -> F (_ ⨁ _)`
- ψ is a morphism `J -> F I`
- for every monoid object (X, +_C : X ⨁ X -> X , 0_C : I -> X ) in C,
there is a monoid object (F X, +_D : F X ⨂ F X -> F X, 0_D : J -> F X) in D
- the data of the monoid object `F X` is derived from the data of the monoid object `X`. i.e.
- +_D = F +_C ∘ ϕ
- 0_D = F 0_C ∘ ψ

This is what you get from assuming the second "then" bullet point in the list above. If all of this is true, is `F`, `ϕ`, `ψ` a lax monoidal functor?

This has some chance of being true.

If you're stuck, you might as well try the following. I don't know if
it works out --- haven't checked it.

Step 1:

Assuming `(C, ⨁, I, ...)` is also monoidal bi-closed, I think that
for each `C`-object `A`, we have a monoid structures on `A^A` (for
each choice of adjoint `-^A`). By our assumption, each `F(A^A)` is
then a monoid. Moreover, we have a morphism `F(A^A) ⨂ FA -> FA` for
one of these `^A`, and `FA ⨂ F(A^A)` for the other, which let us think
of `F(A^A)` as a subobject of "`FA ^ FA`" (whether or not this
exponential actually exists in `D`).

Now try to see whether by chasing appropriate `I`-elements of `A^A`
and `((A ⨁ B) ⨁ C)^((A ⨁ B) ⨁ C)` you can deduce that `F` is in fact
monoidal.

Step 2, if step 1 works out:

We can move from `C` to a monoidal bi-closed category `[C^op, Set]`
using Yoneda and the Day tensor product, and similarly to
`[D^op, Set]`.

Perhaps you can then deduce that if `F` maps monoids to monoids, then
it extends to a similar functor `[C^op, Set] -> [D^op, Set]` that maps
monoids to monoids, and so by Step 1 is a monoidal functor.

If that's the case, perhaps you can deduce the original `F` is monoidal.

Step 3, if step 2 works out:

If step 2 works out, this means there should be an elementary proof for
the converse. Find it. :P.

Well, since the identity function is a catamorphism, and you can always use it to derive a solution, maybe it's just not a descriptive concept

Put differently, when does a problem has no catamorphic solution?

Hi,
I have a question about monoidal categories. The axioms for a monoid are 1) composition, 2) existence of a left/right unit, and 3) associativity. For a monoidal category the tensor product define composition, there is a unit and laws for this unit, but I'm not sure I understand the associator. I mean there is an associator but there is also a daunting pentagram axiom diagram. Is there an explanation of this pentagram, I mean why do we need it to define a monoidal category and not to define a monoid ? Would not having it makes a monoidal category not equivalent to a monoid for the category of set ?