From 96897a539257901ed10d3b9761e20911e19a72df Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Sat, 9 May 2026 18:22:16 +0100
Subject: [PATCH 01/22] Birational

---
 Mathlib.lean                                  |   3 +-
 .../Birational/Birational.lean                | 260 ++++++++++++++++++
 .../{ => Birational}/RationalMap.lean         |   0
 Mathlib/AlgebraicGeometry/Restrict.lean       |   2 +
 4 files changed, 264 insertions(+), 1 deletion(-)
 create mode 100644 Mathlib/AlgebraicGeometry/Birational/Birational.lean
 rename Mathlib/AlgebraicGeometry/{ => Birational}/RationalMap.lean (100%)

diff --git a/Mathlib.lean b/Mathlib.lean
index 1993c03a943305..6a765dfc1307f9 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -1319,6 +1319,8 @@ public import Mathlib.AlgebraicGeometry.AffineSpace
 public import Mathlib.AlgebraicGeometry.AffineTransitionLimit
 public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
 public import Mathlib.AlgebraicGeometry.Artinian
+public import Mathlib.AlgebraicGeometry.Birational.Birational
+public import Mathlib.AlgebraicGeometry.Birational.RationalMap
 public import Mathlib.AlgebraicGeometry.ColimitsOver
 public import Mathlib.AlgebraicGeometry.Cover.Directed
 public import Mathlib.AlgebraicGeometry.Cover.MorphismProperty
@@ -1418,7 +1420,6 @@ public import Mathlib.AlgebraicGeometry.Properties
 public import Mathlib.AlgebraicGeometry.PullbackCarrier
 public import Mathlib.AlgebraicGeometry.Pullbacks
 public import Mathlib.AlgebraicGeometry.QuasiAffine
-public import Mathlib.AlgebraicGeometry.RationalMap
 public import Mathlib.AlgebraicGeometry.RelativeGluing
 public import Mathlib.AlgebraicGeometry.ResidueField
 public import Mathlib.AlgebraicGeometry.Restrict
diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
new file mode 100644
index 00000000000000..1ba27153f27143
--- /dev/null
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -0,0 +1,260 @@
+/-
+Copyright (c) 2026 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justus Springer
+-/
+module
+
+public import Mathlib.AlgebraicGeometry.AffineSpace
+public import Mathlib.AlgebraicGeometry.Birational.RationalMap
+/-!
+
+# Birationality and Rationality of schemes.
+
+This file defines partial isomorphisms between schemes and uses them to formalize
+birationality and rationality.
+
+## Main definitions
+
+- `Scheme.PartialIso X Y`: an isomorphism between a dense open subscheme of `X` and a
+  dense open subscheme of `Y`.
+- `Scheme.Birational X Y`: `X` and `Y` are birational, i.e. there exists a `PartialIso X Y`.
+- `Scheme.BirationalOver S X Y`: `X` and `Y` are birational over `S`.
+- `Scheme.IsRationalOver S X`: `X` is rational over `S`, i.e. birational over `S` to some
+  affine space `𝔸(Fin n; S)`.
+
+-/
+
+@[expose] public section
+
+universe u v
+
+open CategoryTheory
+
+namespace AlgebraicGeometry
+
+namespace Scheme
+
+/-- A partial isomorphism from `X` to `Y` is an isomorphism between dense open subschemes
+of `X` and `Y`. -/
+structure PartialIso (X Y : Scheme.{u}) where
+  /-- The source open subscheme of a partial isomorphism. -/
+  source : X.Opens
+  dense_source : Dense (source : Set X)
+  /-- The target open subscheme of a partial isomorphism. -/
+  target : Y.Opens
+  dense_target : Dense (target : Set Y)
+  /-- The underlying isomorphism of a partial isomorphism. -/
+  iso : source.toScheme ≅ target.toScheme
+
+namespace PartialIso
+
+variable {X Y Z S : Scheme.{u}}
+
+variable (S) in
+/-- A partial isomorphism `f : X.PartialIso Y` is over `S` if its underlying isomorphism
+is a morphism over `S`. -/
+abbrev IsOver (f : X.PartialIso Y) [X.Over S] [Y.Over S] : Prop :=
+  f.iso.hom.IsOver S
+
+lemma ext_iff (f g : X.PartialIso Y) :
+    f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target),
+      f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e' := by
+  constructor
+  · rintro rfl
+    simp
+  · obtain ⟨U₁, hU₁, U₂, hU₂, f⟩ := f
+    obtain ⟨V₁, hV₁, V₂, hU₂, g⟩ := g
+    simp only [forall_exists_index]
+    rintro rfl rfl e
+    simpa using e
+
+@[ext]
+lemma ext (f g : X.PartialIso Y) (e : f.source = g.source) (e' : g.target = f.target)
+    (H : f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e') : f = g := by
+  rw [ext_iff]
+  exact ⟨e, e', H⟩
+
+variable (X) in
+/-- The identity partial isomorphism on `X`, defined on all of `X`. -/
+@[simps]
+def refl : X.PartialIso X where
+  source := ⊤
+  dense_source := dense_univ
+  target := ⊤
+  dense_target := dense_univ
+  iso := Iso.refl _
+
+set_option backward.isDefEq.respectTransparency false in
+instance isOver_refl [X.Over S] : (refl X).IsOver S := by simp
+
+/-- The inverse of a partial isomorphism. -/
+@[symm, simps]
+def symm (f : X.PartialIso Y) : Y.PartialIso X where
+  source := f.target
+  dense_source := f.dense_target
+  target := f.source
+  dense_target := f.dense_source
+  iso := f.iso.symm
+
+set_option backward.isDefEq.respectTransparency false in
+instance isOver_symm [X.Over S] [Y.Over S] (f : X.PartialIso Y) [f.IsOver S] :
+    f.symm.IsOver S := by
+  simp
+
+/-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
+of `g`. See `trans` for the version that does not require this. -/
+@[simps]
+noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source) :
+    X.PartialIso Z where
+  source := f.source
+  dense_source := f.dense_source
+  target := g.target
+  dense_target := g.dense_target
+  iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
+
+set_option backward.isDefEq.respectTransparency false in
+instance isOver_trans' [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialIso Y) (g : Y.PartialIso Z)
+    [f.IsOver S] [g.IsOver S] (e : f.target = g.source) : (trans' f g e).IsOver S := by
+  simp [isoOfEq_hom]
+
+/-- Restrict the source of a partial isomorphism to a smaller dense open. -/
+@[simps source target, simps -isSimp iso]
+noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense (U : Set X))
+    (hU' : U ≤ f.source) : X.PartialIso Y where
+  source := U
+  dense_source := hU
+  target := f.target.ι ''ᵁ f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U
+  dense_target :=
+    have := PartialMap.Opens.isDominant_ι f.dense_target
+    f.target.ι.denseRange.dense_image f.target.ι.continuous <|
+      f.iso.hom.denseRange.dense_image f.iso.hom.continuous <|
+        hU.preimage f.source.ι.isOpenEmbedding.isOpenMap
+  iso := (Opens.isoOfLE hU').symm ≪≫
+    (f.iso.hom.isoImage (f.source.ι ⁻¹ᵁ U)) ≪≫
+    (f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
+
+set_option backward.isDefEq.respectTransparency false in
+instance isOver_restrictSource [X.Over S] [Y.Over S] (f : X.PartialIso Y) [f.IsOver S]
+    (U : Opens X) (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
+    (f.restrictSource U hU hU').IsOver S := by
+  simp only [Hom.isOver_iff, restrictSource_source, restrictSource_target, restrictSource_iso,
+    Iso.trans_hom, Iso.symm_hom, Category.assoc]
+  rw [← Opens.ι_comp_over, f.target.ι.isoImage_hom_ι_assoc, f.iso.hom.isoImage_hom_ι_assoc,
+    Opens.ι_comp_over, comp_over, ← f.source.ι_comp_over, Opens.isoOfLE_inv_ι_assoc,
+    Opens.ι_comp_over]
+
+/-- Restrict the target of a partial isomorphism to a smaller dense open. -/
+@[simps! source target, simps! -isSimp iso]
+noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense (U : Set Y))
+    (hU' : U ≤ f.target) : X.PartialIso Y :=
+  (f.symm.restrictSource U hU hU').symm
+
+instance isOver_restrictTarget [X.Over S] [Y.Over S] (f : X.PartialIso Y) [f.IsOver S]
+    (U : Opens Y) (hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
+    (f.restrictTarget U hU hU').IsOver S :=
+  (f.symm.restrictSource U hU hU').isOver_symm
+
+/-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
+@[trans, simps! source target, simps! -isSimp iso]
+noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso Z :=
+  have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
+  (f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl
+
+instance isOver_trans [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialIso Y) (g : Y.PartialIso Z)
+    [f.IsOver S] [g.IsOver S] : (f.trans g).IsOver S :=
+  isOver_trans' _ _ _
+
+/-- The underlying partial map of a partial isomorphism. -/
+@[simps]
+def toPartialMap (f : X.PartialIso Y) : X.PartialMap Y where
+  domain := f.source
+  dense_domain := f.dense_source
+  hom := f.iso.hom ≫ f.target.ι
+
+/-- The underlying rational map of a partial isomorphism. -/
+abbrev toRationalMap (f : X.PartialIso Y) : X ⤏ Y := f.toPartialMap.toRationalMap
+
+/-- A scheme isomorphism viewed as a partial isomorphism defined on all of `X` and `Y`. -/
+@[simps]
+noncomputable def _root_.CategoryTheory.Iso.toPartialIso (f : X ≅ Y) : X.PartialIso Y where
+  source := ⊤
+  dense_source := dense_univ
+  target := ⊤
+  dense_target := dense_univ
+  iso := X.topIso ≪≫ f ≪≫ Y.topIso.symm
+
+end PartialIso
+
+/-- `X` and `Y` are birational if there exists a partial isomorphism between them. -/
+def Birational (X Y : Scheme.{u}) : Prop := Nonempty (PartialIso X Y)
+
+/-- Choose a partial isomorphism witnessing that `X` and `Y` are birational. -/
+noncomputable def Birational.partialIso {X Y : Scheme.{u}} (h : Birational X Y) :
+    PartialIso X Y :=
+  Classical.choice h
+
+@[refl]
+lemma Birational.refl (X : Scheme.{u}) : Birational X X :=
+  ⟨.refl X⟩
+
+@[symm]
+lemma Birational.symm {X Y : Scheme.{u}} (h : Birational X Y) : Birational Y X :=
+  ⟨h.partialIso.symm⟩
+
+@[trans]
+lemma Birational.trans {X Y Z : Scheme.{u}} (h₁ : Birational X Y) (h₂ : Birational Y Z) :
+    Birational X Z :=
+  ⟨h₁.partialIso.trans h₂.partialIso⟩
+
+/-- `X` and `Y` are birational over `S` if there exists a partial isomorphism between them
+that is compatible with the structure maps to `S`. -/
+def BirationalOver (S X Y : Scheme.{u}) [X.Over S] [Y.Over S] : Prop :=
+  ∃ f : PartialIso X Y, f.IsOver S
+
+/-- Choose a partial isomorphism witnessing that `X` and `Y` are birational over `S`. -/
+noncomputable def BirationalOver.partialIso {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
+    (h : BirationalOver S X Y) :=
+  h.choose
+
+instance BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
+    (h : BirationalOver S X Y) : h.partialIso.IsOver S :=
+  h.choose_spec
+
+@[refl]
+lemma BirationalOver.refl (S X : Scheme.{u}) [X.Over S] : BirationalOver S X X :=
+  ⟨.refl X, inferInstance⟩
+
+@[symm]
+lemma BirationalOver.symm {S X Y : Scheme.{u}} [X.Over S] [Y.Over S] (h : BirationalOver S X Y) :
+    BirationalOver S Y X :=
+  ⟨h.partialIso.symm, inferInstance⟩
+
+@[trans]
+lemma BirationalOver.trans {S X Y Z : Scheme.{u}} [X.Over S] [Y.Over S] [Z.Over S]
+    (h₁ : BirationalOver S X Y) (h₂ : BirationalOver S Y Z) :
+    BirationalOver S X Z :=
+  ⟨h₁.partialIso.trans h₂.partialIso, inferInstance⟩
+
+/-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
+affine space `𝔸(Fin n; S)`. -/
+@[mk_iff]
+class IsRationalOver (S X : Scheme.{max u v}) [X.Over S] : Prop where
+  exists_birationalOver_affineSpace' : ∃ (n : Type v), BirationalOver S X 𝔸(n; S)
+
+lemma exists_birationalOver_affineSpace (S X : Scheme.{max u v}) [X.Over S]
+    [IsRationalOver.{u, v} S X] : ∃ (n : Type v), BirationalOver S X 𝔸(n; S) :=
+  IsRationalOver.exists_birationalOver_affineSpace'
+
+instance (S : Scheme.{max u v}) (n : Type v) : IsRationalOver.{u, v} S 𝔸(n; S) where
+  exists_birationalOver_affineSpace' := ⟨n, .refl S 𝔸(n; S)⟩
+
+/-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational. -/
+lemma BirationalOver.isRationalOver {S X Y : Scheme.{max u v}} [X.Over S] [Y.Over S]
+    [IsRationalOver.{u, v} S Y] (h : BirationalOver S X Y) : IsRationalOver.{u, v} S X := by
+  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace S Y
+  exact ⟨n, h.trans hn⟩
+
+end Scheme
+
+end AlgebraicGeometry
diff --git a/Mathlib/AlgebraicGeometry/RationalMap.lean b/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean
similarity index 100%
rename from Mathlib/AlgebraicGeometry/RationalMap.lean
rename to Mathlib/AlgebraicGeometry/Birational/RationalMap.lean
diff --git a/Mathlib/AlgebraicGeometry/Restrict.lean b/Mathlib/AlgebraicGeometry/Restrict.lean
index e1cb8636768e34..e01738cbf934f2 100644
--- a/Mathlib/AlgebraicGeometry/Restrict.lean
+++ b/Mathlib/AlgebraicGeometry/Restrict.lean
@@ -59,6 +59,8 @@ instance : IsOpenImmersion U.ι := inferInstanceAs (IsOpenImmersion (X.ofRestric
 @[simps! over] instance : U.toScheme.CanonicallyOver X where
   hom := U.ι
 
+lemma ι_comp_over (S : Scheme.{u}) [X.Over S] : U.ι ≫ X ↘ S = U.toScheme ↘ S := rfl
+
 instance (U : X.Opens) : U.ι.IsOver X where
 
 lemma toScheme_carrier : (U : Type u) = (U : Set X) := rfl

From 1c8990599915687b989cae64b9361f25cf66bf0d Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Sat, 9 May 2026 18:38:40 +0100
Subject: [PATCH 02/22] fix docstring

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 1ba27153f27143..e45cbc0da2c8ed 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -237,7 +237,7 @@ lemma BirationalOver.trans {S X Y Z : Scheme.{u}} [X.Over S] [Y.Over S] [Z.Over
   ⟨h₁.partialIso.trans h₂.partialIso, inferInstance⟩
 
 /-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
-affine space `𝔸(Fin n; S)`. -/
+affine space `𝔸(n; S)`. -/
 @[mk_iff]
 class IsRationalOver (S X : Scheme.{max u v}) [X.Over S] : Prop where
   exists_birationalOver_affineSpace' : ∃ (n : Type v), BirationalOver S X 𝔸(n; S)

From 8b051232a5d74ae1f0a847fb8996e783948050f3 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Sat, 9 May 2026 19:38:31 +0100
Subject: [PATCH 03/22] change universes of IsRationalOver

---
 .../AlgebraicGeometry/Birational/Birational.lean   | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index e45cbc0da2c8ed..afe5cd8f7928a2 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -239,19 +239,19 @@ lemma BirationalOver.trans {S X Y Z : Scheme.{u}} [X.Over S] [Y.Over S] [Z.Over
 /-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
 affine space `𝔸(n; S)`. -/
 @[mk_iff]
-class IsRationalOver (S X : Scheme.{max u v}) [X.Over S] : Prop where
-  exists_birationalOver_affineSpace' : ∃ (n : Type v), BirationalOver S X 𝔸(n; S)
+class IsRationalOver (S X : Scheme.{u}) [X.Over S] : Prop where
+  exists_birationalOver_affineSpace' : ∃ (n : Type), BirationalOver S X 𝔸(n; S)
 
-lemma exists_birationalOver_affineSpace (S X : Scheme.{max u v}) [X.Over S]
-    [IsRationalOver.{u, v} S X] : ∃ (n : Type v), BirationalOver S X 𝔸(n; S) :=
+lemma exists_birationalOver_affineSpace (S X : Scheme.{u}) [X.Over S]
+    [IsRationalOver S X] : ∃ (n : Type), BirationalOver S X 𝔸(n; S) :=
   IsRationalOver.exists_birationalOver_affineSpace'
 
-instance (S : Scheme.{max u v}) (n : Type v) : IsRationalOver.{u, v} S 𝔸(n; S) where
+instance (S : Scheme.{u}) (n : Type) : IsRationalOver S 𝔸(n; S) where
   exists_birationalOver_affineSpace' := ⟨n, .refl S 𝔸(n; S)⟩
 
 /-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational. -/
-lemma BirationalOver.isRationalOver {S X Y : Scheme.{max u v}} [X.Over S] [Y.Over S]
-    [IsRationalOver.{u, v} S Y] (h : BirationalOver S X Y) : IsRationalOver.{u, v} S X := by
+lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
+    [IsRationalOver S Y] (h : BirationalOver S X Y) : IsRationalOver S X := by
   obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace S Y
   exact ⟨n, h.trans hn⟩
 

From b537f066dccaa00afa1be1a6d0395cfde782d7fc Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Sun, 10 May 2026 14:07:13 +0100
Subject: [PATCH 04/22] add section on dense opens

---
 .../Birational/Birational.lean                | 33 +++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index afe5cd8f7928a2..18550de515c149 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -255,6 +255,39 @@ lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
   obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace S Y
   exact ⟨n, h.trans hn⟩
 
+section DenseOpen
+
+variable {X S : Scheme.{u}} [X.Over S] (U : Opens X)
+
+/-- A dense open set `U : Opens X` induces a partial isomorphism between `U` and `X`. -/
+@[simps]
+def Opens.partialIso_of_dense (hU : Dense (U : Set X)) : PartialIso U X where
+  source := ⊤
+  dense_source := dense_univ
+  target := U
+  dense_target := hU
+  iso := U.toScheme.topIso
+
+set_option backward.isDefEq.respectTransparency false in
+instance isOver_partialIso_of_dense (hU : Dense (U : Set X)) :
+    (U.partialIso_of_dense hU).IsOver S := by simp
+
+/-- A dense open set `U : Opens X` is birational to `X`. -/
+lemma Opens.birational_of_dense (hU : Dense (U : Set X)) : Birational U X :=
+  ⟨U.partialIso_of_dense hU⟩
+
+/-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`. -/
+lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver S U X :=
+  ⟨U.partialIso_of_dense hU, inferInstance⟩
+
+/-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational. -/
+lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver S X] :
+    IsRationalOver S U := by
+  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace S X
+  exact ⟨n, (U.birationalOver_of_dense hU).trans hn⟩
+
+end DenseOpen
+
 end Scheme
 
 end AlgebraicGeometry

From c34e1e8dcb7a0487b1fe3ac0665b94f2b64e69a2 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 13:09:59 +0100
Subject: [PATCH 05/22] use `Type u` in `IsRationalOver`

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 18550de515c149..1ed07a99c93f1d 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -240,13 +240,13 @@ lemma BirationalOver.trans {S X Y Z : Scheme.{u}} [X.Over S] [Y.Over S] [Z.Over
 affine space `𝔸(n; S)`. -/
 @[mk_iff]
 class IsRationalOver (S X : Scheme.{u}) [X.Over S] : Prop where
-  exists_birationalOver_affineSpace' : ∃ (n : Type), BirationalOver S X 𝔸(n; S)
+  exists_birationalOver_affineSpace' : ∃ (n : Type u), BirationalOver S X 𝔸(n; S)
 
 lemma exists_birationalOver_affineSpace (S X : Scheme.{u}) [X.Over S]
-    [IsRationalOver S X] : ∃ (n : Type), BirationalOver S X 𝔸(n; S) :=
+    [IsRationalOver S X] : ∃ (n : Type u), BirationalOver S X 𝔸(n; S) :=
   IsRationalOver.exists_birationalOver_affineSpace'
 
-instance (S : Scheme.{u}) (n : Type) : IsRationalOver S 𝔸(n; S) where
+instance (S : Scheme.{u}) (n : Type u) : IsRationalOver S 𝔸(n; S) where
   exists_birationalOver_affineSpace' := ⟨n, .refl S 𝔸(n; S)⟩
 
 /-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational. -/

From 3d96bdc82d51688df0f3e6c19816f7f4feb12c3f Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 14:23:20 +0100
Subject: [PATCH 06/22] don't use OverClass

---
 .../Birational/Birational.lean                | 112 +++++++++---------
 1 file changed, 53 insertions(+), 59 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 1ed07a99c93f1d..12b44147ec3573 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -49,13 +49,7 @@ structure PartialIso (X Y : Scheme.{u}) where
 
 namespace PartialIso
 
-variable {X Y Z S : Scheme.{u}}
-
-variable (S) in
-/-- A partial isomorphism `f : X.PartialIso Y` is over `S` if its underlying isomorphism
-is a morphism over `S`. -/
-abbrev IsOver (f : X.PartialIso Y) [X.Over S] [Y.Over S] : Prop :=
-  f.iso.hom.IsOver S
+variable {X Y Z S : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
 
 lemma ext_iff (f g : X.PartialIso Y) :
     f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target),
@@ -85,9 +79,6 @@ def refl : X.PartialIso X where
   dense_target := dense_univ
   iso := Iso.refl _
 
-set_option backward.isDefEq.respectTransparency false in
-instance isOver_refl [X.Over S] : (refl X).IsOver S := by simp
-
 /-- The inverse of a partial isomorphism. -/
 @[symm, simps]
 def symm (f : X.PartialIso Y) : Y.PartialIso X where
@@ -97,10 +88,9 @@ def symm (f : X.PartialIso Y) : Y.PartialIso X where
   dense_target := f.dense_source
   iso := f.iso.symm
 
-set_option backward.isDefEq.respectTransparency false in
-instance isOver_symm [X.Over S] [Y.Over S] (f : X.PartialIso Y) [f.IsOver S] :
-    f.symm.IsOver S := by
-  simp
+lemma isOver_symm (f : X.PartialIso Y) (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) :
+    f.symm.iso.hom ≫ f.symm.target.ι ≫ sX = f.symm.source.ι ≫ sY := by
+  simpa [← cancel_epi f.iso.hom] using hf.symm
 
 /-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
 of `g`. See `trans` for the version that does not require this. -/
@@ -113,13 +103,14 @@ noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target
   dense_target := g.dense_target
   iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
 
-set_option backward.isDefEq.respectTransparency false in
-instance isOver_trans' [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialIso Y) (g : Y.PartialIso Z)
-    [f.IsOver S] [g.IsOver S] (e : f.target = g.source) : (trans' f g e).IsOver S := by
-  simp [isoOfEq_hom]
+lemma isOver_trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source)
+    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
+    (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
+    (trans' f g e).iso.hom ≫ (trans' f g e).target.ι ≫ sZ = (trans' f g e).source.ι ≫ sX := by
+  simp [← hf, hg]
 
 /-- Restrict the source of a partial isomorphism to a smaller dense open. -/
-@[simps source target, simps -isSimp iso]
+@[simps source target iso]
 noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense (U : Set X))
     (hU' : U ≤ f.source) : X.PartialIso Y where
   source := U
@@ -134,26 +125,25 @@ noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense
     (f.iso.hom.isoImage (f.source.ι ⁻¹ᵁ U)) ≪≫
     (f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
 
-set_option backward.isDefEq.respectTransparency false in
-instance isOver_restrictSource [X.Over S] [Y.Over S] (f : X.PartialIso Y) [f.IsOver S]
+lemma isOver_restrictSource (f : X.PartialIso Y)
+    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
     (U : Opens X) (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
-    (f.restrictSource U hU hU').IsOver S := by
-  simp only [Hom.isOver_iff, restrictSource_source, restrictSource_target, restrictSource_iso,
-    Iso.trans_hom, Iso.symm_hom, Category.assoc]
-  rw [← Opens.ι_comp_over, f.target.ι.isoImage_hom_ι_assoc, f.iso.hom.isoImage_hom_ι_assoc,
-    Opens.ι_comp_over, comp_over, ← f.source.ι_comp_over, Opens.isoOfLE_inv_ι_assoc,
-    Opens.ι_comp_over]
+    (f.restrictSource U hU hU').iso.hom ≫ (f.restrictSource U hU hU').target.ι ≫ sY =
+      (f.restrictSource U hU hU').source.ι ≫ sX := by
+  simp [hf]
 
 /-- Restrict the target of a partial isomorphism to a smaller dense open. -/
-@[simps! source target, simps! -isSimp iso]
+@[simps! source target iso]
 noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense (U : Set Y))
     (hU' : U ≤ f.target) : X.PartialIso Y :=
   (f.symm.restrictSource U hU hU').symm
 
-instance isOver_restrictTarget [X.Over S] [Y.Over S] (f : X.PartialIso Y) [f.IsOver S]
-    (U : Opens Y) (hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
-    (f.restrictTarget U hU hU').IsOver S :=
-  (f.symm.restrictSource U hU hU').isOver_symm
+lemma isOver_restrictTarget (f : X.PartialIso Y)
+    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) (U : Opens Y) (hU : Dense (U : Set Y))
+    (hU' : U ≤ f.target) :
+    (f.restrictTarget U hU hU').iso.hom ≫ (f.restrictTarget U hU hU').target.ι ≫ sY =
+      (f.restrictTarget U hU hU').source.ι ≫ sX :=
+  isOver_symm _ (isOver_restrictSource _ (isOver_symm f hf) U hU hU')
 
 /-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
 @[trans, simps! source target, simps! -isSimp iso]
@@ -161,9 +151,11 @@ noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso
   have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
   (f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl
 
-instance isOver_trans [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialIso Y) (g : Y.PartialIso Z)
-    [f.IsOver S] [g.IsOver S] : (f.trans g).IsOver S :=
-  isOver_trans' _ _ _
+lemma isOver_trans (f : X.PartialIso Y) (g : Y.PartialIso Z)
+    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
+    (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
+    (f.trans g).iso.hom ≫ (f.trans g).target.ι ≫ sZ = (f.trans g).source.ι ≫ sX :=
+  isOver_trans' _ _ rfl (isOver_restrictTarget _ hf _ _ _) (isOver_restrictSource _ hg _ _ _)
 
 /-- The underlying partial map of a partial isomorphism. -/
 @[simps]
@@ -209,50 +201,52 @@ lemma Birational.trans {X Y Z : Scheme.{u}} (h₁ : Birational X Y) (h₂ : Bira
 
 /-- `X` and `Y` are birational over `S` if there exists a partial isomorphism between them
 that is compatible with the structure maps to `S`. -/
-def BirationalOver (S X Y : Scheme.{u}) [X.Over S] [Y.Over S] : Prop :=
-  ∃ f : PartialIso X Y, f.IsOver S
+def BirationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S) : Prop :=
+  ∃ f : PartialIso X Y, f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX
 
 /-- Choose a partial isomorphism witnessing that `X` and `Y` are birational over `S`. -/
-noncomputable def BirationalOver.partialIso {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
-    (h : BirationalOver S X Y) :=
+noncomputable def BirationalOver.partialIso {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
+    (h : BirationalOver sX sY) :=
   h.choose
 
-instance BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
-    (h : BirationalOver S X Y) : h.partialIso.IsOver S :=
+lemma BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
+    (h : BirationalOver sX sY) :
+    h.partialIso.iso.hom ≫ h.partialIso.target.ι ≫ sY = h.partialIso.source.ι ≫ sX :=
   h.choose_spec
 
 @[refl]
-lemma BirationalOver.refl (S X : Scheme.{u}) [X.Over S] : BirationalOver S X X :=
-  ⟨.refl X, inferInstance⟩
+lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX sX :=
+  ⟨.refl X, by simp⟩
 
 @[symm]
-lemma BirationalOver.symm {S X Y : Scheme.{u}} [X.Over S] [Y.Over S] (h : BirationalOver S X Y) :
-    BirationalOver S Y X :=
-  ⟨h.partialIso.symm, inferInstance⟩
+lemma BirationalOver.symm {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
+    (h : BirationalOver sX sY) : BirationalOver sY sX :=
+  ⟨h.partialIso.symm, PartialIso.isOver_symm _ h.partialIso_isOver⟩
 
 @[trans]
-lemma BirationalOver.trans {S X Y Z : Scheme.{u}} [X.Over S] [Y.Over S] [Z.Over S]
-    (h₁ : BirationalOver S X Y) (h₂ : BirationalOver S Y Z) :
-    BirationalOver S X Z :=
-  ⟨h₁.partialIso.trans h₂.partialIso, inferInstance⟩
+lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
+    (h₁ : BirationalOver sX sY) (h₂ : BirationalOver sY sZ) :
+    BirationalOver sX sZ :=
+  ⟨h₁.partialIso.trans h₂.partialIso,
+    PartialIso.isOver_trans _ _ h₁.partialIso_isOver h₂.partialIso_isOver⟩
 
 /-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
 affine space `𝔸(n; S)`. -/
 @[mk_iff]
-class IsRationalOver (S X : Scheme.{u}) [X.Over S] : Prop where
-  exists_birationalOver_affineSpace' : ∃ (n : Type u), BirationalOver S X 𝔸(n; S)
+class IsRationalOver {S X : Scheme.{u}} (sX : X ⟶ S) : Prop where
+  exists_birationalOver_affineSpace' : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S)
 
-lemma exists_birationalOver_affineSpace (S X : Scheme.{u}) [X.Over S]
-    [IsRationalOver S X] : ∃ (n : Type u), BirationalOver S X 𝔸(n; S) :=
+lemma exists_birationalOver_affineSpace {S X : Scheme.{u}} (sX : X ⟶ S)
+    [IsRationalOver sX] : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S) :=
   IsRationalOver.exists_birationalOver_affineSpace'
 
-instance (S : Scheme.{u}) (n : Type u) : IsRationalOver S 𝔸(n; S) where
-  exists_birationalOver_affineSpace' := ⟨n, .refl S 𝔸(n; S)⟩
+instance (S : Scheme.{u}) (n : Type u) : IsRationalOver (𝔸(n; S) ↘ S) where
+  exists_birationalOver_affineSpace' := ⟨n, .refl _⟩
 
 /-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational. -/
-lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} [X.Over S] [Y.Over S]
-    [IsRationalOver S Y] (h : BirationalOver S X Y) : IsRationalOver S X := by
-  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace S Y
+lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
+    [IsRationalOver sY] (h : BirationalOver sX sY) : IsRationalOver sX := by
+  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace sY
   exact ⟨n, h.trans hn⟩
 
 section DenseOpen

From 30966304ed036fe6528d407a7a84e722d45978d4 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 15:27:20 +0100
Subject: [PATCH 07/22] fixes

---
 .../Birational/Birational.lean                 | 18 +++++++-----------
 1 file changed, 7 insertions(+), 11 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 12b44147ec3573..e302d46e1fe4b6 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -251,7 +251,7 @@ lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y
 
 section DenseOpen
 
-variable {X S : Scheme.{u}} [X.Over S] (U : Opens X)
+variable {X S : Scheme.{u}} (U : Opens X) (sX : X ⟶ S)
 
 /-- A dense open set `U : Opens X` induces a partial isomorphism between `U` and `X`. -/
 @[simps]
@@ -262,23 +262,19 @@ def Opens.partialIso_of_dense (hU : Dense (U : Set X)) : PartialIso U X where
   dense_target := hU
   iso := U.toScheme.topIso
 
-set_option backward.isDefEq.respectTransparency false in
-instance isOver_partialIso_of_dense (hU : Dense (U : Set X)) :
-    (U.partialIso_of_dense hU).IsOver S := by simp
-
 /-- A dense open set `U : Opens X` is birational to `X`. -/
 lemma Opens.birational_of_dense (hU : Dense (U : Set X)) : Birational U X :=
   ⟨U.partialIso_of_dense hU⟩
 
 /-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`. -/
-lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver S U X :=
-  ⟨U.partialIso_of_dense hU, inferInstance⟩
+lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver (U.ι ≫ sX) sX :=
+  ⟨U.partialIso_of_dense hU, by simp⟩
 
 /-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational. -/
-lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver S X] :
-    IsRationalOver S U := by
-  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace S X
-  exact ⟨n, (U.birationalOver_of_dense hU).trans hn⟩
+lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver sX] :
+    IsRationalOver (U.ι ≫ sX) := by
+  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace sX
+  exact ⟨n, (U.birationalOver_of_dense sX hU).trans hn⟩
 
 end DenseOpen
 

From ec600b7e0ec5274d16bf81406ac55a5b128355ca Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 15:55:04 +0100
Subject: [PATCH 08/22] add section on open immersions

---
 .../Birational/Birational.lean                 | 18 ++++++++++++++++++
 1 file changed, 18 insertions(+)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index e302d46e1fe4b6..107e699625aa76 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -278,6 +278,24 @@ lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver sX]
 
 end DenseOpen
 
+section OpenImmersion
+
+variable {X U S : Scheme.{u}} 
+
+/-- A dominant open immersion `f : U ⟶ X` induced a partial isomorphism between `U` and `X`. -/
+@[simps! source target iso]
+noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] :=
+  f.isoOpensRange.toPartialIso.trans' (f.opensRange.partialIso_of_dense f.denseRange) rfl
+
+lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Birational U X :=
+  ⟨f.partialIso⟩
+
+lemma Hom.birationalOver (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] (sX : X ⟶ S) (sU : U ⟶ S)
+    (hf : f ≫ sX = sU) : BirationalOver sU sX :=
+  ⟨f.partialIso, by simp [hf]⟩
+
+end OpenImmersion
+
 end Scheme
 
 end AlgebraicGeometry

From 0b3fc8f66026c6db22484e814faa7177ec795816 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Wed, 13 May 2026 14:56:05 +0000
Subject: [PATCH 09/22] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 107e699625aa76..ebc25a0a5d7769 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -280,7 +280,7 @@ end DenseOpen
 
 section OpenImmersion
 
-variable {X U S : Scheme.{u}} 
+variable {X U S : Scheme.{u}}
 
 /-- A dominant open immersion `f : U ⟶ X` induced a partial isomorphism between `U` and `X`. -/
 @[simps! source target iso]

From 26201351730b0001e263a35073283a09120ed1fc Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 16:04:34 +0100
Subject: [PATCH 10/22] simps! everything

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 107e699625aa76..f6e61927ccf6d3 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -146,7 +146,7 @@ lemma isOver_restrictTarget (f : X.PartialIso Y)
   isOver_symm _ (isOver_restrictSource _ (isOver_symm f hf) U hU hU')
 
 /-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
-@[trans, simps! source target, simps! -isSimp iso]
+@[trans, simps! source target iso]
 noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso Z :=
   have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
   (f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl

From 872c51fca9d0ecb526a82d9bf652fe4b30c882a4 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 17:10:04 +0100
Subject: [PATCH 11/22] update docstring, change some names

---
 .../Birational/Birational.lean                | 27 ++++++++++---------
 1 file changed, 14 insertions(+), 13 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index f6e61927ccf6d3..40e7c1fab70421 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -19,9 +19,10 @@ birationality and rationality.
 - `Scheme.PartialIso X Y`: an isomorphism between a dense open subscheme of `X` and a
   dense open subscheme of `Y`.
 - `Scheme.Birational X Y`: `X` and `Y` are birational, i.e. there exists a `PartialIso X Y`.
-- `Scheme.BirationalOver S X Y`: `X` and `Y` are birational over `S`.
-- `Scheme.IsRationalOver S X`: `X` is rational over `S`, i.e. birational over `S` to some
-  affine space `𝔸(Fin n; S)`.
+- `Scheme.BirationalOver sX sY`: `X` and `Y` are birational over `S` via structure maps
+  `sX : X ⟶ S` and `sY : Y ⟶ S`.
+- `Scheme.IsRationalOver sX`: `X` is rational over `S` via structure map `sX : X ⟶ S`,
+  i.e. birational over `S` to some affine space `𝔸(n; S)`.
 
 -/
 
@@ -71,7 +72,7 @@ lemma ext (f g : X.PartialIso Y) (e : f.source = g.source) (e' : g.target = f.ta
 
 variable (X) in
 /-- The identity partial isomorphism on `X`, defined on all of `X`. -/
-@[simps]
+@[refl, simps]
 def refl : X.PartialIso X where
   source := ⊤
   dense_source := dense_univ
@@ -88,7 +89,7 @@ def symm (f : X.PartialIso Y) : Y.PartialIso X where
   dense_target := f.dense_source
   iso := f.iso.symm
 
-lemma isOver_symm (f : X.PartialIso Y) (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) :
+lemma symm_over (f : X.PartialIso Y) (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) :
     f.symm.iso.hom ≫ f.symm.target.ι ≫ sX = f.symm.source.ι ≫ sY := by
   simpa [← cancel_epi f.iso.hom] using hf.symm
 
@@ -103,7 +104,7 @@ noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target
   dense_target := g.dense_target
   iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
 
-lemma isOver_trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source)
+lemma trans'_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source)
     (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
     (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
     (trans' f g e).iso.hom ≫ (trans' f g e).target.ι ≫ sZ = (trans' f g e).source.ι ≫ sX := by
@@ -125,7 +126,7 @@ noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense
     (f.iso.hom.isoImage (f.source.ι ⁻¹ᵁ U)) ≪≫
     (f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
 
-lemma isOver_restrictSource (f : X.PartialIso Y)
+lemma restrictSource_over (f : X.PartialIso Y)
     (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
     (U : Opens X) (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
     (f.restrictSource U hU hU').iso.hom ≫ (f.restrictSource U hU hU').target.ι ≫ sY =
@@ -138,12 +139,12 @@ noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense
     (hU' : U ≤ f.target) : X.PartialIso Y :=
   (f.symm.restrictSource U hU hU').symm
 
-lemma isOver_restrictTarget (f : X.PartialIso Y)
+lemma restrictTarget_over (f : X.PartialIso Y)
     (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) (U : Opens Y) (hU : Dense (U : Set Y))
     (hU' : U ≤ f.target) :
     (f.restrictTarget U hU hU').iso.hom ≫ (f.restrictTarget U hU hU').target.ι ≫ sY =
       (f.restrictTarget U hU hU').source.ι ≫ sX :=
-  isOver_symm _ (isOver_restrictSource _ (isOver_symm f hf) U hU hU')
+  symm_over _ (restrictSource_over _ (symm_over f hf) U hU hU')
 
 /-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
 @[trans, simps! source target iso]
@@ -151,11 +152,11 @@ noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso
   have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
   (f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl
 
-lemma isOver_trans (f : X.PartialIso Y) (g : Y.PartialIso Z)
+lemma trans_over (f : X.PartialIso Y) (g : Y.PartialIso Z)
     (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
     (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
     (f.trans g).iso.hom ≫ (f.trans g).target.ι ≫ sZ = (f.trans g).source.ι ≫ sX :=
-  isOver_trans' _ _ rfl (isOver_restrictTarget _ hf _ _ _) (isOver_restrictSource _ hg _ _ _)
+  trans'_over _ _ rfl (restrictTarget_over _ hf _ _ _) (restrictSource_over _ hg _ _ _)
 
 /-- The underlying partial map of a partial isomorphism. -/
 @[simps]
@@ -221,14 +222,14 @@ lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX
 @[symm]
 lemma BirationalOver.symm {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
     (h : BirationalOver sX sY) : BirationalOver sY sX :=
-  ⟨h.partialIso.symm, PartialIso.isOver_symm _ h.partialIso_isOver⟩
+  ⟨h.partialIso.symm, PartialIso.symm_over _ h.partialIso_isOver⟩
 
 @[trans]
 lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
     (h₁ : BirationalOver sX sY) (h₂ : BirationalOver sY sZ) :
     BirationalOver sX sZ :=
   ⟨h₁.partialIso.trans h₂.partialIso,
-    PartialIso.isOver_trans _ _ h₁.partialIso_isOver h₂.partialIso_isOver⟩
+    PartialIso.trans_over _ _ h₁.partialIso_isOver h₂.partialIso_isOver⟩
 
 /-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
 affine space `𝔸(n; S)`. -/

From 02ee8ef803b49cfa202f5367156b869eeda5f690 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 13 May 2026 17:14:24 +0100
Subject: [PATCH 12/22] small changes

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 40e7c1fab70421..3f801371d3a94e 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -28,7 +28,7 @@ birationality and rationality.
 
 @[expose] public section
 
-universe u v
+universe u
 
 open CategoryTheory
 
@@ -215,16 +215,13 @@ lemma BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY :
     h.partialIso.iso.hom ≫ h.partialIso.target.ι ≫ sY = h.partialIso.source.ι ≫ sX :=
   h.choose_spec
 
-@[refl]
 lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX sX :=
   ⟨.refl X, by simp⟩
 
-@[symm]
-lemma BirationalOver.symm {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
+lemma BirationalOver.symm {S X Y : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S}
     (h : BirationalOver sX sY) : BirationalOver sY sX :=
   ⟨h.partialIso.symm, PartialIso.symm_over _ h.partialIso_isOver⟩
 
-@[trans]
 lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
     (h₁ : BirationalOver sX sY) (h₂ : BirationalOver sY sZ) :
     BirationalOver sX sZ :=

From 1df80ce0b8a0d4696c226c11b79848fe12ec57c1 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Thu, 14 May 2026 22:39:00 +0100
Subject: [PATCH 13/22] fix

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 6c94edb2d62fc3..53a0f993a9f98b 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -118,7 +118,7 @@ noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense
   dense_source := hU
   target := f.target.ι ''ᵁ f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U
   dense_target :=
-    have := PartialMap.Opens.isDominant_ι f.dense_target
+    have := Opens.isDominant_ι f.dense_target
     f.target.ι.denseRange.dense_image f.target.ι.continuous <|
       f.iso.hom.denseRange.dense_image f.iso.hom.continuous <|
         hU.preimage f.source.ι.isOpenEmbedding.isOpenMap

From a508980cd1ece475eaa387fb53da8fd2f7ddcc3d Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Thu, 28 May 2026 12:32:00 +0100
Subject: [PATCH 14/22] fix

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 53a0f993a9f98b..b0a6da33f641c3 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -253,7 +253,7 @@ variable {X S : Scheme.{u}} (U : Opens X) (sX : X ⟶ S)
 
 /-- A dense open set `U : Opens X` induces a partial isomorphism between `U` and `X`. -/
 @[simps]
-def Opens.partialIso_of_dense (hU : Dense (U : Set X)) : PartialIso U X where
+def Opens.partialIsoOfDense (hU : Dense (U : Set X)) : PartialIso U X where
   source := ⊤
   dense_source := dense_univ
   target := U
@@ -262,11 +262,11 @@ def Opens.partialIso_of_dense (hU : Dense (U : Set X)) : PartialIso U X where
 
 /-- A dense open set `U : Opens X` is birational to `X`. -/
 lemma Opens.birational_of_dense (hU : Dense (U : Set X)) : Birational U X :=
-  ⟨U.partialIso_of_dense hU⟩
+  ⟨U.partialIsoOfDense hU⟩
 
 /-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`. -/
 lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver (U.ι ≫ sX) sX :=
-  ⟨U.partialIso_of_dense hU, by simp⟩
+  ⟨U.partialIsoOfDense hU, by simp⟩
 
 /-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational. -/
 lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver sX] :
@@ -283,7 +283,7 @@ variable {X U S : Scheme.{u}}
 /-- A dominant open immersion `f : U ⟶ X` induced a partial isomorphism between `U` and `X`. -/
 @[simps! source target iso]
 noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] :=
-  f.isoOpensRange.toPartialIso.trans' (f.opensRange.partialIso_of_dense f.denseRange) rfl
+  f.isoOpensRange.toPartialIso.trans' (f.opensRange.partialIsoOfDense f.denseRange) rfl
 
 lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Birational U X :=
   ⟨f.partialIso⟩

From 6b98083b010b62112626902e5f3b1912ef1fbd12 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 3 Jun 2026 14:30:07 +0100
Subject: [PATCH 15/22] add backward options

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index b0a6da33f641c3..5cb57db40c42e9 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -89,6 +89,7 @@ def symm (f : X.PartialIso Y) : Y.PartialIso X where
   dense_target := f.dense_source
   iso := f.iso.symm
 
+set_option backward.defeqAttrib.useBackward true in
 lemma symm_over (f : X.PartialIso Y) (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) :
     f.symm.iso.hom ≫ f.symm.target.ι ≫ sX = f.symm.source.ι ≫ sY := by
   simpa [← cancel_epi f.iso.hom] using hf.symm
@@ -104,6 +105,7 @@ noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target
   dense_target := g.dense_target
   iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
 
+set_option backward.defeqAttrib.useBackward true in
 lemma trans'_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source)
     (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
     (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
@@ -126,6 +128,7 @@ noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense
     (f.iso.hom.isoImage (f.source.ι ⁻¹ᵁ U)) ≪≫
     (f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
 
+set_option backward.defeqAttrib.useBackward true in
 lemma restrictSource_over (f : X.PartialIso Y)
     (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
     (U : Opens X) (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
@@ -215,6 +218,7 @@ lemma BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY :
     h.partialIso.iso.hom ≫ h.partialIso.target.ι ≫ sY = h.partialIso.source.ι ≫ sX :=
   h.choose_spec
 
+set_option backward.defeqAttrib.useBackward true in
 lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX sX :=
   ⟨.refl X, by simp⟩
 
@@ -264,6 +268,7 @@ def Opens.partialIsoOfDense (hU : Dense (U : Set X)) : PartialIso U X where
 lemma Opens.birational_of_dense (hU : Dense (U : Set X)) : Birational U X :=
   ⟨U.partialIsoOfDense hU⟩
 
+set_option backward.defeqAttrib.useBackward true in
 /-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`. -/
 lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver (U.ι ≫ sX) sX :=
   ⟨U.partialIsoOfDense hU, by simp⟩
@@ -288,6 +293,7 @@ noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f
 lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Birational U X :=
   ⟨f.partialIso⟩
 
+set_option backward.defeqAttrib.useBackward true in
 lemma Hom.birationalOver (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] (sX : X ⟶ S) (sU : U ⟶ S)
     (hf : f ≫ sX = sU) : BirationalOver sU sX :=
   ⟨f.partialIso, by simp [hf]⟩

From d0fd850f0a3734980503e88a303d0ab3d3059c45 Mon Sep 17 00:00:00 2001
From: Justus Springer <50165510+justus-springer@users.noreply.github.com>
Date: Wed, 3 Jun 2026 14:34:01 +0100
Subject: [PATCH 16/22] Apply suggestions from code review

Co-authored-by: Christian Merten <christian@merten.dev>
---
 .../AlgebraicGeometry/Birational/Birational.lean  | 15 +++++++--------
 1 file changed, 7 insertions(+), 8 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index b0a6da33f641c3..c1193ae62c643b 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -32,9 +32,7 @@ universe u
 
 open CategoryTheory
 
-namespace AlgebraicGeometry
-
-namespace Scheme
+namespace AlgebraicGeometry.Scheme
 
 /-- A partial isomorphism from `X` to `Y` is an isomorphism between dense open subschemes
 of `X` and `Y`. -/
@@ -111,7 +109,7 @@ lemma trans'_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.so
   simp [← hf, hg]
 
 /-- Restrict the source of a partial isomorphism to a smaller dense open. -/
-@[simps source target iso]
+@[simps]
 noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense (U : Set X))
     (hU' : U ≤ f.source) : X.PartialIso Y where
   source := U
@@ -170,7 +168,7 @@ abbrev toRationalMap (f : X.PartialIso Y) : X ⤏ Y := f.toPartialMap.toRational
 
 /-- A scheme isomorphism viewed as a partial isomorphism defined on all of `X` and `Y`. -/
 @[simps]
-noncomputable def _root_.CategoryTheory.Iso.toPartialIso (f : X ≅ Y) : X.PartialIso Y where
+noncomputable def ofIso (f : X ≅ Y) : X.PartialIso Y where
   source := ⊤
   dense_source := dense_univ
   target := ⊤
@@ -180,6 +178,7 @@ noncomputable def _root_.CategoryTheory.Iso.toPartialIso (f : X ≅ Y) : X.Parti
 end PartialIso
 
 /-- `X` and `Y` are birational if there exists a partial isomorphism between them. -/
+@[stacks 0A20 "(1)"]
 def Birational (X Y : Scheme.{u}) : Prop := Nonempty (PartialIso X Y)
 
 /-- Choose a partial isomorphism witnessing that `X` and `Y` are birational. -/
@@ -232,7 +231,7 @@ lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S}
 affine space `𝔸(n; S)`. -/
 @[mk_iff]
 class IsRationalOver {S X : Scheme.{u}} (sX : X ⟶ S) : Prop where
-  exists_birationalOver_affineSpace' : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S)
+  exists_birationalOver_affineSpace (sX) : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S)
 
 lemma exists_birationalOver_affineSpace {S X : Scheme.{u}} (sX : X ⟶ S)
     [IsRationalOver sX] : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S) :=
@@ -280,9 +279,9 @@ section OpenImmersion
 
 variable {X U S : Scheme.{u}}
 
-/-- A dominant open immersion `f : U ⟶ X` induced a partial isomorphism between `U` and `X`. -/
+/-- A dominant open immersion `f : U ⟶ X` induces a partial isomorphism between `U` and `X`. -/
 @[simps! source target iso]
-noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] :=
+noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : U.PartialIso X :=
   f.isoOpensRange.toPartialIso.trans' (f.opensRange.partialIsoOfDense f.denseRange) rfl
 
 lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Birational U X :=

From ff96612192b4c26997257be11955f602170f07ce Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 3 Jun 2026 14:37:01 +0100
Subject: [PATCH 17/22] fixes

---
 .../AlgebraicGeometry/Birational/Birational.lean | 16 +++++-----------
 1 file changed, 5 insertions(+), 11 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 6b7412fc48a6b9..db300039055c48 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -237,17 +237,13 @@ affine space `𝔸(n; S)`. -/
 class IsRationalOver {S X : Scheme.{u}} (sX : X ⟶ S) : Prop where
   exists_birationalOver_affineSpace (sX) : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S)
 
-lemma exists_birationalOver_affineSpace {S X : Scheme.{u}} (sX : X ⟶ S)
-    [IsRationalOver sX] : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S) :=
-  IsRationalOver.exists_birationalOver_affineSpace'
-
 instance (S : Scheme.{u}) (n : Type u) : IsRationalOver (𝔸(n; S) ↘ S) where
-  exists_birationalOver_affineSpace' := ⟨n, .refl _⟩
+  exists_birationalOver_affineSpace := ⟨n, .refl _⟩
 
 /-- If a scheme `X` is `S`-birational to an `S`-rational scheme `Y`, then `X` is `S`-rational. -/
 lemma BirationalOver.isRationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
     [IsRationalOver sY] (h : BirationalOver sX sY) : IsRationalOver sX := by
-  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace sY
+  obtain ⟨n, hn⟩ := IsRationalOver.exists_birationalOver_affineSpace sY
   exact ⟨n, h.trans hn⟩
 
 section DenseOpen
@@ -275,7 +271,7 @@ lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver (U
 /-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational. -/
 lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver sX] :
     IsRationalOver (U.ι ≫ sX) := by
-  obtain ⟨n, hn⟩ := exists_birationalOver_affineSpace sX
+  obtain ⟨n, hn⟩ := IsRationalOver.exists_birationalOver_affineSpace sX
   exact ⟨n, (U.birationalOver_of_dense sX hU).trans hn⟩
 
 end DenseOpen
@@ -287,7 +283,7 @@ variable {X U S : Scheme.{u}}
 /-- A dominant open immersion `f : U ⟶ X` induces a partial isomorphism between `U` and `X`. -/
 @[simps! source target iso]
 noncomputable def Hom.partialIso (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : U.PartialIso X :=
-  f.isoOpensRange.toPartialIso.trans' (f.opensRange.partialIsoOfDense f.denseRange) rfl
+  (PartialIso.ofIso f.isoOpensRange).trans' (f.opensRange.partialIsoOfDense f.denseRange) rfl
 
 lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Birational U X :=
   ⟨f.partialIso⟩
@@ -299,6 +295,4 @@ lemma Hom.birationalOver (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] (sX :
 
 end OpenImmersion
 
-end Scheme
-
-end AlgebraicGeometry
+end AlgebraicGeometry.Scheme

From a1c377b76536496033493199b665152c692ea967 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Wed, 3 Jun 2026 15:22:28 +0100
Subject: [PATCH 18/22] add PartialIso.IsOver

---
 .../Birational/Birational.lean                | 53 +++++++++----------
 1 file changed, 24 insertions(+), 29 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index db300039055c48..15f0f6969961f6 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -7,8 +7,8 @@ module
 
 public import Mathlib.AlgebraicGeometry.AffineSpace
 public import Mathlib.AlgebraicGeometry.Birational.RationalMap
-/-!
 
+/-!
 # Birationality and Rationality of schemes.
 
 This file defines partial isomorphisms between schemes and uses them to formalize
@@ -50,6 +50,11 @@ namespace PartialIso
 
 variable {X Y Z S : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
 
+variable (sX sY) in
+/-- A partial iso is an `S`-map if the underlying morphism is. -/
+abbrev IsOver (f : X.PartialIso Y) : Prop :=
+  f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX
+
 lemma ext_iff (f g : X.PartialIso Y) :
     f = g ↔ ∃ (e : f.source = g.source) (e' : g.target = f.target),
       f.iso = X.isoOfEq e ≪≫ g.iso ≪≫ Y.isoOfEq e' := by
@@ -88,9 +93,8 @@ def symm (f : X.PartialIso Y) : Y.PartialIso X where
   iso := f.iso.symm
 
 set_option backward.defeqAttrib.useBackward true in
-lemma symm_over (f : X.PartialIso Y) (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) :
-    f.symm.iso.hom ≫ f.symm.target.ι ≫ sX = f.symm.source.ι ≫ sY := by
-  simpa [← cancel_epi f.iso.hom] using hf.symm
+lemma symm_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) : f.symm.IsOver sY sX := by
+  simpa [IsOver, ← cancel_epi f.iso.hom] using hf.symm
 
 /-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
 of `g`. See `trans` for the version that does not require this. -/
@@ -105,10 +109,8 @@ noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target
 
 set_option backward.defeqAttrib.useBackward true in
 lemma trans'_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source)
-    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
-    (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
-    (trans' f g e).iso.hom ≫ (trans' f g e).target.ι ≫ sZ = (trans' f g e).source.ι ≫ sX := by
-  simp [← hf, hg]
+    (hf : f.IsOver sX sY) (hg : g.IsOver sY sZ) : (trans' f g e).IsOver sX sZ := by
+  simp [IsOver, ← hf, hg]
 
 /-- Restrict the source of a partial isomorphism to a smaller dense open. -/
 @[simps]
@@ -127,12 +129,10 @@ noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense
     (f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
 
 set_option backward.defeqAttrib.useBackward true in
-lemma restrictSource_over (f : X.PartialIso Y)
-    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
-    (U : Opens X) (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
-    (f.restrictSource U hU hU').iso.hom ≫ (f.restrictSource U hU hU').target.ι ≫ sY =
-      (f.restrictSource U hU hU').source.ι ≫ sX := by
-  simp [hf]
+lemma restrictSource_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) (U : Opens X)
+    (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
+    (f.restrictSource U hU hU').IsOver sX sY := by
+  simp [IsOver, hf]
 
 /-- Restrict the target of a partial isomorphism to a smaller dense open. -/
 @[simps! source target iso]
@@ -140,11 +140,9 @@ noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense
     (hU' : U ≤ f.target) : X.PartialIso Y :=
   (f.symm.restrictSource U hU hU').symm
 
-lemma restrictTarget_over (f : X.PartialIso Y)
-    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX) (U : Opens Y) (hU : Dense (U : Set Y))
-    (hU' : U ≤ f.target) :
-    (f.restrictTarget U hU hU').iso.hom ≫ (f.restrictTarget U hU hU').target.ι ≫ sY =
-      (f.restrictTarget U hU hU').source.ι ≫ sX :=
+lemma restrictTarget_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) (U : Opens Y)
+    (hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
+    (f.restrictTarget U hU hU').IsOver sX sY := 
   symm_over _ (restrictSource_over _ (symm_over f hf) U hU hU')
 
 /-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
@@ -153,10 +151,8 @@ noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso
   have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
   (f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl
 
-lemma trans_over (f : X.PartialIso Y) (g : Y.PartialIso Z)
-    (hf : f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX)
-    (hg : g.iso.hom ≫ g.target.ι ≫ sZ = g.source.ι ≫ sY) :
-    (f.trans g).iso.hom ≫ (f.trans g).target.ι ≫ sZ = (f.trans g).source.ι ≫ sX :=
+lemma trans_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (hf : f.IsOver sX sY)
+    (hg : g.IsOver sY sZ) : (f.trans g).IsOver sX sZ :=
   trans'_over _ _ rfl (restrictTarget_over _ hf _ _ _) (restrictSource_over _ hg _ _ _)
 
 /-- The underlying partial map of a partial isomorphism. -/
@@ -205,7 +201,7 @@ lemma Birational.trans {X Y Z : Scheme.{u}} (h₁ : Birational X Y) (h₂ : Bira
 /-- `X` and `Y` are birational over `S` if there exists a partial isomorphism between them
 that is compatible with the structure maps to `S`. -/
 def BirationalOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S) : Prop :=
-  ∃ f : PartialIso X Y, f.iso.hom ≫ f.target.ι ≫ sY = f.source.ι ≫ sX
+  ∃ f : PartialIso X Y, f.IsOver sX sY
 
 /-- Choose a partial isomorphism witnessing that `X` and `Y` are birational over `S`. -/
 noncomputable def BirationalOver.partialIso {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
@@ -213,13 +209,12 @@ noncomputable def BirationalOver.partialIso {S X Y : Scheme.{u}} (sX : X ⟶ S)
   h.choose
 
 lemma BirationalOver.partialIso_isOver {S X Y : Scheme.{u}} (sX : X ⟶ S) (sY : Y ⟶ S)
-    (h : BirationalOver sX sY) :
-    h.partialIso.iso.hom ≫ h.partialIso.target.ι ≫ sY = h.partialIso.source.ι ≫ sX :=
+    (h : BirationalOver sX sY) : h.partialIso.IsOver sX sY :=
   h.choose_spec
 
 set_option backward.defeqAttrib.useBackward true in
 lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX sX :=
-  ⟨.refl X, by simp⟩
+  ⟨.refl X, by simp [PartialIso.IsOver]⟩
 
 lemma BirationalOver.symm {S X Y : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S}
     (h : BirationalOver sX sY) : BirationalOver sY sX :=
@@ -266,7 +261,7 @@ lemma Opens.birational_of_dense (hU : Dense (U : Set X)) : Birational U X :=
 set_option backward.defeqAttrib.useBackward true in
 /-- A dense open set `U : Opens X` of a scheme `X` over `S` is `S`-birational to `X`. -/
 lemma Opens.birationalOver_of_dense (hU : Dense (U : Set X)) : BirationalOver (U.ι ≫ sX) sX :=
-  ⟨U.partialIsoOfDense hU, by simp⟩
+  ⟨U.partialIsoOfDense hU, by simp [PartialIso.IsOver]⟩
 
 /-- A dense open set `U : Opens X` of a `S`-rational scheme `X` is `S`-rational. -/
 lemma Opens.isRationalOver_of_dense (hU : Dense (U : Set X)) [IsRationalOver sX] :
@@ -291,7 +286,7 @@ lemma Hom.birational (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] : Biration
 set_option backward.defeqAttrib.useBackward true in
 lemma Hom.birationalOver (f : U ⟶ X) [IsOpenImmersion f] [IsDominant f] (sX : X ⟶ S) (sU : U ⟶ S)
     (hf : f ≫ sX = sU) : BirationalOver sU sX :=
-  ⟨f.partialIso, by simp [hf]⟩
+  ⟨f.partialIso, by simp [PartialIso.IsOver, hf]⟩
 
 end OpenImmersion
 

From 515dabda3f21ee21943946f72c3f69980804fea9 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci-lite[bot]"
 <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
Date: Wed, 3 Jun 2026 14:23:25 +0000
Subject: [PATCH 19/22] [pre-commit.ci lite] apply automatic fixes

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 15f0f6969961f6..8a06623d6dea6f 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -142,7 +142,7 @@ noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense
 
 lemma restrictTarget_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) (U : Opens Y)
     (hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
-    (f.restrictTarget U hU hU').IsOver sX sY := 
+    (f.restrictTarget U hU hU').IsOver sX sY :=
   symm_over _ (restrictSource_over _ (symm_over f hf) U hU hU')
 
 /-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/

From d653fe2c9faa86a7e84fd380034bf5d676aced61 Mon Sep 17 00:00:00 2001
From: Justus Springer <50165510+justus-springer@users.noreply.github.com>
Date: Fri, 5 Jun 2026 13:22:43 +0100
Subject: [PATCH 20/22] Apply suggestions from code review

Co-authored-by: Christian Merten <christian@merten.dev>
---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 8a06623d6dea6f..90f3900d64407c 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -93,7 +93,7 @@ def symm (f : X.PartialIso Y) : Y.PartialIso X where
   iso := f.iso.symm
 
 set_option backward.defeqAttrib.useBackward true in
-lemma symm_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) : f.symm.IsOver sY sX := by
+lemma IsOver.symm {f : X.PartialIso Y} (hf : f.IsOver sX sY) : f.symm.IsOver sY sX := by
   simpa [IsOver, ← cancel_epi f.iso.hom] using hf.symm
 
 /-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
@@ -108,7 +108,7 @@ noncomputable def trans' (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target
   iso := f.iso ≪≫ Y.isoOfEq e ≪≫ g.iso
 
 set_option backward.defeqAttrib.useBackward true in
-lemma trans'_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (e : f.target = g.source)
+lemma IsOver.trans' {f : X.PartialIso Y} {g : Y.PartialIso Z} {e : f.target = g.source}
     (hf : f.IsOver sX sY) (hg : g.IsOver sY sZ) : (trans' f g e).IsOver sX sZ := by
   simp [IsOver, ← hf, hg]
 
@@ -129,7 +129,7 @@ noncomputable def restrictSource (f : X.PartialIso Y) (U : Opens X) (hU : Dense
     (f.target.ι.isoImage (f.iso.hom ''ᵁ f.source.ι ⁻¹ᵁ U))
 
 set_option backward.defeqAttrib.useBackward true in
-lemma restrictSource_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) (U : Opens X)
+lemma IsOver.restrictSource {f : X.PartialIso Y} (hf : f.IsOver sX sY) (U : Opens X)
     (hU : Dense (U : Set X)) (hU' : U ≤ f.source) :
     (f.restrictSource U hU hU').IsOver sX sY := by
   simp [IsOver, hf]
@@ -140,7 +140,7 @@ noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense
     (hU' : U ≤ f.target) : X.PartialIso Y :=
   (f.symm.restrictSource U hU hU').symm
 
-lemma restrictTarget_over (f : X.PartialIso Y) (hf : f.IsOver sX sY) (U : Opens Y)
+lemma IsOver.restrictTarget {f : X.PartialIso Y} (hf : f.IsOver sX sY) (U : Opens Y)
     (hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
     (f.restrictTarget U hU hU').IsOver sX sY :=
   symm_over _ (restrictSource_over _ (symm_over f hf) U hU hU')
@@ -151,7 +151,7 @@ noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso
   have := f.dense_target.inter_of_isOpen_right g.dense_source g.source.2
   (f.restrictTarget _ this inf_le_left).trans' (g.restrictSource _ this inf_le_right) rfl
 
-lemma trans_over (f : X.PartialIso Y) (g : Y.PartialIso Z) (hf : f.IsOver sX sY)
+lemma IsOver.trans {f : X.PartialIso Y} {g : Y.PartialIso Z} (hf : f.IsOver sX sY)
     (hg : g.IsOver sY sZ) : (f.trans g).IsOver sX sZ :=
   trans'_over _ _ rfl (restrictTarget_over _ hf _ _ _) (restrictSource_over _ hg _ _ _)
 

From 1ee796934a036da50f9b1d7253f504f17db6424a Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Fri, 5 Jun 2026 14:07:42 +0100
Subject: [PATCH 21/22] fix

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 90f3900d64407c..63fa8f08a1579f 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -94,7 +94,7 @@ def symm (f : X.PartialIso Y) : Y.PartialIso X where
 
 set_option backward.defeqAttrib.useBackward true in
 lemma IsOver.symm {f : X.PartialIso Y} (hf : f.IsOver sX sY) : f.symm.IsOver sY sX := by
-  simpa [IsOver, ← cancel_epi f.iso.hom] using hf.symm
+  simpa [IsOver, ← cancel_epi f.iso.hom] using Eq.symm hf
 
 /-- Compose two partial isomorphisms along a proof that the target of `f` equals the source
 of `g`. See `trans` for the version that does not require this. -/
@@ -143,7 +143,7 @@ noncomputable def restrictTarget (f : X.PartialIso Y) (U : Opens Y) (hU : Dense
 lemma IsOver.restrictTarget {f : X.PartialIso Y} (hf : f.IsOver sX sY) (U : Opens Y)
     (hU : Dense (U : Set Y)) (hU' : U ≤ f.target) :
     (f.restrictTarget U hU hU').IsOver sX sY :=
-  symm_over _ (restrictSource_over _ (symm_over f hf) U hU hU')
+  (hf.symm.restrictSource U hU hU').symm
 
 /-- Compose two partial isomorphisms, restricting to the intersection of the intermediate opens. -/
 @[trans, simps! source target iso]
@@ -153,7 +153,7 @@ noncomputable def trans (f : X.PartialIso Y) (g : Y.PartialIso Z) : X.PartialIso
 
 lemma IsOver.trans {f : X.PartialIso Y} {g : Y.PartialIso Z} (hf : f.IsOver sX sY)
     (hg : g.IsOver sY sZ) : (f.trans g).IsOver sX sZ :=
-  trans'_over _ _ rfl (restrictTarget_over _ hf _ _ _) (restrictSource_over _ hg _ _ _)
+  (hf.restrictTarget _ _ _).trans' (hg.restrictSource _ _ _)
 
 /-- The underlying partial map of a partial isomorphism. -/
 @[simps]
@@ -218,13 +218,12 @@ lemma BirationalOver.refl {S X : Scheme.{u}} (sX : X ⟶ S) : BirationalOver sX
 
 lemma BirationalOver.symm {S X Y : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S}
     (h : BirationalOver sX sY) : BirationalOver sY sX :=
-  ⟨h.partialIso.symm, PartialIso.symm_over _ h.partialIso_isOver⟩
+  ⟨h.partialIso.symm, h.partialIso_isOver.symm⟩
 
 lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S} {sZ : Z ⟶ S}
     (h₁ : BirationalOver sX sY) (h₂ : BirationalOver sY sZ) :
     BirationalOver sX sZ :=
-  ⟨h₁.partialIso.trans h₂.partialIso,
-    PartialIso.trans_over _ _ h₁.partialIso_isOver h₂.partialIso_isOver⟩
+  ⟨h₁.partialIso.trans h₂.partialIso, h₁.partialIso_isOver.trans h₂.partialIso_isOver⟩
 
 /-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
 affine space `𝔸(n; S)`. -/

From 95fecc71d35128e03604fbc357d5c7ae32484f10 Mon Sep 17 00:00:00 2001
From: Justus Springer <justusspringer@gmx.de>
Date: Thu, 25 Jun 2026 12:45:11 +0100
Subject: [PATCH 22/22] add comment

---
 Mathlib/AlgebraicGeometry/Birational/Birational.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/AlgebraicGeometry/Birational/Birational.lean b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
index 63fa8f08a1579f..a191e2e295f390 100644
--- a/Mathlib/AlgebraicGeometry/Birational/Birational.lean
+++ b/Mathlib/AlgebraicGeometry/Birational/Birational.lean
@@ -226,7 +226,7 @@ lemma BirationalOver.trans {S X Y Z : Scheme.{u}} {sX : X ⟶ S} {sY : Y ⟶ S}
   ⟨h₁.partialIso.trans h₂.partialIso, h₁.partialIso_isOver.trans h₂.partialIso_isOver⟩
 
 /-- `X` is rational over `S` (or `S`-rational) if it is birational over `S` to some
-affine space `𝔸(n; S)`. -/
+affine space `𝔸(n; S)`. Note that we do not require `n` to be finite here. -/
 @[mk_iff]
 class IsRationalOver {S X : Scheme.{u}} (sX : X ⟶ S) : Prop where
   exists_birationalOver_affineSpace (sX) : ∃ (n : Type u), BirationalOver sX (𝔸(n; S) ↘ S)