The category of commutative Hopf algebras

Stream: Is there code for X?

[Michał Mrugała]

It seems to me that something like Hopf_ <| Under <| CommRingCat.of R is the correct thing to do, but surprisingly CommRingCat doesn't have a MonoidalCategory instance!

[Eric Wieser]

You can get it through the corresponding structure on AlgebraCat Int

[Michał Mrugała]

I'm not sure how this deals with the non-commutativity, since AlgebraCat ℤ consists of non-commutative algebras as well

[Eric Wieser]

Whoops, I meant docs#CommAlg

[Eric Wieser]

Maybe I'm imagining all of this...

[Eric Wieser]

I'm not going totally mad, this just never made it to mathlib: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Monoidal.20instance.20on.20R-algebras/near/396531046

[Eric Wieser]

There's another thread about CommAlg elsewhere too

[Michał Mrugała]

I made a thread asking if it exists too at some point

[Christian Merten]

Maybe we should make an abbrev CommAlgCat R := Under R, so that this question does not keep coming up.