Equivalence between Hopf algebras and affine group schemes

Stream: toric

[Yaël Dillies]

@Michał Mrugała, @Andrew Yang, I have just rebased hopfToGrp on top of master

[Yaël Dillies]

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]

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]

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]

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]

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]

It's a consequence of the first item in current tasks :)

[Sophie Morel]

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]

It's hidden in here: https://github.com/YaelDillies/Toric/blob/master/Toric/GroupScheme/HopfAffine.lean#L67 :wink:

[Michał Mrugała]

This should follow from

def commAlgEquivUnder (R : CommRingCat) : CommAlg R ≌ Under R

and some categorical nonsense
Yaël's response is better.

[Sophie Morel]

I don't think Yaël's response actually answers my question, but yours does!

[Yaël Dillies]

To be explicit, the equivalence is (commAlgEquivUnder R).op.trans (Over.opEquivOpUnder R).symm

[Sophie Morel]

Yes, I was editing my message to say that I just saw it. :man_facepalming:

[Michał Mrugała]

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]

yaeldillies.github.io/Toric/docs, for future reference

[Yaël Dillies]

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]

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]

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]

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]

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.