English
Restricting a rational map to its domain yields a morphism whose domain is the same; the original map is recovered by restriction.
Русский
Ограничение рациональной карты до ее области определения возвращает морфизм с той же областью определения; исходная карта восстанавливается посредством ограничения.
LaTeX
$$$$ f = f|_{\operatorname{Dom}(f)}. $$$$
Lean4
theorem toPartialMap_toRationalMap_restrict [IsReduced X] [Y.IsSeparated] (f : X.PartialMap Y) :
(f.toRationalMap.toPartialMap.restrict _ f.dense_domain f.le_domain_toRationalMap).hom = f.hom :=
by
dsimp [RationalMap.toPartialMap]
refine (f.toRationalMap.openCoverDomain.ι_glueMorphisms _ _ ⟨_, f, rfl, rfl⟩).trans ?_
generalize_proofs _ _ H _
have : H.choose = f :=
(equiv_iff_of_domain_eq_of_isSeparated (S := ⊤_ _) H.choose_spec.2).mp (toRationalMap_eq_iff.mp H.choose_spec.1)
exact ((ext_iff _ _).mp this.symm).choose_spec.symm