English
Let X, Y, S be schemes over S, and x ∈ X, y ∈ Y lying over s ∈ S. Suppose we have a diagram of S-schemes with a morphism φ between the stalks at x and y that is compatible with the structure maps to S. If Y is locally of finite type over S and X is germ-injective at x, then φ extends to an S-morphism on an open neighborhood U of x: there exists U ⊆ X open with x ∈ U and f: U → Y such that Spec φ = U →^? Y in a compatible way and the maps to S agree. In particular, we can express this as there exists U, hxU, f with Spec.map φ = U.fromSpecStalkOfMem x hxU ≫ f and f ≫ sY = U.ι ≫ sX.
Русский
Пусть X, Y, S — расслоения над S и точки x ∈ X, y ∈ Y над s ∈ S. Пусть дан диаграммный набор S-видов схем и линейное отображение φ между локальными кольцами 𝒪_{X,x} и 𝒪_{Y,y}, удовлетворяющее совместимости с отображениями к S. Если Y локально конечного типа над S, а X гом-инъекта в точке x, то φ распространяется на преобразование S-морфизма на открытом окне U вокруг x: существует открытое подмножество U ⊆ X, содержащее x, и f: U → Y такое, что сопоставление φ эквивалентно U.fromSpecStalkOfMem x hxU ≫ f и локальная карта к S согласуется с f. Формально: ∃ U, hxU, f такие, что Spec.map φ = U.fromSpecStalkOfMem x hxU ≫ f и f ≫ sY = U.ι ≫ sX.
LaTeX
$$$\exists U : X.Opens,\; x ∈ U,\; f : U.toScheme ⟶ Y,\; Spec.map(φ) \;∘\; Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ∘ f \wedge\ f \circ s_Y = U.ι \circ s_X$$$
Lean4
/-- Given `S`-schemes `X Y` and points `x : X` `y : Y` over `s : S`.
Suppose we have the following diagram of `S`-schemes
```
Spec 𝒪_{X, x} ⟶ X
|
Spec(φ)
↓
Spec 𝒪_{Y, y} ⟶ Y
```
Then the map `Spec(φ)` spreads out to an `S`-morphism on an open subscheme `U ⊆ X`,
```
Spec 𝒪_{X, x} ⟶ U ⊆ X
| |
Spec(φ) |
↓ ↓
Spec 𝒪_{Y, y} ⟶ 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.
-/
@[stacks 0BX6]
theorem spread_out_of_isGermInjective [LocallyOfFiniteType sY] {x : X} [X.IsGermInjectiveAt x] {y : Y}
(e : sX.base x = sY.base y) (φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x)
(h : sY.stalkMap y ≫ φ = S.presheaf.stalkSpecializes (Inseparable.of_eq e).specializes ≫ sX.stalkMap x) :
∃ (U : X.Opens) (hxU : x ∈ U) (f : U.toScheme ⟶ Y),
Spec.map φ ≫ Y.fromSpecStalk y = U.fromSpecStalkOfMem x hxU ≫ f ∧ f ≫ sY = U.ι ≫ sX :=
by
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
(isBasis_affine_open S).exists_subset_of_mem_open (Set.mem_univ (sX.base x)) isOpen_univ
have hyU : sY.base y ∈ U := e ▸ hxU
obtain ⟨_, ⟨V : Y.Opens, hV, rfl⟩, hyV, iVU⟩ := (isBasis_affine_open Y).exists_subset_of_mem_open hyU (sY ⁻¹ᵁ U).2
have : sY.appLE U V iVU ≫ Y.presheaf.germ V y hyV ≫ φ = sX.app U ≫ X.presheaf.germ (sX ⁻¹ᵁ U) x hxU :=
by
rw [Scheme.Hom.appLE, Category.assoc, Y.presheaf.germ_res_assoc, ← Scheme.stalkMap_germ_assoc, h]
simp
obtain ⟨W, hxW, φ', i, hW, h₁, h₂⟩ :=
exists_lift_of_germInjective (R := Γ(S, U)) (A := Γ(Y, V)) (U := sX ⁻¹ᵁ U) (x := x) hxU
(Y.presheaf.germ _ y hyV ≫ φ) (sY.appLE U V iVU) (sX.app U)
(LocallyOfFiniteType.finiteType_of_affine_subset ⟨_, hU⟩ ⟨_, hV⟩ _) this
refine ⟨W, hxW, W.toSpecΓ ≫ Spec.map φ' ≫ hV.fromSpec, ?_, ?_⟩
·
rw [W.fromSpecStalkOfMem_toSpecΓ_assoc x hxW, ← Spec.map_comp_assoc, ← h₁, Spec.map_comp, Category.assoc, ←
IsAffineOpen.fromSpecStalk, IsAffineOpen.fromSpecStalk_eq_fromSpecStalk]
· simp only [Category.assoc]
rw [← IsAffineOpen.Spec_map_appLE_fromSpec sY hU hV iVU, ← Spec.map_comp_assoc, ← h₂, ← Scheme.Hom.appLE, ←
hW.isoSpec_hom, IsAffineOpen.Spec_map_appLE_fromSpec sX hU hW i, ← Iso.eq_inv_comp,
IsAffineOpen.isoSpec_inv_ι_assoc]
