Coalgebras/bialgebras/Hopf algebras

Stream: maths

[Amelia Livingston]

Does anyone have any thoughts on how these objects should be set up? I've tried several configurations for coalgebras and bialgebras and there's always something a little ugly. I've settled on making them classes and I'm keen to get bialgebra to extend coalgebra, for no reason other than personal taste. I'm just messing around with this stuff; I want to mention them in a talk on Thursday.

[Johan Commelin]

I can imagine it quickly gets ugly. On paper we very quickly suggest to a very suggestive notation.

[Johan Commelin]

https://en.wikipedia.org/wiki/Coalgebra#Sweedler_notation

[Johan Commelin]

But this seems very hard to mimic in Lean.

[Kalle Kytölä]

Sweedler's notation is indeed very useful, and looks scary for formalization.

But is that absolutely horrible to mimick in Lean? Sweedler's notation of course amounts to choosing non-canonical expressions for the coproducts of all elements (indexed collections of $a_{(1)}$'s and $a_{(2)}$'s for every $a$), but maybe even choice can do that. Lemmas are true for the appropriate sums of such non-canonical choices, so that doesn't look too bad as such. And one certainly wants separate non-canonical representations for iterated coproducts, but still one can set up lemmas to translate between these. (In the worst case one will then have to juggle such coassociativity lemmas just like one would do with associativity lemmas without ring, which would indeed be bad. Do we need a coring tactic?)

I of course haven't tried, but I'm optimistically hoping that it looks even scarier than it ends up being. :big_smile:

[Johan Commelin]

Maybe you can get quite far with appropriate induction lemmas? But it would need some engineering to get a usable system, I guess.

[Kalle Kytölä]

I also expect that a lot of engineering would be needed.

Probably one anyway wants to avoid working with elements as much as possible (and therefore avoid Sweedler notation as much as possible). (Sure, at times Sweedler's notation might really be the easiest way, but other times it is just used out of habit.) So in parallel to engineering Sweedler's notation, maybe this area would also benefit from engineering for good ways to compose multilinear maps in flexibly specified (diagrammatic?) ways?

[Junyan Xu]

@Vasily Ilin tried to construct the Hopf algebra structure on K[X] last April-May, but seemed to give up (due to timeouts/slowness?) and apparently then switched to defining affine group schemes using representable functors. Not sure what lessons came out of it ... here are some relevant threads:

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20structure.20vs.20class/near/282163086
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/refactoring.20proofs
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/get.20the.20two.20maps.20from.20an.20isomorphism

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20algebra.20maps.20takes.201.20to.201
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20.60calc.60.20block
https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/deterministic.20timeout.20on.20definition.20of.20structure

[Vasily Ilin]

https://github.com/leomayer1/Hopf/tree/master/src
Here is the repo with our attempt!

[Junyan Xu]

Oh nice! You did finish checking K[X]'s Hopf algebra structure without sorries.

[Kevin Buzzard]

@Amelia Livingston what did you not like about that approach? Like sheaves of modules I can quite believe that each approach has advantages and disadvantages.

[Amelia Livingston]

I had just seen Scott Morrison's comment that coalgebras and bialgebras should be defined first so was having a go at that. But I hadn't read all of these threads so thank you! And I've been using the functor definition too - wanted to compare them and show they're equivalent

I've had a little go at using Sweedler notation because I think it might improve organisation in my coalgebra/bialgebra stuff, but I haven't finished setting it up.

[Amelia Livingston]

FWIW Vasily if you do want to PR your work, I'm not looking to PR mine - just wanted to roll my own (for a talk I'm now too ill to give) and so I know what's going on, and then use it for more specific things, which I maybe would PR.

[Kevin Buzzard]

I would like to see group schemes in mathlib because they're a huge source of very nice results and you don't need any of the theory of varieties to set them up

[Amelia Livingston]

I think Joël Riou has some cool work on internal objects in categories here I was hoping might get PR'ed someday, as explained here

[Pedro Sánchez Terraf]

Amelia Livingston said:

I had just seen Scott Morrison's comment that coalgebras and bialgebras should be defined first so was having a go at that.

One (most probably superfluous) remark: There's a bunch of "general coalgebra" stuff (as in "general/universal algebra") in CS, so I understand the classical coalgebra will be under some appropriate namespace.

[Eric Wieser]

I doubt that will be the case; coalgebra would probably end up in the root namespace like algebra is.

[Eric Wieser]

Thanks to @Ali Ramsey, we now have docs#Coalgebra !

[Kevin Buzzard]

So bialgebras next and then Hopf algebras?

[Yaël Dillies]

Is it really called "conunitality" in the literature?

[Johan Commelin]

That must be a typo

[Kyle Miller]

fixed the typo: #8874

[Eric Wieser]

It looks like you based it on the version that the docs were built from and not master, and picked up a merge conflict as a result.

[Kyle Miller]

Oops. I tried doing this quickly by using the github interface rather than pulling mathlib locally...