isCompact_isOpen_iff_ideal — Mathlib

English

For a subset s of Spec(R), s is compact and open if and only if there exists a finitely generated ideal I of R such that s is the complement of the zero locus of I.

Русский

Для подмножества s в спектре Р, s компактно и открыто тогда и только тогда, когда существует конечносогеный идеал I в R такой, что s является дополнением к нуль-радикалу I.

LaTeX

$$$$ \text{IsCompact}(s) \wedge \text{IsOpen}(s) \iff \exists I \,(I.FG) \wedge (\sqrt{(0)} = \operatorname{zeroLocus}(I))^c. $$$$

Lean4

theorem isCompact_isOpen_iff_ideal {s : Set (PrimeSpectrum R)} :
    IsCompact s ∧ IsOpen s ↔ ∃ I : Ideal R, I.FG ∧ (zeroLocus I)ᶜ = s :=
  by
  rw [isCompact_isOpen_iff]
  exact ⟨fun ⟨s, e⟩ ↦ ⟨.span s, ⟨s, rfl⟩, by simpa using e⟩, fun ⟨I, ⟨s, hs⟩, e⟩ ↦ ⟨s, by simpa [hs.symm] using e⟩⟩

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