Group algebras

Stream: toric

[Yaël Dillies]

In Toric.Hopf.MonoidAlgebra, we are currently using docs#MonoidAlgebra. Shouldn't we rather be using docs#AddMonoidAlgebra since our groups in the end are additive?

[Yaël Dillies]

I also know MonoidAlgebra and AddMonoidAlgebra don't have the same Hopf structure. Which one do we want?

[Paul Lezeau]

I think docs#AddMonoidAlgebra would be quite reasonable - if only for the nice R[M] notation

[Paul Lezeau]

Yaël Dillies said:

I also know MonoidAlgebra and AddMonoidAlgebradon't have the same Hopf structure. Which one do we want?

Not sure about this though!

[Yaël Dillies]

I've just duplicated all declarations and called it a day

[Sophie Morel]

Speaking of group algebras, it seems that the first thing I have fill out is the sorry on line 19 of the file Toric.GroupScheme.Diagonalizable, i.e. the fact that Spec of a group algebra is a group scheme (over the base ring). It seems natural to prove more generally that Spec of a R-Hopf algebra is a group scheme over Spec R, is this done yet? I could not find anything but did not want to assume.

[Sophie Morel]

Last time we looked at this problem (with Amelia) was in May 2024, and some needed results about Hopf algebras were not available.

[Yaël Dillies]

Yes it is. This is part of the correspondence between Hopf algebras and group schemes that we've just completed.

[Yaël Dillies]

You want to use hopfSpec in Toric.GroupScheme.HopfAffine

[Sophie Morel]

Yoohoo!

[Yaël Dillies]

Actually, that sorry on L. 19 of Toric.GroupScheme.Diagonalizable seems completely out of date! You should be able to just remove it, by importing some other Toric files

[Sophie Morel]

I'll try that, as soon as my vscode is done compiling some files.

[Sophie Morel]

Yup, we're good, the definition of diagonalizable groups now compiles! Now I just need to actually prove stuff about them (= the easy part :grinning_face_with_smiling_eyes: ).

[Sophie Morel]

I created a branch but I don't have push permission to your repository. Should I create a fork?

[Michał Mrugała]

@Yaël Dillies could you give Sophie perms?

[Yaël Dillies]

Whoops, yes, what is your GitHub handle? (and please add it to your Zulip profile!)

[Sophie Morel]

Added! (It's smorel394.)

[Yaël Dillies]

Voilà : https://github.com/YaelDillies/Toric/invitations

[Sophie Morel]

I pushed to master!? I'm so sorry, I was sure I had switched branches! I'll do that now.

[Yaël Dillies]

:scream: Don't worry, it's fine. You certainly wouldn't catch me breaking the build by hastily pushing to master... right? :sweat:

[Yaël Dillies]

Btw hopfSpec is composed with the group algebra functor in specCommGrpAlgebra. You can use this functor directly if you want

[Yaël Dillies]

Maybe IsDiagonalisable should be made an abbrev of specCommGrpAlgebra.essImage, actually?

[Sophie Morel]

Well, there's the "finitely generated" condition on the commutative group.

[Yaël Dillies]

Ah right, of course. But the idea is the same: we could define it as the essential image of an appropriate functor. Probably this will save us some boilerplate down the line

[Sophie Morel]

Sorry, all productive work interrupted, I'm trying to convince git that I do NOT want to push to master every time...

[Kevin Buzzard]

With FLT I just make everyone PR from forks. Why not do that here?

[Michał Mrugała]

Is there an advantage to PRing from forks instead of using branches?

[Yaël Dillies]

I can always set a branch protection rule on master. I just haven't yet found the need to do so

[Edward van de Meent]

don't these events clearly indicate a need?

[Yaël Dillies]

Well, nothing broke, so :shrug: