feat(AlgebraicGeometry/Birational): add birational maps#40871
feat(AlgebraicGeometry/Birational): add birational maps#40871justus-springer wants to merge 43 commits into
Conversation
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Christian Merten <christian@merten.dev>
Co-authored-by: Christian Merten <christian@merten.dev>
…nalMap_composition
PR summary f19be84a35Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
| Current number | Change | Type (strong) |
|---|---|---|
| 7130 | 1 | backward.isDefEq.respectTransparency |
| 4158 | 2 | backward.isDefEq.respectTransparency.types |
Increase in weak tech debt: (relative, absolute) = (1.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 5011 | 1 | exposed public sections |
Current commit f19be84a35
Reference commit cd580e54f1
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).
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
| abbrev IsOver (S : Scheme.{u}) [X.Over S] [Y.Over S] (f : X.BirationalMap Y) : Prop := | ||
| f.hom.IsOver S |
There was a problem hiding this comment.
We are phasing out the Scheme.Over classes: Could you please instead use explicit structure maps (as you already did for Scheme.IsRationalOver).
| set_option backward.isDefEq.respectTransparency.types false in | ||
| lemma PartialIso.toPartialMap_comp_symm (f : X.PartialIso Y) : | ||
| f.toPartialMap.comp f.symm.toPartialMap = | ||
| (PartialMap.id X).restrict f.source f.dense_source le_top := by | ||
| ext1 |
There was a problem hiding this comment.
This could probably go in an earlier file?
|
|
||
| /-- A birational map between irreducible schemes `X` and `Y`. Consists of a pair of dominant | ||
| mutually inverse rational maps `hom : X ⤏ Y` and `inv : Y ⤏ X`. -/ | ||
| structure BirationalMap (X Y : Scheme.{u}) [IrreducibleSpace X] [IrreducibleSpace Y] where |
There was a problem hiding this comment.
Could you please add the relevant stacks tag? It would also be nice to provide some other references (e.g. EGA) and explain a bit how they differ. Could you please also relate this to Scheme.Birational? There could also be a predicate Scheme.RationalMap.Birational saying it is induced by a partial equiv.
An alternative definition, as far as I understand, would be to define an equivalence relation on PartialEquivs and say a birational map is a term of the quotient, this would work without assumptions on X and Y if I understand correctly. Did you consider this?
chrisflav
added
the
awaiting-author
2 participants
We add birational maps between irreducible schemes (dominant rational maps with an inverse). We provide a group structure on birational automorphisms and the subgroup of birational maps that are defined over a base. We also prove that partial isomorphisms give rise to birational maps (leaving the converse as future work).