English
A constructed equivalence between function-field morphisms and rational maps remains valid under Over constructions.
Русский
Сопоставление между морфизмами по полю функций и рациональными картами сохраняется в конструкциях Over.
LaTeX
$$$\text{equivFunctionFieldOver}(X,Y,S) : {f:X.K-\text{morphism} \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 equivFunctionFieldOver [X.Over S] [Y.Over S] [IsIntegral X] [LocallyOfFiniteType (Y ↘ S)] :
{ f : Spec X.functionField ⟶ Y // f.IsOver S } ≃ { f : X ⤏ Y // f.IsOver S } :=
((Equiv.subtypeEquivProp (by simp only [Hom.isOver_iff]; rfl)).trans
(RationalMap.equivFunctionField (X ↘ S) (Y ↘ S))).trans
(Equiv.subtypeEquivProp (by ext f; rw [RationalMap.isOver_iff]))
