isQuotientMap_of_specializingMap — Mathlib

English

If comap f is surjective and f is a generalizing map, then comap f is a quotient map.

Русский

Если comap f сюръективен и f является общеподобной общепредставляющей картой, то comap f — это фактор-карта топологий.

LaTeX

$$$$ \text{isQuotientMap_of_generalizingMap}(f) : \operatorname{Topology.IsQuotientMap}(\operatorname{comap} f). $$$$

Lean4

/-- If `f : Spec S → Spec R` is specializing and surjective, the topology on `Spec R` is the
quotient topology induced by `f`. -/
theorem isQuotientMap_of_specializingMap (h₂ : SpecializingMap (comap f)) : Topology.IsQuotientMap (comap f) :=
  by
  rw [Topology.isQuotientMap_iff_isClosed]
  exact
    ⟨h₁, fun s ↦
      ⟨fun hs ↦ hs.preimage (comap f).continuous, fun hsc ↦
        Set.image_preimage_eq s h₁ ▸
          isClosed_image_of_stableUnderSpecialization _ _ hsc
            (h₂.stableUnderSpecialization_image hsc.stableUnderSpecialization)⟩⟩

Похожие утверждения