Zulip Chat Archive
Stream: toric
Topic: Equivalence between Hopf algebras and affine group schemes
Yaël Dillies (Mar 26 2025 at 09:15):
@Michał Mrugała, @Andrew Yang, I have just rebased hopfToGrp
on top of master
Yaël Dillies (Apr 03 2025 at 18:35):
I believe the correspondence between Hopf algebras and affine group schemes is now fully stated and almost entirely proved. This would be the first milestone of our project :tada:
Yaël Dillies (Apr 04 2025 at 18:51):
And now we have plugged in the (substantially easier) full faithfulness of G ↦ k[G]
, so we can finally compute maps Spec k[G] ⟶ Spec k[H]
. This unlocks many items in the blueprint: Computation of characters/cocharacters of the torus, subgroup of a torus, image of a torus...
Michał Mrugała (Apr 04 2025 at 22:58):
Putting this here for accountability: since this unlocks a lot of the project I'll do some work on improving the blueprint for section 1.1 to make it easier for people to contribute. This is an exciting point in the project because on the scheme side we finally have the language to properly talk about these varieties!
Sophie Morel (Apr 05 2025 at 10:37):
Accountability too: I am finally done with hiring committees so I can start doing math again, so I'll get working on diagonalizable groups.
Sophie Morel (Apr 05 2025 at 17:22):
Are you planning to show that the global sections functor is a right adjoint to the algSpec
functor from (CommAlg R)ᵒᵖ
to Over (Spec R)
? For now I cannot find a constructor of a global sections functors Over (Spec R) ⥤ (CommAlg R)ᵒᵖ
but maybe I missed it. The fact that it is a right adjoint would give that it commutes with limits, and so sends group objects to group objects, and so the fact that it sends a group scheme over Spec R
to a R
-Hopf algebra would follow.
Michał Mrugała (Apr 05 2025 at 17:36):
It's a consequence of the first item in current tasks :)
Sophie Morel (Apr 05 2025 at 19:00):
Do you also need an equivalence between (CommAlg R)ᵒᵖ
and Over (op (CommRing.of R))
? If I understand the first item correctly, it's a purely categorical result.
Yaël Dillies (Apr 05 2025 at 19:03):
It's hidden in here: https://github.com/YaelDillies/Toric/blob/master/Toric/GroupScheme/HopfAffine.lean#L67 :wink:
Michał Mrugała (Apr 05 2025 at 19:03):
This should follow from
def commAlgEquivUnder (R : CommRingCat) : CommAlg R ≌ Under R
and some categorical nonsense
Yaël's response is better.
Sophie Morel (Apr 05 2025 at 19:05):
I don't think Yaël's response actually answers my question, but yours does!
Yaël Dillies (Apr 05 2025 at 19:06):
To be explicit, the equivalence is (commAlgEquivUnder R).op.trans (Over.opEquivOpUnder R).symm
Sophie Morel (Apr 05 2025 at 19:07):
Yes, I was editing my message to say that I just saw it. :man_facepalming:
Michał Mrugała (Apr 05 2025 at 21:19):
Btw, we have internal API docs for this project on the project website. It might make looking for some results a bit easier!
Yaël Dillies (Apr 05 2025 at 21:21):
yaeldillies.github.io/Toric/docs, for future reference
Yaël Dillies (Apr 18 2025 at 21:18):
Here are the other two past works on the correspondence between Hopf algebras and affine group schemes that I could find:
- #maths > Coalgebras/bialgebras/Hopf algebras
- https://github.com/ImperialCollegeLondon/FLT/compare/main...CrazyAffine, and the corresponding paper: https://link.springer.com/chapter/10.1007/978-3-031-64529-7_9
Yaël Dillies (Apr 24 2025 at 18:05):
Working on cleaning the correspondence up, I noticed that our current Hopf.HopfAlg
file could be rephrased nicely as setting up the category CommHopfAlg
of commutative Hopf algebras and showing it's equivalent to that of cogroup algebras.
Yaël Dillies (Apr 24 2025 at 18:08):
I've just opened YaelDillies/toric#21 to realise this vision. There are two new categories CommBialg R
and CommHopfAlg R
, defined as the categories of commutative R
-bialgebras and commutative R
-Hopf algebras respectively, and we show they are equivalent to (Mon_ (CommAlg R)ᵒᵖ)ᵒᵖ
and (Grp_ (CommAlg R)ᵒᵖ)ᵒᵖ
respectively.
Yaël Dillies (Apr 24 2025 at 18:11):
The proofs are literal copy-pastes from the ones that Michal wrote in Hopf.HopfAlg
. Unfortunately, performance is poor, and not all the existing Hopf.HopfAlg
proofs compile in their new location.
Yaël Dillies (Apr 24 2025 at 18:11):
However, said proofs are precisely the ones that should be made one-liners after the CartesianMonoidalCategory
refactor is done. So I suggest we work on that now.
Last updated: May 02 2025 at 03:31 UTC