stableUnderSpecialization_image_iff

English

For Z closed in PrimeSpectrum(S) and a ring hom f, StableUnderSpecialization of comap f '' Z is equivalent to IsClosed (comap f '' Z).

Русский

Для Z, замкнутого в PrimeSpectrum(S), и кольцевого гомоморфизма f, выписывается эквивалентность: StableUnderSpecialization comap f''Z ⇔ IsClosed comap f''Z.

LaTeX

$$$$ \operatorname{StableUnderSpecialization}( \operatorname{comap} f '' Z ) \iff \operatorname{IsClosed}( \operatorname{comap} f '' Z ). $$$$

Lean4

theorem stableUnderSpecialization_image_iff (Z : Set (PrimeSpectrum S)) (hZ : IsClosed Z) :
    StableUnderSpecialization (comap f '' Z) ↔ IsClosed (comap f '' Z) :=
  ⟨isClosed_image_of_stableUnderSpecialization f Z hZ, fun h ↦ h.stableUnderSpecialization⟩

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