Skip to content

Commit 46c7419

Browse files
justus-springerpre-commit-ci-lite[bot]
justus-springer
and
pre-commit-ci-lite[bot]
committed
feat(AlgebraicGeometry/Birational): Birationality and rationality of schemes (leanprover-community#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 (leanprover-community#39445), and once that's done, there should be a theorem connecting the two definitions. - [x] depends on: leanprover-community#39316 Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
1 parent 2899f15 commit 46c7419

3 files changed

Lines changed: 295 additions & 0 deletions

File tree

‎Mathlib.lean‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1349,6 +1349,7 @@ public import Mathlib.AlgebraicGeometry.AffineTransitionLimit
13491349
public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
13501350
public import Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
13511351
public import Mathlib.AlgebraicGeometry.Artinian
1352+
public import Mathlib.AlgebraicGeometry.Birational.Birational
13521353
public import Mathlib.AlgebraicGeometry.Birational.Dominant
13531354
public import Mathlib.AlgebraicGeometry.Birational.RationalMap
13541355
public import Mathlib.AlgebraicGeometry.ColimitsOver

‎Mathlib/AlgebraicGeometry/Birational/Birational.lean‎

Lines changed: 292 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,292 @@
1+
/-
2+
Copyright (c) 2026 Justus Springer. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Justus Springer
5+
-/
6+
module
7+
8+
public import Mathlib.AlgebraicGeometry.AffineSpace
9+
public import Mathlib.AlgebraicGeometry.Birational.RationalMap
10+
11+
/-!
12+
# Birationality and Rationality of schemes.
13+
14+
This file defines partial isomorphisms between schemes and uses them to formalize
15+
birationality and rationality.
16+
17+
## Main definitions
18+
19+
- `Scheme.PartialIso X Y`: an isomorphism between a dense open subscheme of `X` and a
20+
dense open subscheme of `Y`.
21+
- `Scheme.Birational X Y`: `X` and `Y` are birational, i.e. there exists a `PartialIso X Y`.
22+
- `Scheme.BirationalOver sX sY`: `X` and `Y` are birational over `S` via structure maps
23+
`sX : X ⟶ S` and `sY : Y ⟶ S`.
24+
- `Scheme.IsRationalOver sX`: `X` is rational over `S` via structure map `sX : X ⟶ S`,
25+
i.e. birational over `S` to some affine space `𝔸(n; S)`.
26+
27+
-/
28+
29+
@[expose] public section
30+
31+
universe u
32+
33+
open CategoryTheory
34+
35+
namespace AlgebraicGeometry.Scheme
36+
37+
/-- A partial isomorphism from `X` to `Y` is an isomorphism between dense open subschemes
38+
of `X` and `Y`. -/
39+
structure PartialIso (X Y : Scheme.{u}) where
40+
/-- The source open subscheme of a partial isomorphism. -/
41+
source : X.Opens
42+
dense_source : Dense (source : Set X)
43+
/-- The target open subscheme of a partial isomorphism. -/
44+
target : Y.Opens
45+
dense_target : Dense (target : Set Y)
46+
/-- The underlying isomorphism of a partial isomorphism. -/
47+
iso : source.toScheme ≅ target.toScheme
48+
49+
namespace PartialIso
50+
51+
variable {X Y Z S : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
52+
53+
variable (sX sY) in
54+
/-- A partial iso is an `S`-map if the underlying morphism is. -/
55+
abbrev IsOver (f : X.PartialIso Y) : Prop :=
56+
f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX
57+
58+
lemma ext_iff (f g : X.PartialIso Y) :
59+
f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target),
60+
f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e' := by
61+
constructor
62+
· rintro rfl
63+
simp
64+
· obtain ⟨U₁, hU₁, U₂, hU₂, f⟩ := f
65+
obtain ⟨V₁, hV₁, V₂, hU₂, g⟩ := g
66+
simp only [forall_exists_index]
67+
rintro rfl rfl e
68+
simpa using e
69+
70+
@[ext]
71+
lemma ext (f g : X.PartialIso Y) (e : f.source = g.source) (e' : g.target = f.target)
72+
(H : f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e') : f = g := by
73+
rw [ext_iff]
74+
exact ⟨e, e', H⟩
75+
76+
variable (X) in
77+
/-- The identity partial isomorphism on `X`, defined on all of `X`. -/
78+
@[refl, simps]
79+
def refl : X.PartialIso X where
80+
source := ⊤
81+
dense_source := dense_univ
82+
target := ⊤
83+
dense_target := dense_univ
84+
iso := Iso.refl _
85+
86+
/-- The inverse of a partial isomorphism. -/
87+
@[symm, simps]
88+
def symm (f : X.PartialIso Y) : Y.PartialIso X where
89+
source := f.target
90+
dense_source := f.dense_target
91+
target := f.source
92+
dense_target := f.dense_source
93+
iso := f.iso.symm
94+
95+
set_option backward.defeqAttrib.useBackward true in
96+
lemma IsOver.symm {f : X.PartialIso Y} (hf : f.IsOver sX sY) : f.symm.IsOver sY sX := by
97+
simpa [IsOver, ← cancel_epi f.iso.hom] using Eq.symm hf
98+
99+
/-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
100+
of `g`. See `trans` for the version that does not require this. -/
101+
@[simps]
102+
noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source) :
103+
X.PartialIso Z where
104+
source := f.source
105+
dense_source := f.dense_source
106+
target := g.target
107+
dense_target := g.dense_target
108+
iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
109+
110+
set_option backward.defeqAttrib.useBackward true in
111+
lemma IsOver.trans' {f : X.PartialIso Y} {g : Y.PartialIso Z} {e : f.target = g.source}
112+
(hf : f.IsOver sX sY) (hg : g.IsOver sY sZ) : (trans' f g e).IsOver sX sZ := by
113+
simp [IsOver, ← hf, hg]
114+
115+
/-- Restrict the source of a partial isomorphism to a smaller dense open. -/
116+
@[simps]
117+
noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense (U : Set X))
118+
(hU' : U ≤ f.source) : X.PartialIso Y where
119+
source := U
120+
dense_source := hU
121+
target := f.target.ι ''ᵁ f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U
122+
dense_target :=
123+
have := Opens.isDominant_ι f.dense_target
124+
f.target.ι.denseRange.dense_image f.target.ι.continuous <|
125+
f.iso.hom.denseRange.dense_image f.iso.hom.continuous <|
126+
hU.preimage f.source.ι.isOpenEmbedding.isOpenMap
127+
iso := (Opens.isoOfLE hU').symm ≪≫
128+
(f.iso.hom.isoImage (f.source.ι ⁻¹ᵁ U)) ≪≫
129+
(f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
130+
131+
set_option backward.defeqAttrib.useBackward true in
132+
lemma IsOver.restrictSource {f : X.PartialIso Y} (hf : f.IsOver sX sY) (U : Opens X)
133+
(hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
134+
(f.restrictSource U hU hU').IsOver sX sY := by
135+
simp [IsOver, hf]
136+
137+
/-- Restrict the target of a partial isomorphism to a smaller dense open. -/
138+
@[simps! source target iso]
139+
noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense (U : Set Y))
140+
(hU' : U ≤ f.target) : X.PartialIso Y :=
141+
(f.symm.restrictSource U hU hU').symm
142+
143+
lemma IsOver.restrictTarget {f : X.PartialIso Y} (hf : f.IsOver sX sY) (U : Opens Y)
144+
(hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
145+
(f.restrictTarget U hU hU').IsOver sX sY :=
146+
(hf.symm.restrictSource U hU hU').symm
147+
148+
/-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
149+
@[trans, simps! source target iso]
150+
noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso Z :=
151+
have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
152+
(f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl
153+
154+
lemma IsOver.trans {f : X.PartialIso Y} {g : Y.PartialIso Z} (hf : f.IsOver sX sY)
155+
(hg : g.IsOver sY sZ) : (f.trans g).IsOver sX sZ :=
156+
(hf.restrictTarget _ _ _).trans' (hg.restrictSource _ _ _)
157+
158+
/-- The underlying partial map of a partial isomorphism. -/
159+
@[simps]
160+
def toPartialMap (f : X.PartialIso Y) : X.PartialMap Y where
161+
domain := f.source
162+
dense_domain := f.dense_source
163+
hom := f.iso.hom ≫ f.target.ι
164+
165+
/-- The underlying rational map of a partial isomorphism. -/
166+
abbrev toRationalMap (f : X.PartialIso Y) : X ⤏ Y := f.toPartialMap.toRationalMap
167+
168+
/-- A scheme isomorphism viewed as a partial isomorphism defined on all of `X` and `Y`. -/
169+
@[simps]
170+
noncomputable def ofIso (f : X ≅ Y) : X.PartialIso Y where
171+
source := ⊤
172+
dense_source := dense_univ
173+
target := ⊤
174+
dense_target := dense_univ
175+
iso := X.topIso ≪≫ f ≪≫ Y.topIso.symm
176+
177+
end PartialIso
178+
179+
/-- `X` and `Y` are birational if there exists a partial isomorphism between them. -/
180+
@[stacks 0A20 "(1)"]
181+
def Birational (X Y : Scheme.{u}) : Prop := Nonempty (PartialIso X Y)
182+
183+
/-- Choose a partial isomorphism witnessing that `X` and `Y` are birational. -/
184+
noncomputable def Birational.partialIso {X Y : Scheme.{u}} (h : Birational X Y) :
185+
PartialIso X Y :=
186+
Classical.choice h
187+
188+
@[refl]
189+
lemma Birational.refl (X : Scheme.{u}) : Birational X X :=
190+
⟨.refl X⟩
191+
192+
@[symm]
193+
lemma Birational.symm {X Y : Scheme.{u}} (h : Birational X Y) : Birational Y X :=
194+
⟨h.partialIso.symm⟩
195+
196+
@[trans]
197+
lemma Birational.trans {X Y Z : Scheme.{u}} (h₁ : Birational X Y) (h₂ : Birational Y Z) :
198+
Birational X Z :=
199+
⟨h₁.partialIso.trans h₂.partialIso⟩
200+
201+
/-- `X` and `Y` are birational over `S` if there exists a partial isomorphism between them
202+
that is compatible with the structure maps to `S`. -/
203+
def BirationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S) : Prop :=
204+
∃ f : PartialIso X Y, f.IsOver sX sY
205+
206+
/-- Choose a partial isomorphism witnessing that `X` and `Y` are birational over `S`. -/
207+
noncomputable def BirationalOver.partialIso {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
208+
(h : BirationalOver sX sY) :=
209+
h.choose
210+
211+
lemma BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
212+
(h : BirationalOver sX sY) : h.partialIso.IsOver sX sY :=
213+
h.choose_spec
214+
215+
set_option backward.defeqAttrib.useBackward true in
216+
lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX sX :=
217+
⟨.refl X, by simp [PartialIso.IsOver]⟩
218+
219+
lemma BirationalOver.symm {S X Y : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S}
220+
(h : BirationalOver sX sY) : BirationalOver sY sX :=
221+
⟨h.partialIso.symm, h.partialIso_isOver.symm⟩
222+
223+
lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
224+
(h₁ : BirationalOver sX sY) (h₂ : BirationalOver sY sZ) :
225+
BirationalOver sX sZ :=
226+
⟨h₁.partialIso.trans h₂.partialIso, h₁.partialIso_isOver.trans h₂.partialIso_isOver⟩
227+
228+
/-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
229+
affine space `𝔸(n; S)`. Note that we do not require `n` to be finite here. -/
230+
@[mk_iff]
231+
class IsRationalOver {S X : Scheme.{u}} (sX : X ⟶ S) : Prop where
232+
exists_birationalOver_affineSpace (sX) : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S)
233+
234+
instance (S : Scheme.{u}) (n : Type u) : IsRationalOver (𝔸(n; S) ↘ S) where
235+
exists_birationalOver_affineSpace := ⟨n, .refl _⟩
236+
237+
/-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational. -/
238+
lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
239+
[IsRationalOver sY] (h : BirationalOver sX sY) : IsRationalOver sX := by
240+
obtain ⟨n, hn⟩ := IsRationalOver.exists_birationalOver_affineSpace sY
241+
exact ⟨n, h.trans hn⟩
242+
243+
section DenseOpen
244+
245+
variable {X S : Scheme.{u}} (U : Opens X) (sX : X ⟶ S)
246+
247+
/-- A dense open set `U : Opens X` induces a partial isomorphism between `U` and `X`. -/
248+
@[simps]
249+
def Opens.partialIsoOfDense (hU : Dense (U : Set X)) : PartialIso U X where
250+
source := ⊤
251+
dense_source := dense_univ
252+
target := U
253+
dense_target := hU
254+
iso := U.toScheme.topIso
255+
256+
/-- A dense open set `U : Opens X` is birational to `X`. -/
257+
lemma Opens.birational_of_dense (hU : Dense (U : Set X)) : Birational U X :=
258+
⟨U.partialIsoOfDense hU⟩
259+
260+
set_option backward.defeqAttrib.useBackward true in
261+
/-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`. -/
262+
lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver (U.ι ≫ sX) sX :=
263+
⟨U.partialIsoOfDense hU, by simp [PartialIso.IsOver]⟩
264+
265+
/-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational. -/
266+
lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver sX] :
267+
IsRationalOver (U.ι ≫ sX) := by
268+
obtain ⟨n, hn⟩ := IsRationalOver.exists_birationalOver_affineSpace sX
269+
exact ⟨n, (U.birationalOver_of_dense sX hU).trans hn⟩
270+
271+
end DenseOpen
272+
273+
section OpenImmersion
274+
275+
variable {X U S : Scheme.{u}}
276+
277+
/-- A dominant open immersion `f : U ⟶ X` induces a partial isomorphism between `U` and `X`. -/
278+
@[simps! source target iso]
279+
noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : U.PartialIso X :=
280+
(PartialIso.ofIso f.isoOpensRange).trans' (f.opensRange.partialIsoOfDense f.denseRange) rfl
281+
282+
lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Birational U X :=
283+
⟨f.partialIso⟩
284+
285+
set_option backward.defeqAttrib.useBackward true in
286+
lemma Hom.birationalOver (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] (sX : X ⟶ S) (sU : U ⟶ S)
287+
(hf : f ≫ sX = sU) : BirationalOver sU sX :=
288+
⟨f.partialIso, by simp [PartialIso.IsOver, hf]⟩
289+
290+
end OpenImmersion
291+
292+
end AlgebraicGeometry.Scheme

‎Mathlib/AlgebraicGeometry/Restrict.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -59,6 +59,8 @@ instance : IsOpenImmersion U.ι := inferInstanceAs (IsOpenImmersion (X.ofRestric
5959
@[simps! over] instance : U.toScheme.CanonicallyOver X where
6060
hom := U.ι
6161

62+
lemma ι_comp_over (S : Scheme.{u}) [X.Over S] : U.ι ≫ X ↘ S = U.toScheme ↘ S := rfl
63+
6264
instance (U : X.Opens) : U.ι.IsOver X where
6365

6466
lemma toScheme_carrier : (U : Type u) = (U : Set X) := rfl

0 commit comments

Comments
 (0)