English
A generalizing morphism which is locally of finite presentation is open on the base map.
Русский
Обобщающее отображение, локально конечной презентации которого является открытым отображение базового пространства.
LaTeX
$$$[\text{LocallyOfFinitePresentation}(f)] \land \text{GeneralizingMap}(f.base) \Rightarrow \text{IsOpenMap}(f.base).$$$
Lean4
/-- A generalizing morphism, locally of finite presentation is open. -/
@[stacks 01U1]
theorem isOpenMap_of_generalizingMap [LocallyOfFinitePresentation f] (hf : GeneralizingMap f.base) : IsOpenMap f.base :=
by
change topologically IsOpenMap f
wlog hY : ∃ R, Y = Spec R
· rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically IsOpenMap) Y.affineCover]
intro i
dsimp only [Scheme.Cover.pullbackHom]
refine this _ ?_ ⟨_, rfl⟩
exact
IsZariskiLocalAtTarget.of_isPullback (P := topologically GeneralizingMap) (iY := Y.affineCover.f i)
(IsPullback.of_hasPullback ..) hf
obtain ⟨R, rfl⟩ := hY
wlog hX : ∃ S, X = Spec S
· rw [IsZariskiLocalAtSource.iff_of_openCover (P := topologically IsOpenMap) X.affineCover]
intro i
refine this f _ _ ?_ ⟨_, rfl⟩
exact IsZariskiLocalAtSource.comp (P := topologically GeneralizingMap) hf _
obtain ⟨S, rfl⟩ := hX
obtain ⟨φ, rfl⟩ := Spec.map_surjective f
algebraize [φ.hom]
convert PrimeSpectrum.isOpenMap_comap_of_hasGoingDown_of_finitePresentation
· rwa [Algebra.HasGoingDown.iff_generalizingMap_primeSpectrumComap]
· apply (HasRingHomProperty.Spec_iff (P := @LocallyOfFinitePresentation)).mp inferInstance
