English
Under the same hypotheses as above, comap f yields a quotient map between spectra.
Русский
При тех же предпосылках comap f задаёт фактор-мэп между спектрами.
LaTeX
$$$$ \text{isQuotientMap_of_generalizingMap}(f) : \operatorname{Topology.IsQuotientMap}(\operatorname{comap} f). $$$$
Lean4
/-- If `f : Spec S → Spec R` is generalizing and surjective, the topology on `Spec R` is the
quotient topology induced by `f`. -/
theorem isQuotientMap_of_generalizingMap (h₂ : GeneralizingMap (comap f)) : Topology.IsQuotientMap (comap f) :=
by
rw [Topology.isQuotientMap_iff_isClosed]
refine ⟨h₁, fun s ↦ ⟨fun hs ↦ hs.preimage (comap f).continuous, fun hsc ↦ Set.image_preimage_eq s h₁ ▸ ?_⟩⟩
apply isClosed_image_of_stableUnderSpecialization _ _ hsc
rw [Set.image_preimage_eq s h₁, ← stableUnderGeneralization_compl_iff]
convert h₂.stableUnderGeneralization_image hsc.isOpen_compl.stableUnderGeneralization
rw [← Set.preimage_compl, Set.image_preimage_eq _ h₁]
