isClosedEmbedding_comap_snd — Mathlib

English

The map from PrimeSpectrum R to PrimeSpectrum (R×S) given by comap with snd is a closed embedding; its image is a closed subset of Spec(R×S).

Русский

Отображение из PrimeSpectrum(R) в PrimeSpectrum(R×S) через snd является замкнутым вложением; образ — замкнутое подмножество спектра R×S.

LaTeX

$$$$\\text{IsClosedEmbedding}(\\mathrm{comap}(\\mathrm{snd}_{R,S})).$$$$

Lean4

theorem isClosedEmbedding_comap_snd : IsClosedEmbedding (comap (RingHom.snd R S)) :=
  (isClosedEmbedding_iff _).mpr
    ⟨isEmbedding_comap_of_surjective _ _ Prod.snd_surjective, by simp_rw [range_comap_snd, isClosed_zeroLocus]⟩

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