Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Miracle Flatness and Zariski's Main Theorem #4014

Open
adomani opened this issue Sep 1, 2020 · 0 comments
Open

Miracle Flatness and Zariski's Main Theorem #4014

adomani opened this issue Sep 1, 2020 · 0 comments
Labels
feature-request This issue is a feature request, either for mathematics, tactics, or CI

Comments

@adomani
Copy link
Collaborator

adomani commented Sep 1, 2020

Two useful results to have in mathlib are

  1. the Miracle Flatness Lemma,
  2. Zariski's Main Theorem.

Also, the Appendices of Bjorn Poonen's Rational points on varieties, especially Appendix C contain lots of relevant material on the web of implications among properties of morphisms.
@jcommelin jcommelin added the feature-request This issue is a feature request, either for mathematics, tactics, or CI label Sep 1, 2020
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
feature-request This issue is a feature request, either for mathematics, tactics, or CI
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jcommelin @adomani