English
Let R, S be local rings with a local morphism f: R → S. Then the induced map on spectra sends the closed point of Spec S to the closed point of Spec R.
Русский
Пусть R, S — локальные кольца и имеется локальное отображение f: R → S. Тогда индуцированное отображение на спектрах отправляет закрытую точку Spec S в закрытую точку Spec R.
LaTeX
$$$(\\mathrm{Spec}\\, f).base(\\text{closedPoint } S) = \\text{closedPoint } R$$$
Lean4
instance subcanonical_zariskiTopology : zariskiTopology.Subcanonical :=
by
apply GrothendieckTopology.Subcanonical.of_isSheaf_yoneda_obj
intro X
rw [Presieve.isSheaf_pretopology]
rintro Y S hS x hx
obtain ⟨(𝓤 : OpenCover Y), rfl⟩ := exists_cover_of_mem_pretopology hS
let e : Y ⟶ X :=
𝓤.glueMorphisms (fun j => x (𝓤.f _) (.mk _)) <| by
intro i j
apply hx
exact Limits.pullback.condition
refine ⟨e, ?_, ?_⟩
· rintro Z e ⟨j⟩
dsimp [e]
rw [𝓤.ι_glueMorphisms]
· intro e' h
apply 𝓤.hom_ext
intro j
rw [𝓤.ι_glueMorphisms]
exact h (𝓤.f j) (.mk j)
