Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: Idempotent monoid objects

Asad Saeeduddin (Apr 16 2020 at 17:34):

What sort of additional equipment is necessary on top of a monoidal structure in order to be able to talk about "idempotent monoid objects"?

sarahzrf (Apr 16 2020 at 17:37):

probably something along these lines https://ncatlab.org/nlab/show/monoidal+category+with+diagonals

sarahzrf (Apr 16 2020 at 17:38):

what you want to say is that the identity is equal to the squaring map, so you need to be able to define a squaring map

sarahzrf (Apr 16 2020 at 17:39):

hence you need to be able to "duplicate elements of the monoid", in internal phrasing

Asad Saeeduddin (Apr 16 2020 at 17:40):

I was looking at that, but I couldn't figure out when we have such a "monoidal category with diagonals" besides when the category is fully cartesian

sarahzrf (Apr 16 2020 at 17:40):

it does say that the monoidal product will be cartesian if it has both diagonals and deletion

Nathanael Arkor (Apr 16 2020 at 17:41):

The nLab page gives an example: pointed sets with the smash product.

sarahzrf (Apr 16 2020 at 17:41):

the monoidal product on Rel w/ the graph of Set's diagonal might qualify for this—lemme think about it

Reid Barton (Apr 16 2020 at 17:42):

What is "idempotent monoid object" supposed to mean? Are idempotent monads supposed to be an example?

sarahzrf (Apr 16 2020 at 17:42):

ooh

Asad Saeeduddin (Apr 16 2020 at 17:42):

@Nathanael Arkor isn't that category still cartesian?

sarahzrf (Apr 16 2020 at 17:42):

i just assumed something which would specialize to the ordinary notion of an idempotent monoid in Set

sarahzrf (Apr 16 2020 at 17:42):

it isnt cartesian

Asad Saeeduddin (Apr 16 2020 at 17:43):

no, that's what I'm trying to avoid. I don't want to be specific to Set, or even to cartesian monoidal categories, because I suspect I have an example of this, but the category is not cartesian monoidal

Reid Barton (Apr 16 2020 at 17:43):

I know the point of the question is that you are looking for a definition, but it would be nice to have some more clues about what it is you are trying to define :upside_down:

sarahzrf (Apr 16 2020 at 17:44):

you want to avoid your definition producing ordinary idempotent monoids when you interpret it in Set? :mischievous:

Reid Barton (Apr 16 2020 at 17:44):

For example: at least one example of a category in which you know how to define the object, and what the object is supposed to be there.

Reid Barton (Apr 16 2020 at 17:45):

Since we apparently have two entirely different interpretations already.

Reid Barton (Apr 16 2020 at 17:45):

Or at least, I think they're entirely different.

sarahzrf (Apr 16 2020 at 17:49):

mm, yeah i think they are different

sarahzrf (Apr 16 2020 at 17:51):

idempotence in reference to a Set monoid is talking about the multiplication, whereas idempotence in reference to a monad is talking about application of the monad

Asad Saeeduddin (Apr 16 2020 at 17:51):

Sorry, let me start at the beginning. I have a category of functors $F : \mathbf{Set} \to \mathbf{Set}$ which are monoids with respect to the Day convolution monoidal structure on $[\mathbf{Set}, \mathbf{Set}]$ . Moreover, the monoidal structure on $\mathbf{Set}$ which induces the Day convolution monoidal structure on the functor category admits a "diagonal map" just as you mentioned.

sarahzrf (Apr 16 2020 at 17:51):

is this some kind of infinitary generalization of species? :thinking:

sarahzrf (Apr 16 2020 at 17:52):

oh wait ur not using the groupoid core either, thats fairly different

Asad Saeeduddin (Apr 16 2020 at 17:54):

let's call that monoidal structure $\otimes : \mathbf{Set} \times \mathbf{Set} \to \mathbf{Set}$ , and its diagonal map $\Delta_{\otimes} : X \to X \otimes X$

sarahzrf (Apr 16 2020 at 17:54):

which monoidal structure on Set are you using?

sarahzrf (Apr 16 2020 at 17:54):

just the cartesian one?

Asad Saeeduddin (Apr 16 2020 at 17:55):

no, it's a different one besides the cartesian one

sarahzrf (Apr 16 2020 at 17:55):

(was thinking that cocartesian seemed plausible in this context)

Asad Saeeduddin (Apr 16 2020 at 17:55):

it's actually literally the coproduct of the cartesian and cocartesian structures

sarahzrf (Apr 16 2020 at 17:55):

o.O

sarahzrf (Apr 16 2020 at 17:55):

coproduct in which category?

Asad Saeeduddin (Apr 16 2020 at 17:55):

in $\mathbf{Set}$

sarahzrf (Apr 16 2020 at 17:56):

the cartesian and cocartesian structures aren't sets, so how can you take their coproduct in set...?

sarahzrf (Apr 16 2020 at 17:56):

you mean pointwise, or

Asad Saeeduddin (Apr 16 2020 at 17:56):

Yes, the functor category $[\mathbf{Set} \times \mathbf{Set}, \mathbf{Set}]$ admits "pointwise" coproducts

sarahzrf (Apr 16 2020 at 17:57):

wasnt sure if maybe there was some fancy category of monoidal structures that might have different coproducts or sth

sarahzrf (Apr 16 2020 at 17:57):

so A ⊗ B is A × B + A + B, then...

sarahzrf (Apr 16 2020 at 17:57):

interesting... is this supposed to be something like "one of A and B, but maybe both"

Asad Saeeduddin (Apr 16 2020 at 17:58):

Right. And now we're talking about that tensor on $\mathbf{Set}$ lifted via Day convolution to the endofunctor category on $\mathbf{Set}$

Asad Saeeduddin (Apr 16 2020 at 17:58):

right, exactly

Asad Saeeduddin (Apr 16 2020 at 17:59):

in other words, we're talking about the category of lax monoidal functors that cohere the monoidal structure of $\otimes$ on $\mathbf{Set}$ with the monoidal structure of the product on $\mathbf{Set}$

sarahzrf (Apr 16 2020 at 18:00):

wait what

sarahzrf (Apr 16 2020 at 18:00):

where did that "in other words" come from? i didnt notice anything about lax monoidal functors so far

Asad Saeeduddin (Apr 16 2020 at 18:01):

A monoid with respect to Day convolution is the same as a lax monoidal functor

sarahzrf (Apr 16 2020 at 18:01):

ooooooh right

sarahzrf (Apr 16 2020 at 18:01):

ok, hold on a moment

sarahzrf (Apr 16 2020 at 18:01):

lemme think about what day convolution looks like in this case

sarahzrf (Apr 16 2020 at 18:03):

so a representative of an element (F ⊗ G)(S) is elements F(A), G(B), and functions A × B → S, A → S, B → S...

Asad Saeeduddin (Apr 16 2020 at 18:04):

yup, exactly

sarahzrf (Apr 16 2020 at 18:04):

:thinking:

Asad Saeeduddin (Apr 16 2020 at 18:04):

or you could just say $A \otimes B \to S$

sarahzrf (Apr 16 2020 at 18:04):

yeah but i wanted to expand it

sarahzrf (Apr 16 2020 at 18:05):

is this for haskell purposes by any chance :upside_down:

Asad Saeeduddin (Apr 16 2020 at 18:05):

so the monoid here takes a little getting used to, but now what I want to talk about is "idempotent" monoids. because we have an obvious diagonal map $A \to A \otimes A$

sarahzrf (Apr 16 2020 at 18:05):

i smell some kind of zipping

Asad Saeeduddin (Apr 16 2020 at 18:05):

busted :)

Asad Saeeduddin (Apr 16 2020 at 18:06):

i'm formalizing "alignable" functors

sarahzrf (Apr 16 2020 at 18:06):

hmm, well, i was already suspicious when i saw your ⊗

sarahzrf (Apr 16 2020 at 18:06):

but this clinches it

sarahzrf (Apr 16 2020 at 18:07):

right, ⊗ is These

Asad Saeeduddin (Apr 16 2020 at 18:08):

