toPartialMap_toRationalMap_restrict

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

Похожие утверждения