isClosedEmbedding_comap_fst — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem isClosedEmbedding_comap_fst : IsClosedEmbedding (comap (RingHom.fst R S)) :=
  (isClosedEmbedding_iff _).mpr
    ⟨isEmbedding_comap_of_surjective _ _ Prod.fst_surjective, by simp_rw [range_comap_fst, isClosed_zeroLocus]⟩

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