Learning algebraic geometry; how can I contribute?

Stream: new members

[Soham Chowdhury]

Hi everyone! A friend sent me a link to @Kevin Buzzard's answer on the "What are perfectoid spaces?" MO question, which is how I got here. I'm learning algebraic geometry right now. More to the point, I have some experience using Agda and Idris (but not Lean).

I would enjoy helping to formalise material related to what I'm learning; how can I help?

[Kevin Buzzard]

Well, someone needs to prove that the integral closure of a subring is a subring :-)

[Kenny Lau]

what the hell, @Soham Chowdhury

[Kevin Buzzard]

Here are some projects which the community thinks are accessible: https://github.com/leanprover-community/mathlib/wiki/Potential-projects

[Soham Chowdhury]

@Kenny Lau is it ... possible I know you?

[Kenny Lau]

guess who sent you that link

[Soham Chowdhury]

Oh haha

Well, someone needs to prove that the integral closure of a subring is a subring :-)

That sounds like something I can do!

[Kevin Buzzard]

Here is a challenging project which would teach you a bunch about Lean: prove that Hom(X,Spec(R)) = Hom(R,O_X(X)).

[Kenny Lau]

Here is a challenging project which would teach you a bunch about Lean: prove that Hom(X,Spec(R)) = Hom(R,O_X(X)).

yeah, that...

[Kevin Buzzard]

Anthony Bordg also sent me an email saying he might be interested in doing this. As I'm sure you'll know from Idris, there's a big difference between learning alg geom from a book and actually telling Lean about it.

[Kevin Buzzard]

What exactly are you learning?

[Soham Chowdhury]

Chapter 5 of Vakil's FOAG right now, so I don't know all that much :)

[Soham Chowdhury]

But basic commutative algebra sounds like something I could get started on.

[Kevin Buzzard]

Several people have been asking what they could work on. Of course embarking on a project like proving a standard algebra theorem with a new theorem prover (and then asking a gazillion questions here) is a really good way to learn how to use the theorem prover, but I am currently slightly worried that whenever someone who knows any algebra asks what they could do, I reply with basically the same reply.

[Kevin Buzzard]

As far as comm alg goes, we have localisation of rings, a PR for tensor products, a definition of Noetherian rings and modules but 0 theorems (other than the fact that the two usual definitions are equivalent), and enough group theory to make doing basic commutative algebra feasible.

[Soham Chowdhury]

I guess even if someone "beats me to" one of these problems, I'm sure the payoff from becoming comfortable with Lean will make it that much easier to work on harder things like, e.g. the Hom(X, Spec R) theorem you mentioned.

[Kevin Buzzard]

Lean has affine schemes but not projective schemes, so you're a little ahead ;-)

[Kevin Buzzard]

However they're not in mathlib, they're in a stacks project repo on my github https://github.com/kbuzzard/lean-stacks-project which I wrote to learn Lean, so this code sometimes leaves some things to be desired...

[Soham Chowdhury]

Is the definition of Noetherian modules in mathlib master? I can't seem to find it there.

[Kevin Buzzard]

I watched it be born but I don't know where it is. It was only created on Wednesday.

[Mario Carneiro]

it is in a branch on the community fork

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/search?q=noetherian&unscoped_q=noetherian doesn't find it

[Kevin Buzzard]

https://github.com/leanprover-community/mathlib/commit/ef5c110626b0197118299071a98ed98e1aead287

[Soham Chowdhury]

I believe GitHub search only looks in master.

[Kevin Buzzard]

I believe that too, now. We next need that submodules and quotient modules of Noetherian modules are Noetherian. This should be easy if we have some basic facts about there being a natural injection from the submodules of M/N to the submodules of M -- is this in mathlib? @Kenny Lau Is this something like Proposition 1.1 of A-M?

[Kevin Buzzard]

oh, that's only for rings. OK so here's a concrete thing we need: order-preserving bijection between submodules of M/N and submodules of M containing N.

[Kevin Buzzard]

Is that there already? Does anyone know? I don't remember seeing it.

[Kenny Lau]

looks like a Galois correspondence to me

[Soham Chowdhury]

I'm going to check back here if (rather, when) I have questions. Thanks for the pointers.

[Patrick Massot]

@Soham Chowdhury do you know where to start? (hint: the answer is https://leanprover.github.io/theorem_proving_in_lean/).

[Johan Commelin]

Also see this thread in Zulip: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/subject/noetherian.20modules (You might need to enable the "maths" stream somewhere in your settings; but I thought this was done by default nowadays.)