English
For a qc morphism f, the base map is closed if and only if it is specializing.
Русский
Для квази-компактного морфизма f базовая карта закрыта тогда и только тогда, когда она является специализирующейся.
LaTeX
$$$IsClosedMap(f.base) \\iff SpecializingMap(f.base)$ under qc-conditions$$
Lean4
@[stacks 01K9]
theorem isClosedMap_iff_specializingMap (f : X ⟶ Y) [QuasiCompact f] : IsClosedMap f.base ↔ SpecializingMap f.base :=
by
refine ⟨fun h ↦ h.specializingMap, fun H ↦ ?_⟩
wlog hY : ∃ R, Y = Spec R
· change topologically (@IsClosedMap) f
rw [IsZariskiLocalAtTarget.iff_of_openCover (P := topologically @IsClosedMap) Y.affineCover]
intro i
haveI hqc : QuasiCompact (Y.affineCover.pullbackHom f i) :=
IsZariskiLocalAtTarget.of_isPullback (.of_hasPullback _ _) inferInstance
refine this (Y.affineCover.pullbackHom f i) ?_ ⟨_, rfl⟩
exact IsZariskiLocalAtTarget.of_isPullback (P := topologically @SpecializingMap) (.of_hasPullback _ _) H
obtain ⟨S, rfl⟩ := hY
clear * - H
intro Z hZ
replace H := hZ.stableUnderSpecialization.image H
wlog hX : ∃ R, X = Spec R
· obtain ⟨R, g, hg⟩ := compactSpace_iff_exists.mp ((quasiCompact_over_affine_iff f).mp inferInstance)
have inst : QuasiCompact (g ≫ f) := HasAffineProperty.iff_of_isAffine.mpr (by infer_instance)
have := this _ (g ≫ f) (g.base ⁻¹' Z) (hZ.preimage g.continuous)
simp_rw [Scheme.comp_base, TopCat.comp_app, ← Set.image_image, Set.image_preimage_eq _ hg] at this
exact this H ⟨_, rfl⟩
obtain ⟨R, rfl⟩ := hX
obtain ⟨φ, rfl⟩ := Spec.homEquiv.symm.surjective f
exact PrimeSpectrum.isClosed_image_of_stableUnderSpecialization φ.hom Z hZ H
