isOver_toRationalMap_iff_of_isSeparated

English

For a reduced X and separated Y over S, an open dense test shows that f is over S iff its rational map version is over S.

Русский

Для редуцированной X и разделимой Y над S падение над S по открытой плотной проверке равносильно тому, что рациональная карта над S тоже имеет данность над S.

LaTeX

$$$f.toRationalMap.IsOver S \iff f.IsOver S$$$

Lean4

theorem isOver_toRationalMap_iff_of_isSeparated [X.Over S] [Y.Over S] [IsReduced X] [S.IsSeparated]
    {f : X.PartialMap Y} : f.toRationalMap.IsOver S ↔ f.IsOver S :=
  by
  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
  obtain ⟨U, hU, hU', H⟩ := f.exists_restrict_isOver (S := S)
  rw [isOver_iff]
  have : IsDominant (X.homOfLE hU') := Opens.isDominant_homOfLE hU _
  exact ext_of_isDominant (ι := X.homOfLE hU') (by simpa using H.1)

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