isClosed_singleton_iff_isMaximal — Mathlib

English

A singleton {x} is closed if and only if the associated ideal x.asIdeal is maximal.

Русский

Единственный замкнутый компонент {x} существует тогда и только тогда, когда x.asIdeal является максимальным.

LaTeX

$$$\\operatorname{IsClosed}({x}) \\iff x.asIdeal \\text{ is maximal}$$$

Lean4

theorem isClosed_singleton_iff_isMaximal (x : PrimeSpectrum R) :
    IsClosed ({ x } : Set (PrimeSpectrum R)) ↔ x.asIdeal.IsMaximal :=
  by
  rw [← closure_subset_iff_isClosed, ← zeroLocus_vanishingIdeal_eq_closure, vanishingIdeal_singleton]
  constructor <;> intro H
  · rcases x.asIdeal.exists_le_maximal x.2.1 with ⟨m, hm, hxm⟩
    exact (congr_arg asIdeal (@H ⟨m, hm.isPrime⟩ hxm)) ▸ hm
  · exact fun p hp ↦ PrimeSpectrum.ext (H.eq_of_le p.2.1 hp).symm

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