isClosed_image_of_stableUnderSpecialization

English

If f is a ring hom with surjective comap and a specializing map, then comap f is a quotient map of topologies.

Русский

Если f — гомоморфизм колец, отображение comap f соответствует сюръективному отображению и является фактор-мэп топологий.

LaTeX

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

Lean4

theorem isClosed_image_of_stableUnderSpecialization (Z : Set (PrimeSpectrum S)) (hZ : IsClosed Z)
    (hf : StableUnderSpecialization (comap f '' Z)) : IsClosed (comap f '' Z) :=
  by
  obtain ⟨I, rfl⟩ := (PrimeSpectrum.isClosed_iff_zeroLocus_ideal Z).mp hZ
  refine (isClosed_iff_zeroLocus _).mpr ⟨I.comap f, le_antisymm ?_ fun p hp ↦ ?_⟩
  · rintro _ ⟨q, hq, rfl⟩
    exact Ideal.comap_mono hq
  · obtain ⟨q, hqI, hq, hqle⟩ := p.asIdeal.exists_ideal_comap_le_prime I hp
    exact hf ((le_iff_specializes ⟨q.comap f, inferInstance⟩ p).mp hqle) ⟨⟨q, hq⟩, hqI, rfl⟩

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