stableUnderSpecialization_range_iff

English

For a ring hom f, the range of comap f is stable under specialization if and only if it is closed.

Русский

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

LaTeX

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

Lean4

@[stacks 00HY]
theorem stableUnderSpecialization_range_iff :
    StableUnderSpecialization (Set.range (comap f)) ↔ IsClosed (Set.range (comap f)) :=
  ⟨isClosed_range_of_stableUnderSpecialization f, fun h ↦ h.stableUnderSpecialization⟩

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