[Merged by Bors] - feat(AlgebraicGeometry/Birational): Birationality and rationality of schemes#39122
Conversation
PR summary 8367f1548cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (strong) |
|---|---|---|
| 4510 | 6 | backward.defeqAttrib.useBackward |
Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 4967 | 1 | exposed public sections |
Current commit 8367f1548c
Reference commit 008653f6c0
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
github-actions
Bot
added
the
file-removed
766c496 to
1c89905
Compare
justus-springer
changed the title
chrisflav
left a comment
chrisflav
left a comment
There was a problem hiding this comment.
Thanks for working on this! Looking forward to a lot more birational geometry in mathlib! Some initial comments, I have not looked at the rest of the code closely yet because it depends on these comments.
chrisflav
added
the
awaiting-author
erdOne
left a comment
erdOne
left a comment
There was a problem hiding this comment.
Not a detailed review but some design questions worth thinking about (even if not addressed in this PR)
- Should you be working with
PartialMaporRationalMap? In particular isext_iffright? Or do you only want equality on a dense subset? - Do we still want to work with
OverClass(I hate it now and I presume @chrisflav agrees)? - How will this mesh with "birational morphisms"? Do we want an
IsBirationalpredicate on rational maps also? (and thenIsBirational f.toRationalMap) - How far are we from rational <=> function field is rational? I would hope we can do this in this very PR or a follow up?
|
Thank you both for the comments! @erdOne, here are my thoughts to your points.
Edit: I replaced uses of
|
justus-springer
removed
the
awaiting-author
mathlib-dependent-issues
Bot
added
blocked-by-other-PR
|
This PR/issue depends on: |
GitHub Actions
Inactive
|
Thanks! |
|
🚀 Pull request has been placed on the maintainer queue by chrisflav. |
mathlib-triage
Bot
added
the
maintainer-merge
|
Could you merge again with master as there were some disrupting changes recently? |
joelriou
added
the
awaiting-author
justus-springer
added
awaiting-CI
github-actions
Bot
removed
the
awaiting-CI
justus-springer
added
the
awaiting-CI
github-actions
Bot
removed
the
awaiting-CI
|
@joelriou I merged master again today, no changes were necessary. Do you think this is mergeable soon? |
joelriou
added
the
awaiting-author
justus-springer
added
awaiting-CI
github-actions
Bot
removed
the
awaiting-CI
|
Thanks! bors merge |
mathlib-triage
Bot
removed
the
maintainer-merge
…schemes (#39122) This is a first step (of hopefully many) towards some basic birational geometry. This PR adds `Birational/Birational.lean`, which defines predicates `Birational`, `BirationalOver` and `IsRationalOver` for arbitrary schemes and provides basic API (e.g. that they are equivalence relations, and that affine space is rational). Some notes on the choice of definitions: There are multiple ways to define what it means for two schemes to be birational to each other. A common one is: "There exists a rational map with a rational inverse". However, this would require defining composition of rational maps, which is not always defined (In order to compose `f : X ⤏ Y` with `g : Y ⤏ Z`, you need at least `X` preirreducible, `Y` nonempty and `f` dominant). On the other hand, I can define "There exist dense subsets `U : Opens X` and `V : Opens Y` such that `U ≅ V` as schemes" for any two schemes `X` and `Y`, with no conditions. Hence I chose that as a definition. I'm also working on defining composition of rational maps (#39445), and once that's done, there should be a theorem connecting the two definitions. - [x] depends on: #39316 Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
mathlib-bors
Bot
added
the
bors-staging
|
Pull request successfully merged into master. Build succeeded: |
mathlib-bors
Bot
changed the title
4 participants
This is a first step (of hopefully many) towards some basic birational geometry. This PR adds
Birational/Birational.lean, which defines predicatesBirational,BirationalOverandIsRationalOverfor arbitrary schemes and provides basic API (e.g. that they are equivalence relations, and that affine space is rational).Some notes on the choice of definitions: There are multiple ways to define what it means for
two schemes to be birational to each other. A common one is: "There exists a
rational map with a rational inverse". However, this would require defining composition of
rational maps, which is not always defined (In order to compose
f : X ⤏ Ywithg : Y ⤏ Z, youneed at least
Xpreirreducible,Ynonempty andfdominant). On the other hand, I can define"There exist dense subsets
U : Opens XandV : Opens Ysuch thatU ≅ Vas schemes" forany two schemes
XandY, with no conditions. Hence I chose that as a definition. I'm alsoworking on defining composition of rational maps (#39445), and once that's done, there should be a theorem
connecting the two definitions.