feat(AlgebraicGeometry/Birational): composition of rational maps (#39445)

justus-springer · justus-springer · commit d45663d02f17 · 2026-07-10T02:16:48.000Z
Define composition of partial and rational maps. - [x] depends on: #39442 - [x] depends on: #39443 - [x] depends on: #39317 - [x] depends on: #40189
diff --git a/Mathlib.lean b/Mathlib.lean
@@ -1350,6 +1350,7 @@ public import Mathlib.AlgebraicGeometry.AlgClosed.Basic
 public import Mathlib.AlgebraicGeometry.AlgebraicCycle.Basic
 public import Mathlib.AlgebraicGeometry.Artinian
 public import Mathlib.AlgebraicGeometry.Birational.Birational
+public import Mathlib.AlgebraicGeometry.Birational.Composition
 public import Mathlib.AlgebraicGeometry.Birational.Dominant
 public import Mathlib.AlgebraicGeometry.Birational.RationalMap
 public import Mathlib.AlgebraicGeometry.ColimitsOver
diff --git a/Mathlib/AlgebraicGeometry/Birational/Composition.lean b/Mathlib/AlgebraicGeometry/Birational/Composition.lean
@@ -0,0 +1,219 @@
+/-
+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.Birational.Dominant
+
+/-!
+# Composition of rational maps
+
+This file defines composition for partial maps and rational maps between schemes.
+
+## Main definitions
+
+- `Scheme.PartialMap.comp`: given a dominant partial map `f : X.PartialMap Y` and any partial map
+  `g : Y.PartialMap Z`, their composition `f.comp g : X.PartialMap Z` is defined on the preimage
+  of `g`'s domain under `f`.
+- `Scheme.RationalMap.comp`: composition of rational maps, defined via a dominant representative.
+
+## Main statements
+
+- `Scheme.PartialMap.comp_equiv_of_equiv`: Composition respects equivalence of partial maps.
+- `Scheme.PartialMap.comp_assoc`: Composition of partial maps is associative.
+- `Scheme.RationalMap.comp_assoc`: Composition of rational maps is associative.
+
+-/
+
+@[expose] public section
+
+universe u
+
+open CategoryTheory
+
+namespace AlgebraicGeometry.Scheme
+
+variable {X Y Z : Scheme.{u}}
+
+section PreirreducibleSpace
+
+variable [PreirreducibleSpace X] [Nonempty Y]
+
+namespace PartialMap
+
+/-- Composition of partial maps. The domain of `f.comp g` is the preimage of `g.domain` under `f`,
+viewed as an open subscheme of `X`. Requires `f.hom` to be dominant so that the domain is dense. -/
+@[simps]
+noncomputable def comp (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) :
+    X.PartialMap Z where
+  domain := f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain
+  dense_domain := (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain).2.dense <| by
+    simpa [← Set.nonempty_preimage_iff] using
+      f.hom.denseRange.inter_open_nonempty _ g.domain.2 g.dense_domain.nonempty
+  hom := (f.domain.ι.isoImage _).inv ≫ f.hom ∣_ g.domain ≫ g.hom
+
+set_option backward.defeqAttrib.useBackward true in
+lemma comp_restrict_left (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens)
+    (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) (g : Y.PartialMap Z) :
+    (f.restrict U hU hU').comp g = (f.comp g).restrict (f.domain.ι ''ᵁ f.hom ⁻¹ᵁ g.domain ⊓ U)
+      ((f.comp g).dense_domain.inter_of_isOpen_right hU U.2) inf_le_left := by
+  ext
+  · simp [ι_image_homOfLE_eq_ι_image_inf]
+  · simp [morphismRestrict_comp, isoImage_ι_inv_morphismRestrict_homOfLE_assoc, isoOfEq_hom]
+
+set_option backward.defeqAttrib.useBackward true in
+lemma comp_restrict_right (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z)
+    (V : Y.Opens) (hV : Dense (V : Set Y)) (hV' : V ≤ g.domain) :
+    f.comp (g.restrict V hV hV') = (f.comp g).restrict
+      (f.domain.ι ''ᵁ (f.hom ⁻¹ᵁ V)) ((f.domain.ι ''ᵁ f.hom ⁻¹ᵁ V).2.dense <| by
+        simpa [← Set.nonempty_preimage_iff] using
+          f.hom.denseRange.inter_open_nonempty _ V.2 hV.nonempty)
+      (f.domain.ι.image_mono (f.hom.preimage_mono hV')) := by
+  ext
+  · simp
+  · simp [← f.domain.ι.isoImage_inv_homOfLE_assoc _ _ (f.hom.preimage_mono hV'),
+      ← morphismRestrict_homOfLE_assoc f.hom _ _ hV']
+
+set_option backward.defeqAttrib.useBackward true in
+/-- Composition respects equivalence of partial maps on the left. -/
+lemma comp_equiv_of_equiv_left {f₁ f₂ : X.PartialMap Y} [IsDominant f₁.hom] [IsDominant f₂.hom]
+    (h : f₁.equiv f₂) (g : Y.PartialMap Z) :
+    (f₁.comp g).equiv (f₂.comp g) := by
+  obtain ⟨W, hW, hW₁, hW₂, e⟩ := h
+  replace e : f₁.restrict W hW hW₁ = f₂.restrict W hW hW₂ :=
+    PartialMap.ext _ _ rfl (by simpa using e)
+  replace e := congr($(e).comp g)
+  rw [comp_restrict_left, comp_restrict_left] at e
+  exact equiv_of_restrict_eq _ _ e
+
+set_option backward.defeqAttrib.useBackward true in
+/-- Composition respects equivalence of partial maps on the right. -/
+lemma comp_equiv_of_equiv_right (f : X.PartialMap Y) [IsDominant f.hom] {g₁ g₂ : Y.PartialMap Z}
+    (h : g₁.equiv g₂) : (f.comp g₁).equiv (f.comp g₂) := by
+  obtain ⟨W, hW, hW₁, hW₂, e⟩ := h
+  replace e : g₁.restrict W hW hW₁ = g₂.restrict W hW hW₂ :=
+    PartialMap.ext _ _ rfl (by simpa using e)
+  replace e := congr(f.comp $e)
+  rw [comp_restrict_right, comp_restrict_right] at e
+  exact equiv_of_restrict_eq _ _ e
+
+/-- Composition respects equivalence of partial maps in both arguments. -/
+lemma comp_equiv_of_equiv (f₁ f₂ : X.PartialMap Y) [IsDominant f₁.hom] [IsDominant f₂.hom]
+    (hf : f₁.equiv f₂) (g₁ g₂ : Y.PartialMap Z) (hg : g₁.equiv g₂) :
+    (f₁.comp g₁).equiv (f₂.comp g₂) :=
+  equivalence_rel.trans (comp_equiv_of_equiv_left hf _) (comp_equiv_of_equiv_right _ hg)
+
+set_option backward.defeqAttrib.useBackward true in
+instance isDominant_comp_hom (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z)
+    [IsDominant g.hom] : IsDominant (f.comp g).hom := by
+  dsimp only [comp_domain, comp_hom]
+  have := IsZariskiLocalAtTarget.restrict ‹IsDominant f.hom› g.domain
+  infer_instance
+
+set_option backward.defeqAttrib.useBackward true in
+@[simp]
+lemma comp_assoc {X₁ X₂ X₃ Y : Scheme.{u}} [PreirreducibleSpace X₁] [IrreducibleSpace X₂]
+    [Nonempty X₃] (f : X₁.PartialMap X₂) [IsDominant f.hom] (g : X₂.PartialMap X₃)
+    [IsDominant g.hom] (h : X₃.PartialMap Y) :
+    (f.comp g).comp h = f.comp (g.comp h) := by
+  ext
+  · simp_rw [comp_domain, comp_hom, ← Category.assoc, Hom.comp_preimage, Hom.inv_preimage,
+      ← Hom.comp_image, Hom.isoImage_hom_ι, Hom.comp_image, image_morphismRestrict_preimage]
+  · dsimp
+    simp_rw [morphismRestrict_comp, morphismRestrict_ι_image_ι_isoImage_inv_assoc,
+      Hom.comp_preimage, Category.assoc]
+    conv_lhs => rw [← Category.assoc]
+    conv_rhs => rw [← Category.assoc, ← Category.assoc, ← Category.assoc]
+    congr 1
+    simp [← cancel_mono (Opens.ι _)]
+
+set_option backward.defeqAttrib.useBackward true in
+@[simp]
+lemma comp_toPartialMap (f : X.PartialMap Y) [IsDominant f.hom] (g : Y ⟶ Z) :
+    f.comp g.toPartialMap = f.compHom g := by
+  ext1
+  · simp
+  · simp_rw [comp_hom, Hom.toPartialMap_domain, Hom.toPartialMap_hom, compHom_hom, topIso_hom,
+      morphismRestrict_ι_assoc, f.domain.isoImage_ι_inv_ι_assoc, isoOfEq_hom]
+    rfl
+
+set_option backward.defeqAttrib.useBackward true in
+lemma comp_id (f : X.PartialMap Y) [IsDominant f.hom] : f.comp (PartialMap.id Y) = f := by simp
+
+end PartialMap
+
+namespace RationalMap
+
+-- If better def-eqs are required, consider refactoring this by using `Quotient.liftOn₂`
+-- and a bundled structure `DominantPartialMap`.
+/-- Composition of rational maps. Requires `f` to be dominant, so that we may choose
+a dominant representative. -/
+noncomputable def comp (f : X ⤏ Y) [f.IsDominant] (g : Y ⤏ Z) : X ⤏ Z :=
+  Quotient.liftOn g (PartialMap.toRationalMap ∘ f.representative.comp) <| fun _ _ h ↦ by
+    rw [Function.comp_apply, Function.comp_apply, PartialMap.toRationalMap_eq_iff]
+    exact PartialMap.comp_equiv_of_equiv_right _ h
+
+lemma comp_def (f : X ⤏ Y) [f.IsDominant] (g : Y.PartialMap Z) :
+    f.comp g.toRationalMap = (f.representative.comp g).toRationalMap :=
+  rfl
+
+lemma toRationalMap_comp (f : X.PartialMap Y) [IsDominant f.hom] (g : Y.PartialMap Z) :
+    f.toRationalMap.comp g.toRationalMap = (f.comp g).toRationalMap := by
+  rw [RationalMap.comp_def, PartialMap.toRationalMap_eq_iff]
+  exact PartialMap.comp_equiv_of_equiv_left f.representative_toRationalMap_equiv _
+
+@[simp]
+lemma comp_id (f : X ⤏ Y) [f.IsDominant] : f.comp (RationalMap.id Y) = f := by
+  simp [RationalMap.comp_def]
+
+instance (f : X ⤏ Y) [f.IsDominant] (g : Y ⤏ Z) [g.IsDominant] : (f.comp g).IsDominant := by
+  rw [← g.toRationalMap_representative, RationalMap.comp_def]
+  infer_instance
+
+lemma comp_toRationalMap (f : X ⤏ Y) [f.IsDominant] (h : Y ⟶ Z) :
+    f.comp h.toRationalMap = f.compHom h := by
+  simp [comp_def, PartialMap.comp_toPartialMap]
+
+@[grind _=_]
+lemma comp_assoc {X₁ X₂ X₃ Y : Scheme.{u}} [PreirreducibleSpace X₁] [IrreducibleSpace X₂]
+    [Nonempty X₃] (f₁ : X₁ ⤏ X₂) [f₁.IsDominant] (f₂ : X₂ ⤏ X₃) [f₂.IsDominant] (f₃ : X₃ ⤏ Y) :
+    (f₁.comp f₂).comp f₃ = f₁.comp (f₂.comp f₃) := by
+  rw [← f₃.toRationalMap_representative]
+  simp_rw [comp_def, ← PartialMap.comp_assoc, PartialMap.toRationalMap_eq_iff]
+  apply PartialMap.comp_equiv_of_equiv_left
+  rw [← f₂.toRationalMap_representative, comp_def]
+  apply (f₁.representative.comp f₂.representative).representative_toRationalMap_equiv.trans
+  apply PartialMap.comp_equiv_of_equiv_right
+  rw [toRationalMap_representative]
+
+instance isOver_comp {S : Scheme.{u}} [IrreducibleSpace Y] [Nonempty Z] [X.Over S] [Y.Over S]
+    [Z.Over S] (f : X ⤏ Y) [f.IsDominant] [f.IsOver S] (g : Y ⤏ Z) [g.IsDominant] [g.IsOver S] :
+    (f.comp g).IsOver S := by
+  rw [isOver_iff, ← comp_toRationalMap, comp_assoc, comp_toRationalMap,
+    isOver_iff.mp ‹g.IsOver S›, comp_toRationalMap, RationalMap.isOver_iff.mp ‹f.IsOver S›]
+
+end RationalMap
+
+end PreirreducibleSpace
+
+set_option backward.defeqAttrib.useBackward true in
+@[simp]
+lemma PartialMap.id_comp {X Y : Scheme.{u}} [IrreducibleSpace X] (f : X.PartialMap Y) :
+    (PartialMap.id X).comp f = f := by
+  ext1
+  · simp_rw [comp_domain, Hom.toPartialMap_domain, Hom.toPartialMap_hom, Category.comp_id,
+      ← X.topIso_hom, ← Hom.inv_image, ← Hom.comp_image, Iso.inv_hom_id, Hom.id_image]
+  · simp_rw [comp_hom, Hom.toPartialMap_hom, Hom.toPartialMap_domain, morphismRestrict_comp,
+      morphismRestrict_id, ← X.topIso_hom, Hom.comp_preimage, Hom.id_preimage,
+      Category.comp_id, ← X.topIso.hom.isoImage_preimage_hom_homOfLE, Category.assoc,
+      Iso.inv_hom_id_assoc]
+    rfl
+
+@[simp, grind =]
+lemma RationalMap.id_comp {X Y : Scheme.{u}} [IrreducibleSpace X] (f : X ⤏ Y) :
+    (RationalMap.id X).comp f = f := by
+  rw [← f.toRationalMap_representative, toRationalMap_comp, PartialMap.id_comp]
+
+end AlgebraicGeometry.Scheme
diff --git a/Mathlib/AlgebraicGeometry/Birational/Dominant.lean b/Mathlib/AlgebraicGeometry/Birational/Dominant.lean
@@ -36,7 +36,7 @@ namespace PartialMap
 
 set_option backward.defeqAttrib.useBackward true in
 /-- Restricting a dominant partial map to a dense open yields a dominant partial map. -/
-lemma isDominant_restrict_hom (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens)
+instance isDominant_restrict_hom (f : X.PartialMap Y) [IsDominant f.hom] (U : X.Opens)
     (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) : IsDominant (f.restrict U hU hU').hom := by
   dsimp only [restrict_domain, restrict_hom]
   have : IsDominant (X.homOfLE hU') := Opens.isDominant_homOfLE hU hU'
diff --git a/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean b/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean
@@ -120,15 +120,38 @@ def compHom (f : X.PartialMap Y) (g : Y ⟶ Z) : X.PartialMap Z where
   dense_domain := f.dense_domain
   hom := f.hom ≫ g
 
+set_option backward.defeqAttrib.useBackward true in
+@[simp]
+lemma compHom_id (f : X.PartialMap Y) : f.compHom (𝟙 Y) = f := by
+  ext <;> simp
+
 set_option backward.defeqAttrib.useBackward true in
 instance [X.Over S] [Y.Over S] [Z.Over S] (f : X.PartialMap Y) (g : Y ⟶ Z)
     [f.IsOver S] [g.IsOver S] : (f.compHom g).IsOver S where
 
 /-- A scheme morphism as a partial map. -/
 @[simps]
-def _root_.AlgebraicGeometry.Scheme.Hom.toPartialMap (f : X.Hom Y) :
+def _root_.AlgebraicGeometry.Scheme.Hom.toPartialMap (f : X ⟶ Y) :
     X.PartialMap Y := ⟨⊤, dense_univ, X.topIso.hom ≫ f⟩
 
+set_option backward.defeqAttrib.useBackward true in
+instance (f : X ⟶ Y) [IsDominant f] : IsDominant f.toPartialMap.hom := by
+  dsimp
+  have := Opens.isDominant_ι (X := X) (U := ⊤) dense_univ
+  infer_instance
+
+lemma _root_.AlgebraicGeometry.Scheme.Hom.toPartialMap_compHom (f : X ⟶ Y) (g : Y ⟶ Z) :
+    f.toPartialMap.compHom g = (f ≫ g).toPartialMap := rfl
+
+variable (X) in
+/-- The identity partial map. -/
+protected abbrev id : X.PartialMap X := (𝟙 X : X ⟶ X).toPartialMap
+
+@[simp]
+lemma id_compHom (f : X ⟶ Y) : (PartialMap.id X).compHom f = f.toPartialMap := by
+  apply PartialMap.ext _ _ rfl
+  simp
+
 set_option backward.defeqAttrib.useBackward true in
 instance [X.Over S] [Y.Over S] (f : X ⟶ Y) [f.IsOver S] : f.toPartialMap.IsOver S where
 
@@ -226,20 +249,37 @@ def equiv (f g : X.PartialMap Y) : Prop :=
   ∃ (W : X.Opens) (hW : Dense (W : Set X)) (hWl : W ≤ f.domain) (hWr : W ≤ g.domain),
     (f.restrict W hW hWl).hom = (g.restrict W hW hWr).hom
 
+lemma equiv_of_restrict_eq (f g : X.PartialMap Y) {W₁ W₂ : X.Opens} {hW₁ : Dense (W₁ : Set X)}
+    {hW₂ : Dense (W₂ : Set X)} {hW₁' : W₁ ≤ f.domain} {hW₂' : W₂ ≤ g.domain}
+    (H : f.restrict W₁ hW₁ hW₁' = g.restrict W₂ hW₂ hW₂') : f.equiv g := by
+  have e : W₁ = W₂ := congr($(H).domain)
+  subst e
+  exact ⟨W₁, hW₁, hW₁', hW₂', congr($(H).hom)⟩
+
+@[refl]
+lemma equiv.refl (f : X.PartialMap Y) : f.equiv f :=
+  ⟨f.domain, f.dense_domain, by simp⟩
+
+@[symm]
+lemma equiv.symm {f g : X.PartialMap Y} : f.equiv g → g.equiv f := by
+  intro ⟨W, hW, hWl, hWr, e⟩
+  exact ⟨W, hW, hWr, hWl, e.symm⟩
+
 set_option backward.defeqAttrib.useBackward true in
+@[trans]
+lemma equiv.trans {f g h : X.PartialMap Y} : f.equiv g → g.equiv h → f.equiv h := by
+  intro ⟨W₁, hW₁, hW₁l, hW₁r, e₁⟩ ⟨W₂, hW₂, hW₂l, hW₂r, e₂⟩
+  refine ⟨W₁ ⊓ W₂, hW₁.inter_of_isOpen_left hW₂ W₁.2, inf_le_left.trans hW₁l,
+    inf_le_right.trans hW₂r, ?_⟩
+  dsimp at e₁ e₂
+  simp only [restrict_domain, restrict_hom, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_left hW₁l,
+    Category.assoc, e₁, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_right hW₂r, ← e₂]
+  simp only [homOfLE_homOfLE_assoc]
+
 lemma equivalence_rel : Equivalence (@Scheme.PartialMap.equiv X Y) where
-  refl f := ⟨f.domain, f.dense_domain, by simp⟩
-  symm {f g} := by
-    intro ⟨W, hW, hWl, hWr, e⟩
-    exact ⟨W, hW, hWr, hWl, e.symm⟩
-  trans {f g h} := by
-    intro ⟨W₁, hW₁, hW₁l, hW₁r, e₁⟩ ⟨W₂, hW₂, hW₂l, hW₂r, e₂⟩
-    refine ⟨W₁ ⊓ W₂, hW₁.inter_of_isOpen_left hW₂ W₁.2, inf_le_left.trans hW₁l,
-      inf_le_right.trans hW₂r, ?_⟩
-    dsimp at e₁ e₂
-    simp only [restrict_domain, restrict_hom, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_left hW₁l,
-      Category.assoc, e₁, ← X.homOfLE_homOfLE (U := W₁ ⊓ W₂) inf_le_right hW₂r, ← e₂]
-    simp only [homOfLE_homOfLE_assoc]
+  refl := equiv.refl
+  symm := equiv.symm
+  trans := equiv.trans
 
 instance : Setoid (X.PartialMap Y) := ⟨@PartialMap.equiv X Y, equivalence_rel⟩
 
@@ -334,6 +374,10 @@ def PartialMap.toRationalMap (f : X.PartialMap Y) : X ⤏ Y := Quotient.mk _ f
 /-- A scheme morphism as a rational map. -/
 abbrev Hom.toRationalMap (f : X.Hom Y) : X ⤏ Y := f.toPartialMap.toRationalMap
 
+variable (X) in
+/-- The identity rational map. -/
+abbrev RationalMap.id : X ⤏ X := (PartialMap.id X).toRationalMap
+
 variable (S) in
 /-- A rational map is an `S`-map if some partial map in the equivalence class is an `S`-map. -/
 class RationalMap.IsOver [X.Over S] [Y.Over S] (f : X ⤏ Y) : Prop where
@@ -391,6 +435,11 @@ def RationalMap.compHom (f : X ⤏ Y) (g : Y ⟶ Z) : X ⤏ Z := by
 lemma RationalMap.compHom_toRationalMap (f : X.PartialMap Y) (g : Y ⟶ Z) :
     (f.compHom g).toRationalMap = f.toRationalMap.compHom g := rfl
 
+@[simp]
+lemma RationalMap.id_compHom (f : X ⟶ Y) :
+    (RationalMap.id X).compHom f = f.toRationalMap := by
+  rw [RationalMap.id, ← compHom_toRationalMap, PartialMap.id_compHom]
+
 instance [X.Over S] [Y.Over S] [Z.Over S] (f : X ⤏ Y) (g : Y ⟶ Z)
     [f.IsOver S] [g.IsOver S] : (f.compHom g).IsOver S where
   exists_partialMap_over := by
diff --git a/Mathlib/AlgebraicGeometry/OpenImmersion.lean b/Mathlib/AlgebraicGeometry/OpenImmersion.lean
@@ -201,6 +201,9 @@ lemma id_image {X : Scheme} (U : X.Opens) : 𝟙 X ''ᵁ U = U :=
 lemma inv_image {X Y : Scheme} (e : X ≅ Y) (U : Y.Opens) : e.inv ''ᵁ U = e.hom ⁻¹ᵁ U :=
   TopologicalSpace.Opens.ext <| (Scheme.homeoOfIso e.symm).toEquiv.image_eq_preimage_symm _
 
+lemma inv_preimage {X Y : Scheme} (e : X ≅ Y) (U : X.Opens) : e.inv ⁻¹ᵁ U = e.hom ''ᵁ U :=
+  (inv_image e.symm U).symm
+
 @[simp]
 lemma apply_mem_image_iff {X Y : Scheme} (f : X ⟶ Y) [IsOpenImmersion f]
     {U : X.Opens} {x : X} : f x ∈ f ''ᵁ U ↔ x ∈ U :=
