Zulip Chat Archive

Stream: maths

Topic: Difficulty of formalizing Hartshorne's exercises


view this post on Zulip Roman Bars (Mar 19 2021 at 09:30):

How difficult would it be to formalize the statements of the exercises in Hartshorne's textbook on algebraic geometry? What about the solutions?

view this post on Zulip Johan Commelin (Mar 19 2021 at 09:35):

Given the current state of the art, I think it would be very impressive to get past page 5.

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 09:36):

I skipped chapter 1 and started with chapter 2 when I thought about this, but the first exercise was about a constant sheaf and we don't have those in mathlib yet. On the other hand Imperial students did some of the exercises about sheaves (e.g. gluing) within the context of top spaces.

view this post on Zulip Kevin Buzzard (Mar 19 2021 at 09:37):

Hartshorne's definition of presheaf is wrong as well, which makes things worse. for him it's not a functor, there is some random extra axiom F(0)=bot.

view this post on Zulip Bhavik Mehta (Mar 19 2021 at 14:21):

Johan Commelin said:

Given the current state of the art, I think it would be very impressive to get past page 5.

I don't know Hartshorne at all well, but is there anything you think would make it easier to do this?

view this post on Zulip Johan Commelin (Mar 19 2021 at 14:28):

A more extensive commutative algebra library


Last updated: May 14 2021 at 19:21 UTC