isClosed_of_stableUnderSpecialization_of_isConstructible

English

If s is stable under specialization and constructible, then s is closed in the Zariski topology.

Русский

Если множество s стабильно по специализации и конструктивно, то оно замкнуто в цариковской топологии.

LaTeX

$$$StableUnderSpecialization(s) \land IsConstructible(s) \Rightarrow IsClosed(s)$$$

Lean4

@[stacks 00I0 "(1)"]
theorem isClosed_of_stableUnderSpecialization_of_isConstructible {R : Type*} [CommRing R] {s : Set (PrimeSpectrum R)}
    (hs : StableUnderSpecialization s) (hs' : IsConstructible s) : IsClosed s :=
  by
  obtain ⟨S, _, f, rfl⟩ := exists_range_eq_of_isConstructible hs'
  exact isClosed_range_of_stableUnderSpecialization _ hs

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