Zulip Chat Archive

Stream: new members

Topic: Projective geometry

pyon (Oct 26 2019 at 20:14):

Is there any formalization of classical algebraic geometry in Lean? I'm mostly interested in projective geometry, at the level of what's covered in chapter I of Hartshorne, especially theorem I.7.7, about the intersection of a projective variety and a hypersurface not containing it.

If there is nothing like this, how much effort would it take to implement it, given what is already available? I'm reasonably familiar with typed functional languages (ML, Haskell), but dependently typed ones not so much. Thanks in advance.

Kevin Buzzard (Oct 26 2019 at 20:14):

no

Kevin Buzzard (Oct 26 2019 at 20:14):

which is a pain because I am teaching such a course next term.

Kevin Buzzard (Oct 26 2019 at 20:14):

so I'm going to have to write it myself. Want to help?

pyon (Oct 26 2019 at 20:15):

If you don't mind my potential slowness in learning the system, sure!

Kevin Buzzard (Oct 26 2019 at 20:20):

It will be a difficult task, but it is true that I will attempt to do it. Quite how far I will get I have no clue.

pyon (Oct 26 2019 at 20:21):

How much ring and field theory is already available?

Kevin Buzzard (Oct 26 2019 at 20:21):

Noetherian rings we have, basic stuff, I don't think anyone has done the Nullstellensatz yet, @Lennard Henze is working on Noether normalisation, we have Hilbert basis theorem

Kevin Buzzard (Oct 26 2019 at 20:23):

I just finished with this term's course yesterday so I was going to turn to this soon, but I need to tidy up my huge backlog of unread emails first.

pyon (Oct 26 2019 at 20:23):

Oh, okay.

pyon (Oct 26 2019 at 20:24):

I guess the positive side of the situation you describe is that, at least, I don't have to learn new mathematics to start contributing. I'm installing Lean right now. :-)

Kevin Buzzard (Oct 26 2019 at 20:24):

FYI here's the course outline from last year:

Course outline.
(1) Affine varieties – definition, examples, maps between varieties, translating
between geometry and commutative algebra (the Nullstellensatz)
(2) Projective varieties – definition, examples, maps between varieties, rigidity
and images of maps
(3) Dimension – several different definitions (all equivalent, but useful for
different purposes), calculating dimensions of examples
(4) Smoothness and singularities – definition, examples, key theorems
(5) Examples of varieties (depending on how much time is left)
What is not in the course?
(1) Schemes
(2) Sheaves and cohomology
(3) Curves, divisors and the Riemann–Roch theorem

Kevin Buzzard (Oct 26 2019 at 20:25):

I think we're always over an alg closed field.

pyon (Oct 26 2019 at 20:25):

I see, thanks.

Lennard Henze (Oct 28 2019 at 10:18):

when I'm done with Noether normalisation I want to turn to Nullstellensatz

Last updated: Dec 20 2023 at 11:08 UTC