So I guess that this is my

I am a PhD student in Glasgow, in the university of Strathclyde, mostly studying category theory and monoidal category adjacent things. Right now, I am really into Hopf Monads

· · Tootle for Mastodon · · ·

@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!