English
Let X, Y be S-schemes and x ∈ X. If φ is a morphism Spec 𝒪_{X,x} ⟶ Y such that φ composed with the Y-structure equals the corresponding base change, then φ can be spread to an S-morphism f: U ⟶ Y for some affine neighborhood U of x, provided Y is locally of finite type over S and X is germ-injective at x. Moreover, φ equals U.fromSpecStalkOfMem x hxU ≫ f and f ≫ sY = U.ι ≫ sX.
Русский
Пусть X, Y — S-схемы и x ∈ X. Пусть φ : Spec 𝒪_{X,x} ⟶ Y удовлетворяет совместимости с структурой над S. Тогда φ можно распрости́ть до S-морфизма f: U ⟶ Y на некоторой окрестности U точки x, если Y локально кончен по типу над S и X гом-инъектируется в x. Тогда φ = U.fromSpecStalkOfMem x hxU ≫ f и f ∘ s_Y = U.ι ∘ s_X.
LaTeX
$$$\exists U : X.Opens,\; x ∈ U,\; f : U.toScheme ⟶ Y,\; φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ s_Y = U.ι ≫ s_X$$$
Lean4
/-- Given `S`-schemes `X Y`, a point `x : X`, and a `S`-morphism `φ : Spec 𝒪_{X, x} ⟶ Y`,
we may spread it out to an `S`-morphism `f : U ⟶ Y`
provided that `Y` is locally of finite type over `S` and
`X` is "germ-injective" at `x` (e.g. when it's integral or locally Noetherian).
TODO: The condition on `X` is unnecessary when `Y` is locally of finite presentation.
-/
theorem spread_out_of_isGermInjective' [LocallyOfFiniteType sY] {x : X} [X.IsGermInjectiveAt x]
(φ : Spec (X.presheaf.stalk x) ⟶ Y) (h : φ ≫ sY = X.fromSpecStalk x ≫ sX) :
∃ (U : X.Opens) (hxU : x ∈ U) (f : U.toScheme ⟶ Y), φ = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX :=
by
have := spread_out_of_isGermInjective sX sY ?_ (Scheme.stalkClosedPointTo φ) ?_
· simpa only [Scheme.Spec_stalkClosedPointTo_fromSpecStalk] using this
· rw [← Scheme.comp_base_apply, h, Scheme.comp_base_apply, Scheme.fromSpecStalk_closedPoint]
· apply Spec.map_injective
rw [← cancel_mono (S.fromSpecStalk _)]
simpa only [Spec.map_comp, Category.assoc, Scheme.Spec_map_stalkMap_fromSpecStalk,
Scheme.Spec_stalkClosedPointTo_fromSpecStalk_assoc, Scheme.Spec_map_stalkSpecializes_fromSpecStalk]
