Google Summer of Code GSoC

Stream: new members

[Leo Mayer]

Hi everyone! My name is Leo, and I'm a math PhD student at the University of Washington in Seattle. I've recently started learning about Lean (I started with the natural numbers game, then did the tutorial project, and am now working through Theorem Proving in Lean), and I want to keep learning about it and also contribute to mathlib. I am also wondering if Lean is going to represented as a mentoring organization for this year's Google Summer of Code, since I would be very interested if so.

[Kevin Buzzard]

What are your interests? There's tons of stuff to do and plenty of people to collaborate with

[Alex J. Best]

I don't know if anyone from Lean has thought seriously about applying for GSOC, it would be very cool of course, but I did read on the coq zulip I believe that they have tried before and been classified as too niche/specific, which is a shame.
Generally more niche projects have a better chance of success as part of a bigger organization (I did GSoC as a student working on the FLINT library for number theory which is also fairly specialist, but I believe they applied as part of an umbrella organization, Lmonade).
The recent changes to GSoC might make space for smaller/more specialist projects but that is not yet clear

[Leo Mayer]

Math-wise, I'm generally into algebra. Recently I've been learning about affine group schemes/hopf algebras, as well as homological algebra/category theory.
For lean I was thinking it would probably make more sense to work on the undergraduate curriculum project rather than trying to implement something more advanced, at least until I get more used to lean.

[Kevin Buzzard]

You should just make Hopf algebras, that would be a great way to start learning :-)

[Yaël Dillies]

I would actually be quite interested in seeing Hopf algebras formalized because explanations online are currently quite hermetic to me.

[Kyle Miller]

Do we have ways of manipulating co-algebraic expressions? (comultiplications & coactions). It seems like it's hard to symbolically prove things about Hopf algebras without Lean having some adeptness at something like Sweedler notation, though I imagine it could be doable using manipulations in monoidal categories, for string diagrammatic reasoning.

[Kevin Buzzard]

A hopf algebra is just an R-algebra A with a map A -> A tensor A satisfying some axioms. Why will this be hard?

[Kyle Miller]

One basic theorem is that the axioms imply that the antipode is an antihomomorphism, and the proof I know involves manipulating expressions that are in $A^{\otimes 6}$ (in the output of some composition of four comultiplications), as intermediate values for a bilinear map $A\otimes A\to A$, which seems somewhat unwieldy... That's used in the proof that if A is commutative or cocommutative then the antipode is an involution.

[Kyle Miller]

Hopf algebras have a duality symmetry where theorems about $A$ also apply to $A^*$, which has the multiplication and comultiplication with reversed roles, and it seems like it would be good to be sure to take advantage of that.

[Kevin Buzzard]

In algebraic geometry a Hopf algebra isn't assumed to be free over the base so there might not be a useful definition of $A^*$.

[Leo Mayer]

Cool I'll get started!
It sounds like there'll be a lot of inheritance happening? Like commutative Hopf algebras (then we get theory of affine gp schemes) or Hopf algebras over a field (then we get duality) both extending the base Hopf algebra?
Is there a reference/style guide for how to structure things in that scenario?
I'll probably have a lot of more basic questions before that question becomes pressing...

[Eric Wieser]

The docstring for docs#algebra (and the implementation notes above it) might be of interest to you