English
If R ⊆ S satisfies Going Down and is of finite presentation, then the map Spec(S) → Spec(R) given by comap(algebraMap R S) is an open map.
Русский
Пусть R ⊆ S удовлетворяют свойству Going Down и имеют конечную презентацию; отображение Spec(S) → Spec(R), заданное comap(algebraMap R S), открытое.
LaTeX
$$$[\\text{Algebra R S}] \\ [\\text{Algebra.HasGoingDown R S}] \\ [\\text{Algebra.FinitePresentation R S}] \\\\ \\text{IsOpenMap}(\\operatorname{comap}(\\text{algebraMap } R S))$$
Lean4
@[stacks 00I1]
theorem isOpenMap_comap_of_hasGoingDown_of_finitePresentation [Algebra R S] [Algebra.HasGoingDown R S]
[Algebra.FinitePresentation R S] : IsOpenMap (comap (algebraMap R S)) :=
by
rw [isBasis_basic_opens.isOpenMap_iff]
rintro _ ⟨_, ⟨f, rfl⟩, rfl⟩
exact
isOpen_of_stableUnderGeneralization_of_isConstructible
((basicOpen f).2.stableUnderGeneralization.image
(Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap.mp ‹_›))
(isConstructible_comap_image (RingHom.finitePresentation_algebraMap.mpr ‹_›) isConstructible_basicOpen)
