English
For any ring hom f:R→S, the morphism Spec.map f is IsSeparated, i.e., a closed immersion in the diagonal sense.
Русский
Для любого кольцевого гомоморфизма f:R→S отображение Spec.map f является IsSeparated: диагональ выступает как замкнутое погружение.
LaTeX
$$$\forall (R,S:\text{CommRingCat}) (f:R\to S),\; \text{IsSeparated}(\text{Spec.map } f).$$$
Lean4
/-- Let `Q` be a property of ring maps that is stable under localization.
Then if the associated property of scheme morphisms holds for `f`, `Q` holds on all stalks. -/
theorem stalkMap
(hQ :
∀ {R S : Type u} [CommRing R] [CommRing S] (f : R →+* S) (_ : Q f) (J : Ideal S) (_ : J.IsPrime),
Q (Localization.localRingHom _ J f rfl))
(hf : P f) (x : X) : Q (f.stalkMap x).hom :=
by
have hQi := (HasRingHomProperty.isLocal_ringHomProperty P).respectsIso
wlog h : IsAffine X ∧ IsAffine Y generalizing X Y f
· obtain ⟨U, hU, hfx, _⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open Y) (Opens.mem_top <| f.base x)
obtain ⟨V, hV, hx, e⟩ := Opens.isBasis_iff_nbhd.mp (isBasis_affine_open X) (show x ∈ f ⁻¹ᵁ U from hfx)
rw [← hQi.arrow_mk_iso_iff (Scheme.Hom.resLEStalkMap f e ⟨x, hx⟩)]
exact this (IsZariskiLocalAtSource.resLE _ hf) _ ⟨hV, hU⟩
obtain ⟨hX, hY⟩ := h
wlog hXY : ∃ R S, Y = Spec R ∧ X = Spec S generalizing X Y
· have : Q ((X.isoSpec.inv ≫ f ≫ Y.isoSpec.hom).stalkMap (X.isoSpec.hom.base x)).hom :=
by
refine this ?_ (X.isoSpec.hom.base x) inferInstance inferInstance ?_
· rwa [P.cancel_left_of_respectsIso, P.cancel_right_of_respectsIso]
· use Γ(Y, ⊤), Γ(X, ⊤)
rw [Scheme.stalkMap_comp, Scheme.stalkMap_comp, CommRingCat.hom_comp, hQi.cancel_right_isIso, CommRingCat.hom_comp,
hQi.cancel_left_isIso] at this
have heq : (X.isoSpec.inv.base (X.isoSpec.hom.base x)) = x := by simp
rwa [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapIsoOfEq f heq)] at this
obtain ⟨R, S, rfl, rfl⟩ := hXY
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
rw [hQi.arrow_mk_iso_iff (Scheme.arrowStalkMapSpecIso φ _)]
rw [Spec_iff (P := P)] at hf
apply hQ _ hf
