fromFunctionField

Mathlib.AlgebraicGeometry.RationalMap

URI: https://scilib.ai/kg/mathlib#AlgebraicGeometry.Scheme.RationalMap.fromFunctionField

Lean4

/-- A rational map restricts to a map from `Spec K(X)`. -/
noncomputable def fromFunctionField [IrreducibleSpace X] (f : X ⤏ Y) : Spec X.functionField ⟶ Y :=
  by
  refine Quotient.lift PartialMap.fromFunctionField ?_ f
  intro f g ⟨W, hW, hWl, hWr, e⟩
  have : f.restrict W hW hWl = g.restrict W hW hWr := by ext1; rfl; rw [e]; simp
  rw [← f.fromFunctionField_restrict hW hWl, this, g.fromFunctionField_restrict]

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

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

Разделы

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

Аффилиация

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