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.
Naïm Favier (Feb 16 2024 at 15:09):Let be an idempotent monad in a cartesian monoidal category (I may want to consider monoidal categories with diagonals more generally, but let's keep it simple), with left and right monoidal strengths and . I am trying, and miserably failing, to prove that the following (outer) diagram commutes:
screenshot-2024-02-16-160553.png
That is, in pseudo-Haskell, liftM2 (,) a a = fmap (λ x → (x, x)) a (which is the usual definition of an "idempotent applicative functor"). The triangles are my attempts, but I still have no idea whether the remaining square commutes. Any ideas?
Naïm Favier (Feb 16 2024 at 22:00):I figured it out:
screenshot-2024-02-16-225953.png
Naïm Favier (Feb 16 2024 at 22:14):I wonder if there's a general strategy for proving this sort of things... I sort of just stared at nlab's proof that idempotent strong monads are commutative until inspiration struck
Hugo Paquet (Feb 18 2024 at 16:24):I don't think this diagram is well-formed (maximal paths don't all end in the same place).
I'd also like to know if this property is true. "Idempotent" in this context seems a bit ambiguous, e.g. the Maybe monad is idempotent as an applicative functor but not as a monad.
Naïm Favier (Feb 18 2024 at 16:36):Oops, you're right. I thought I had convinced myself it worked despite the wonkiness, but now I'm not so sure. I'll see if I can salvage it.
Yes, "idempotent" is ambiguous and not a great name anyway since this does not correspond to the notion of an idempotent monoid in any way. I think a better name would be "diagonal monoidal functor", but oh well (the name "idempotent monoidal functor" is already established in Programming contextual computations).
Naïm Favier (Feb 18 2024 at 17:55):Fixed it:
screenshot-2024-02-18-184753.png
It's still :woozy_face: but at least I can translate it into an equational chain now:
Tδ
= Tδ ; Tη ; μ (monad law)
= Tδ ; T (A × η) ; Ts ; μ (η is left-strong)
= Tδ ; T (A × η) ; η ; μ ; Ts ; μ (monad law)
= Tδ ; T (A × η) ; T (η × TA) ; Tt ; μ ; Ts ; μ (η is right-strong)
= Tδ ; Т (η × η) ; Tt ; μ ; Ts ; μ
= Tη ; Tδ ; Tt ; μ ; Ts ; μ (naturality of Tδ)
= η ; Tδ ; Tt ; μ ; Ts ; μ (idempotence)
= δ ; t ; η ; μ ; Ts ; μ (naturality of η)
= δ ; t ; Ts ; μ (monad law)