Zulip Chat Archive

Stream: new members

Topic: Projective geometry


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 20:14):

no

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 20:14):

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

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 20:14):

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

view this post on Zulip pyon (Oct 26 2019 at 20:15):

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

view this post on Zulip 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.

view this post on Zulip pyon (Oct 26 2019 at 20:21):

How much ring and field theory is already available?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip pyon (Oct 26 2019 at 20:23):

Oh, okay.

view this post on Zulip 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. :-)

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Oct 26 2019 at 20:25):

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

view this post on Zulip pyon (Oct 26 2019 at 20:25):

I see, thanks.

view this post on Zulip Lennard Henze (Oct 28 2019 at 10:18):

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


Last updated: May 16 2021 at 05:21 UTC