Zulip Chat Archive
Stream: triage
Topic: issue #4014: Miracle Flatness and Zariski's Main Theorem
Random Issue Bot (Mar 20 2021 at 14:26):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Damiano Testa (Mar 22 2021 at 13:36):
I still believe that this is important, but also that it requires a lot of material about schemes (and commutative algebra!) to be really "imminent".
Kevin Buzzard (Mar 22 2021 at 13:51):
By the way I'm (very slowly) working on flatness -- I decided that it would be easier to develop the theory after we had Tor though, so I'm currently thinking about that. I'm completely happy with having this as a long-term issue, I think it's a fine goal, but of course we are a long way from having either of these things.
Damiano Testa (Mar 22 2021 at 14:21):
Kevin, thanks for working on flatness/tors!
I agree with you that this is a long-term project: I intended it more as a way of testing when a satisfactory level of scheme-theory had been developed, rather than an "easy goal that is within reach"!
Random Issue Bot (Mar 30 2021 at 14:23):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Damiano Testa (Mar 30 2021 at 14:31):
No further update, but the previous comments on this thread still apply!
Random Issue Bot (Nov 01 2021 at 14:19):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jul 31 2022 at 14:13):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Aug 25 2022 at 14:14):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Oct 30 2022 at 14:18):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Damiano Testa (Oct 30 2022 at 18:35):
Although the formalization of algebraic geometry is growing rapidly, this issue may be solved in Lean4... maybe! :smile:
Kevin Buzzard (Oct 30 2022 at 18:40):
@Damiano Testa do you have a coherent roadmap for proving these results? You give no references in the issue.
Damiano Testa (Oct 30 2022 at 18:41):
Ah, I'll add one once I'm at a computer. For Miracle Flatness it will likely be Matsumura.
Damiano Testa (Oct 30 2022 at 18:42):
For Zariski's main theorem, maybe the stacks project.
Damiano Testa (Oct 30 2022 at 18:43):
I see that I had linked the stacks project for both. I will have to go back and see if Matsumura is more accessible, though.
Damiano Testa (Oct 30 2022 at 18:44):
In any case, I had no coherent road map when I wrote this issue: it was still in the good old days when I thought that formalization was easier than proving results... :upside_down:
Kevin Buzzard (Oct 30 2022 at 18:45):
The proof of ZMT I know (or rather knew) uses sheaf cohomology, so it somehow feels a very long way away. IIRC Hartshorne argues that the cohomological proof is better than older proofs because it's cleaner. Do you have a feeling as to which of the no doubt many proofs will be easiest to formalise? All of these things would sit very well in the issue.
Kevin Buzzard (Oct 30 2022 at 18:45):
Yeah Hartshorne p276 "Zariski's first proof of the theorem was by an entirely different method which did not use cohomology"
Damiano Testa (Oct 30 2022 at 18:46):
Ok, I'll try to make the issue more focused. I will likely also remove the "catch all" reference to rational points.
Damiano Testa (Oct 30 2022 at 18:47):
I think that the proof via formal functions might be also a good one, but I really have to look at the various proofs with formalization in mind to have a better idea.
Kevin Buzzard (Oct 30 2022 at 18:47):
I know you're an algebraic geometer so I trust that you know which of the many goals in e.g. the stacks project are somehow "important", but I'm wondering whether we are getting to a point where we could do with a roadmap to get us to these goals.
Damiano Testa (Oct 30 2022 at 18:48):
Ok, I will try to isolate some "important" results. I am a little short on time these days, but it will get better by mid December.
Damiano Testa (Oct 30 2022 at 18:49):
Also, the current impetus in algebraic geometry in mathlib is via category theory: this is as far as I can possibly get, while still recognizing something as algebraic geometry!
Kevin Buzzard (Oct 30 2022 at 18:51):
Yes, I agree that it's time to reclaim algebraic geometry from the category guys!
Kevin Buzzard (Oct 30 2022 at 18:52):
I am giving 4 lectures on algebraic geometry in Lean in November, and I'm looking for topics. I'm going to do sheaves of modules for the first one (in the naive way, the way which everyone knows will work but everyone complains shouldn't be the way to do it because it will involve duplicating lemmas, an argument which never convinces me)
Damiano Testa (Oct 30 2022 at 18:53):
My suggestion of defining the functor of points in your other thread on AG received an answer from Adam that I still am not sure whether it was a joke or not... :man_facepalming:
Damiano Testa (Oct 30 2022 at 18:55):
About duplicating lemmas, I started out thinking the same as you: copy-paste is easy. But refactoring lemmas that are copy-pasted across the library is actually not too pleasant. So now I try harder to avoid copy pasting...
Random Issue Bot (Jan 01 2023 at 14:09):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Jan 15 2023 at 14:08):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Damiano Testa (Jan 15 2023 at 22:11):
I have not forgotten about this, I just did not have a chance to take the time to prepare a better roadmap!
Random Issue Bot (Feb 01 2023 at 14:08):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Feb 14 2023 at 14:09):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Random Issue Bot (Mar 12 2023 at 14:09):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Kevin Buzzard (Mar 12 2023 at 15:12):
@Jujian Zhang has recently made a lot of progress with flatness.
Random Issue Bot (Aug 27 2023 at 14:07):
Today I chose issue 4014 for discussion!
Miracle Flatness and Zariski's Main Theorem
Created by @damiano (@adomani) on 2020-09-01
Labels: feature-request
Is this issue still relevant? Any recent updates? Anyone making progress?
Last updated: Dec 20 2023 at 11:08 UTC