Zulip Chat Archive

Stream: new members

Topic: Google Summer of Code GSoC


Leo Mayer (Feb 17 2022 at 19:27):

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 (Feb 17 2022 at 21:33):

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

Alex J. Best (Feb 17 2022 at 21:52):

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 (Feb 18 2022 at 18:44):

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 (Feb 18 2022 at 19:10):

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

Yaël Dillies (Feb 18 2022 at 19:22):

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

Kyle Miller (Feb 18 2022 at 19:54):

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 (Feb 18 2022 at 21:40):

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 (Feb 18 2022 at 21:55):

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 A6A^{\otimes 6} (in the output of some composition of four comultiplications), as intermediate values for a bilinear map AAAA\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 (Feb 18 2022 at 21:57):

Hopf algebras have a duality symmetry where theorems about AA also apply to AA^*, 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 (Feb 18 2022 at 23:37):

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

Leo Mayer (Feb 19 2022 at 00:26):

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 (Feb 19 2022 at 01:15):

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


Last updated: Dec 20 2023 at 11:08 UTC