isClosedMap_comap_of_isIntegral — Mathlib

English

If f: R → S is an integral ring homomorphism, then comap f is a closed map on the prime spectra.

Русский

Если f: R → S — интегральный гомоморфизм, тогда comap f — замкнутая отображение спектров простых идей.

LaTeX

$$$$ \text{IsClosedMap}( \operatorname{comap} f ) \text{ if } f \text{ is integral}. $$$$

Lean4

theorem isClosedMap_comap_of_isIntegral (hf : f.IsIntegral) : IsClosedMap (comap f) :=
  by
  refine fun s hs ↦ isClosed_image_of_stableUnderSpecialization _ _ hs ?_
  rintro _ y e ⟨x, hx, rfl⟩
  algebraize [f]
  obtain ⟨q, hq₁, hq₂, hq₃⟩ :=
    Ideal.exists_ideal_over_prime_of_isIntegral y.asIdeal x.asIdeal ((le_iff_specializes _ _).mpr e)
  refine ⟨⟨q, hq₂⟩, ((le_iff_specializes _ ⟨q, hq₂⟩).mp hq₁).mem_closed hs hx, PrimeSpectrum.ext hq₃⟩

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