isClosed_comap_singleton_of_isIntegral

English

Same principle: an integral ring homomorphism yields a closed map on spectra; this is another presentation of the same fact.

Русский

Тот же принцип: интегральный гомоморфизм порождает замкнутое отображение на спектрах.

LaTeX

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

Lean4

theorem isClosed_comap_singleton_of_isIntegral (hf : f.IsIntegral) (x : PrimeSpectrum S)
    (hx : IsClosed ({ x } : Set (PrimeSpectrum S))) : IsClosed ({comap f x} : Set (PrimeSpectrum R)) := by
  simpa using isClosedMap_comap_of_isIntegral f hf _ hx

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