exists_restrict_isOver

Mathlib.AlgebraicGeometry.RationalMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.PartialMap.exists_restrict_isOver

Lean4

theorem exists_restrict_isOver [X.Over S] [Y.Over S] (f : X.PartialMap Y) [f.toRationalMap.IsOver S] :
    ∃ U hU hU', (f.restrict U hU hU').IsOver S :=
  by
  obtain ⟨f', hf₁, hf₂⟩ := RationalMap.IsOver.exists_partialMap_over (S := S) (f := f.toRationalMap)
  obtain ⟨U, hU, hUl, hUr, e⟩ := PartialMap.toRationalMap_eq_iff.mp hf₂
  exact ⟨U, hU, hUr, by rw [IsOver, ← e]; infer_instance⟩

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru