@Jonoidal welcome to Mathstodon! I'll bite, what is a Hopf Monad and how is it different to an ordinary monad?
@jeslie0 Hey James! The idea behind a Hopf monad is that they are meant to be a generalisation of a whole bunch of various “Hopf” structures. Without going too deep into it, if you have a closed monoidal category C, and a monad H, then the Eilenberg Moore category of H will be closed monoidal (in a certain canonical way) iff H is a Hopf monad. What is wild is that this is enough to draw some pretty strong similarities between Hopf algebras and Hopf monads. It’s really pretty!
@Jonoidal ahh, so does this mean that the monad formed from the free-forgetful adjunction on \(R\)-Mod is a Hopf Monad? Hopf algebras are things always wanted learn about, but constantly put on the back burner with everything else I want to look at
@jeslie0 Maybe? It haven't thought about it, but the adjunction \(R\)-Mod\(\rightarrow\) Ab might be Hopf?
Essentially, the requirement is that the forgetful functor is strong monoidal. So if
\[U:R-Mod \rightarrow Ab\]
is the forgetful functor, then you need
\[U(A \otimes B) \cong UA \otimes UB\]
Do you know if that is true?
@Jonoidal I think this is going to be false if we forget down to Set, but it might be true here. I haven't played around that much with abelian categories, so I don't know if that isomorphism holds.
@jeslie0 i see that you are into Agda - most of my colleagues are Agda people, but I’ve unfortunately not learned enough about type theory while I’ve been here to be good conversation 😛
I probably won’t get it, but what kind of stuff are you doing with Hott?
The social network of the future: No ads, no corporate surveillance, ethical design, and decentralization! Own your data with Mastodon!