I went through the laws for the Semialign class and some of them I was able to dismiss as free theorems, most of the others follow from having a symmetric monoidal functor, but the "idempotent" law is what I'm trying to unravel

sarahzrf (Apr 16 2020 at 18:08):

/me looks up Semialign

sarahzrf (Apr 16 2020 at 18:09):

zip :: f a -> f b -> (These a b -> c) -> f c

sarahzrf (Apr 16 2020 at 18:09):

sarahzrf (Apr 16 2020 at 18:10):

i typed that before actually opening the haddock

sarahzrf (Apr 16 2020 at 18:12):

ok im not quite seeing how this corresponds to a monoid object though

Asad Saeeduddin (Apr 16 2020 at 18:13):

you mean you don't get how a lax monoidal functor corresponds to a monoid in some structure?

sarahzrf (Apr 16 2020 at 18:13):

no wait

sarahzrf (Apr 16 2020 at 18:13):

sorry i think i had some things backwards in my head

sarahzrf (Apr 16 2020 at 18:13):

lemme chew on it for another minute

Asad Saeeduddin (Apr 16 2020 at 18:14):

align :: f a -> f b -> f (These a b)

Asad Saeeduddin (Apr 16 2020 at 18:14):

this is the fundamental operation of the Semialign class

Asad Saeeduddin (Apr 16 2020 at 18:14):

we can make the laxity more obvious if we write it as align :: (f a, f b) -> f (These a b)

sarahzrf (Apr 16 2020 at 18:15):

no sorry yeah i got it

sarahzrf (Apr 16 2020 at 18:15):

(i wasnt thinking of it in lax functor terms)

sarahzrf (Apr 16 2020 at 18:16):

ok, join align

sarahzrf (Apr 16 2020 at 18:16):

ha, obnoxious phrasing

sarahzrf (Apr 16 2020 at 18:17):

hmm, interesting

Asad Saeeduddin (Apr 16 2020 at 18:17):

i think this is align . dup, where dup is the diagonal map for the cartesian monoidal structure

Asad Saeeduddin (Apr 16 2020 at 18:17):

and join These is the diagonal map for the other monoidal structure

sarahzrf (Apr 16 2020 at 18:17):

yeah

sarahzrf (Apr 16 2020 at 18:17):

but

sarahzrf (Apr 16 2020 at 18:18):

um, one sec

sarahzrf (Apr 16 2020 at 18:19):

okay, this is interesting... so align isn't the monoid multiplication, alignWith is

Asad Saeeduddin (Apr 16 2020 at 18:19):

yes

Asad Saeeduddin (Apr 16 2020 at 18:20):

align is the laxity of a monoidal functor, which is equivalent to a monoid wrt Day convolution. alignWith is the append operation of that monoid

Asad Saeeduddin (Apr 16 2020 at 18:22):

hence (align | alignWith) as the minimal complete definition

sarahzrf (Apr 16 2020 at 18:22):

i bet we have duplication for the day convolution

sarahzrf (Apr 16 2020 at 18:22):

have you checked that already?

Asad Saeeduddin (Apr 16 2020 at 18:22):

I haven't

Asad Saeeduddin (Apr 16 2020 at 18:23):

I did think about it a bit, but it didn't seem to work

sarahzrf (Apr 16 2020 at 18:23):

oh really

sarahzrf (Apr 16 2020 at 18:23):

hm, ok, so we have x in F(A) and we need to give an element of (F ⊗ F)(A)

sarahzrf (Apr 16 2020 at 18:24):

which we can do by giving some F(X), F(Y), and These X Y → A

Asad Saeeduddin (Apr 16 2020 at 18:24):

I have a duplication for the These monoidal structure, but that's the opposite of what it seems I need to obtain a natural transformation from F to its Day convolution with itself

sarahzrf (Apr 16 2020 at 18:24):

yea

sarahzrf (Apr 16 2020 at 18:24):

i see what u mean

sarahzrf (Apr 16 2020 at 18:24):

hmmm

sarahzrf (Apr 16 2020 at 18:26):

im tempted to say what if we just went with F(A), F(A), and These A A → A by being left-biased

sarahzrf (Apr 16 2020 at 18:26):

but that gives me a bad vibe

Asad Saeeduddin (Apr 16 2020 at 18:26):

maybe i'm approaching this the wrong way in trying to somehow involve the Day convolution monoid in my search for an "idempotent monoid"

Asad Saeeduddin (Apr 16 2020 at 18:27):

maybe what we have instead is that the duplication is preserved by the functor

Asad Saeeduddin (Apr 16 2020 at 18:27):

uh, what's that thing with bimonoids

sarahzrf (Apr 16 2020 at 18:28):

no idea

Asad Saeeduddin (Apr 16 2020 at 18:28):

the comultiplication is a monoid homomorphism and the multiplication is a comonoid homomorphism

Asad Saeeduddin (Apr 16 2020 at 18:28):

or something like that

sarahzrf (Apr 16 2020 at 18:28):

frobenius algebra?

Asad Saeeduddin (Apr 16 2020 at 18:28):

i'm not sure if frobenius algebra is the same thing, but i remember seeing that name somewhere. "bimonoid" is what I read about

sarahzrf (Apr 16 2020 at 18:29):

oh looks like they arent the same

sarahzrf (Apr 16 2020 at 18:29):

i just saw "both monoid & comonoid structures" & jumped to conclusions :-)

Asad Saeeduddin (Apr 16 2020 at 18:31):

does join These :: a -> These a a work as an associative cosemigroup?

sarahzrf (Apr 16 2020 at 18:35):

yeah

John Baez (Apr 16 2020 at 18:36):

A bimonoid is really different from a Frobenius monoid. The most exciting bimonoid axiom is this one:

multiplication is a homomorphism for comultiplication (and vice versa)

The most exciting Frobenius monoid axiom is this one:

comultiplication commutes with left and right multiplication (and vice versa)

Asad Saeeduddin (Apr 16 2020 at 18:37):

and dup :: a -> (a, a) is obviously also one. So maybe:

uncurry align . dup ≡ fmap (join These)

is talking about some kind of comonoid homomorphism

sarahzrf (Apr 16 2020 at 18:38):

hmm, you know what

sarahzrf (Apr 16 2020 at 18:39):

now im getting distracted by the fact that there is a canonical partial monoid structure on every type for ⊗ = These

sarahzrf (Apr 16 2020 at 18:39):

one that's useful in separation logic, even :3c

sarahzrf (Apr 16 2020 at 18:42):

actually, well, the one i've seen in separation logic is with ⊗ = × and uses Maybe instead, but it's basically the same idea

sarahzrf (Apr 16 2020 at 18:42):

"if you only get one input then thats your result; if you get two equal inputs thats your result; if you get conflicting inputs, no result"

sarahzrf (Apr 16 2020 at 18:42):

hmmm well maybe that's not as canonical as it could be, i guess you could also go for no result period on two inputs

sarahzrf (Apr 16 2020 at 18:50):

aha

sarahzrf (Apr 16 2020 at 18:51):

if we go from x ∈ F(A) to the representative (x, x, id_{A ⊗ A}), then i believe we get a transformation F → F ∘ (-)²

Asad Saeeduddin (Apr 16 2020 at 18:52):

Sorry, I'm not following. Are you talking about join (alignWith id) :: f a -> f (These a a)?

sarahzrf (Apr 16 2020 at 18:52):

where that's the tensor power i mean

sarahzrf (Apr 16 2020 at 18:53):

umm i might be, lemme see

sarahzrf (Apr 16 2020 at 18:53):

no im not

sarahzrf (Apr 16 2020 at 18:54):

this doesnt require any monoid structure or anything

sarahzrf (Apr 16 2020 at 18:54):

actually wait wtf am i saying

sarahzrf (Apr 16 2020 at 18:54):

/me stops and thinks

sarahzrf (Apr 16 2020 at 18:54):

