English
Let R → S be a ring hom between commutative rings. If the induced map on prime spectra comap is an embedding and the ring hom is surjective on stalks, then the corresponding map Spec.map f is a preimmersion.
Русский
Пусть f: R → S — гомоморфизм колец между коммутативными кольцами. Если индуцированное отображение на спектрах PrimeSpectrum.comap f.hom является вложением и отображение на stalks сюръективно, тогда Spec.map f — предиммерсион.
LaTeX
$$$\bigl(\operatorname{IsEmbedding}(\operatorname{PrimeSpectrum}.comap f.tHom)\bigr) \land \bigl( f.tHom.SurjectiveOnStalks \bigr) \Rightarrow \operatorname{IsPreimmersion}(\operatorname{Spec.map} f)$$$
Lean4
theorem mk_Spec_map {R S : CommRingCat.{u}} {f : R ⟶ S} (h₁ : IsEmbedding (PrimeSpectrum.comap f.hom))
(h₂ : f.hom.SurjectiveOnStalks) : IsPreimmersion (Spec.map f) :=
(Spec_map_iff f).mpr ⟨h₁, h₂⟩
