equivFunctionField — Mathlib

English

There is a bijection between S-morphisms Spec K(X) ⟶ Y over S and S-rational maps X ⤏ Y over S, respecting structure.

Русский

Существуют взаимно однозначные соответствия между S-морфизмами Spec K(X) ⟶ Y над S и S-рациональными картами X ⤏ Y над S, с сохранением структуры.

LaTeX

$$$\{f:Spec X.functionField \to Y \mid f.IsOver S\} \simeq \{f:X\!\curvearrowright\! Y \mid f.IsOver S\}$$$

Lean4

/-- Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and `X` is integral,
`S`-morphisms `Spec K(X) ⟶ Y` correspond bijectively to `S`-rational maps from `X` to `Y`.
-/
noncomputable def equivFunctionField [IsIntegral X] [LocallyOfFiniteType sY] :
    { f : Spec X.functionField ⟶ Y // f ≫ sY = X.fromSpecStalk _ ≫ sX } ≃
      { f : X ⤏ Y // f.compHom sY = sX.toRationalMap }
    where
  toFun
    f :=
    ⟨.ofFunctionField sX sY f f.2,
      PartialMap.toRationalMap_eq_iff.mpr
        ⟨_, PartialMap.dense_domain _, le_rfl, le_top, by simp [PartialMap.ofFromSpecStalk_comp]⟩⟩
  invFun
    f :=
    ⟨f.1.fromFunctionField, by
      obtain ⟨f, hf⟩ := f
      obtain ⟨f, rfl⟩ := f.exists_rep
      simpa [fromFunctionField_toRationalMap] using congr(RationalMap.fromFunctionField $hf)⟩
  left_inv f := Subtype.ext (RationalMap.fromFunctionField_ofFunctionField _ _ _ _)
  right_inv
    f :=
    Subtype.ext
      (RationalMap.eq_of_fromFunctionField_eq (ofFunctionField sX sY f.1.fromFunctionField _) f
        (RationalMap.fromFunctionField_ofFunctionField _ _ _ _))

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