OH i did miswrite sorry :((

sarahzrf (Apr 16 2020 at 18:55):

setwise, the type of the family is F(A) → (F ⊗ F)(A ⊗ A)

Asad Saeeduddin (Apr 16 2020 at 18:55):

sorry, do those two $\otimes$ symbols stand for different things?

sarahzrf (Apr 16 2020 at 18:56):

yeah

sarahzrf (Apr 16 2020 at 18:56):

the first one is day convolution, the second one is These

Asad Saeeduddin (Apr 16 2020 at 18:56):

ok, thanks

Asad Saeeduddin (Apr 16 2020 at 18:56):

so what is the definition of this morphism F(A) → (F ⊗ F)(A ⊗ A)?

sarahzrf (Apr 16 2020 at 18:56):

so that's almost the type of a duplication map in the functor category, except that it's changing the argument

sarahzrf (Apr 16 2020 at 18:57):

and we can instead see it as F → F² ∘ (-)², where (-)² is the tensor power, not the literal power

sarahzrf (Apr 16 2020 at 18:57):

the definition is

sarahzrf (Apr 16 2020 at 18:57):

for an element x of F(A)

Asad Saeeduddin (Apr 16 2020 at 18:58):

ok, I understand

sarahzrf (Apr 16 2020 at 18:58):

sarahzrf (Apr 16 2020 at 18:59):

so i think the law is that, uh...

Asad Saeeduddin (Apr 16 2020 at 18:59):

ok so we have this thing that is presumably a natural transformation. but we don't have a trivial monoid to get rid of the (-)², instead we have a comonoid on every A

sarahzrf (Apr 16 2020 at 19:00):

well we don't even have a comonoid do we

Asad Saeeduddin (Apr 16 2020 at 19:00):

we do have a monoid to get rid of the F^2

sarahzrf (Apr 16 2020 at 19:00):

yeah

Asad Saeeduddin (Apr 16 2020 at 19:00):

we have a cosemigroup, I haven't thought about the unit

sarahzrf (Apr 16 2020 at 19:00):

most sets don't have a function to the empty set

Asad Saeeduddin (Apr 16 2020 at 19:00):

that half of it doesn't appear in the semialign class anyway

sarahzrf (Apr 16 2020 at 19:01):

yeah but the deletion map of a comonoid has to go to the tensor unit

sarahzrf (Apr 16 2020 at 19:03):

anyway i believe the law is uh.... doing the weird "duplication" in the functor category and then the monoid multiplication is equal to the whiskering of Set's actual duplication

sarahzrf (Apr 16 2020 at 19:03):

"the whiskering of Set's actual duplication" = fmap (join These)

sarahzrf (Apr 16 2020 at 19:08):

i think this is basically like... taking the hypothetical "doing duplication in the functor category and then monoid multiplication is the identity" law, removing a term from the hypothetical definition of duplication in the functor category, and moving it to the other side of the equation

sarahzrf (Apr 16 2020 at 19:10):

instead of putting an inverse to the Set duplication into the functor duplication, we put the Set duplication on the right-hand side

Asad Saeeduddin (Apr 16 2020 at 19:12):

interesting

sarahzrf (Apr 16 2020 at 19:12):

i gotta go tho :T

sarahzrf (Apr 16 2020 at 19:12):

good luck, this seems neat

Asad Saeeduddin (Apr 16 2020 at 19:12):

the more i think about this the more the law seems to be a statement about bimonoids. a monoidal functor is so called because it carries every monoid on the source category to a monoid on the target category. i think all this law is saying is that it sends a bimonoid to a bimonoid

Asad Saeeduddin (Apr 16 2020 at 19:13):

@sarahzrf Thanks for all the help and insights! :wave:

Asad Saeeduddin (Apr 16 2020 at 19:16):

@John Baez Do you know if there is a concept like a weakened bimonoid where one structure is only a (co)semigroup? Are these well studied?

John Baez (Apr 16 2020 at 20:22):

Asad Saeeduddin said:

John Baez Do you know if there is a concept like a weakened bimonoid where one structure is only a (co)semigroup? Are these well studied?

The concept certainly exists: it sounds like you're talking about a semigroup in the category of comonoids (in some symmetric monoidal category), which will be the same as a comonoid in the category of semigroups (in that same symmetric monoidal category). Using theorems about internalization one can quickly prove a lot of basic facts about these gadgets. But I've never heard anyone talk about them!