zeroLocus_empty_iff_eq_top — Mathlib

English

If s ⊆ t are subsets of the spectrum, then vanishingIdeal t ≤ vanishingIdeal s.

Русский

Если s ⊆ t — подмножества спектра, то vanishingIdeal(t) ≤ vanishingIdeal(s).

LaTeX

$$$ s \subseteq t \Rightarrow \operatorname{vanishingIdeal}(t) \le \operatorname{vanishingIdeal}(s) $$$

Lean4

theorem zeroLocus_empty_iff_eq_top {I : Ideal R} : zeroLocus (I : Set R) = ∅ ↔ I = ⊤ :=
  by
  constructor
  · contrapose!
    intro h
    rcases Ideal.exists_le_maximal I h with ⟨M, hM, hIM⟩
    exact ⟨⟨M, hM.isPrime⟩, hIM⟩
  · rintro rfl
    apply zeroLocus_empty_of_one_mem
    trivial

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