From 1038f55b3666aeb2f0ffc2387b3e36cf65493a0d Mon Sep 17 00:00:00 2001 From: Justus Springer Date: Thu, 21 May 2026 13:29:31 +0100 Subject: [PATCH] add RationalMap.representative --- .../AlgebraicGeometry/Birational/RationalMap.lean | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean b/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean index bd67cca3b9d31e..57e8264af3ba32 100644 --- a/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean +++ b/Mathlib/AlgebraicGeometry/Birational/RationalMap.lean @@ -334,6 +334,20 @@ lemma PartialMap.toRationalMap_eq_iff {f g : X.PartialMap Y} : f.toRationalMap = g.toRationalMap ↔ f.equiv g := Quotient.eq +/-- An arbitrarily chosen partial map representing `f`. Use `RationalMap.toPartialMap` instead +if `X` is reduced and `Y` is separated. -/ +noncomputable def RationalMap.representative (f : X ⤏ Y) : X.PartialMap Y := + f.exists_rep.choose + +@[simp] +lemma RationalMap.toRationalMap_representative (f : X ⤏ Y) : + f.representative.toRationalMap = f := + f.exists_rep.choose_spec + +lemma PartialMap.representative_toRationalMap_equiv (f : X.PartialMap Y) : + f.toRationalMap.representative.equiv f := by + rw [← PartialMap.toRationalMap_eq_iff, f.toRationalMap.toRationalMap_representative] + @[simp] lemma PartialMap.restrict_toRationalMap (f : X.PartialMap Y) (U : X.Opens) (hU : Dense (U : Set X)) (hU' : U ≤ f.domain) :