vanishingIdeal_isClosed_isIrreducible

English

The vanishing ideals of closed irreducible sets exhaust all prime ideals.

Русский

Идеалы исчезновения замкнутых ирредуцируемых множеств порождают все простые идеалы.

LaTeX

$$$\\operatorname{vanishingIdeal}\\bigl( \\mathrm{closed\\;irreducible\\;sets} \\bigr) = \\{P \\mid P.IsPrime\\}$$$

Lean4

theorem vanishingIdeal_isClosed_isIrreducible :
    vanishingIdeal (R := R) '' {s | IsClosed s ∧ IsIrreducible s} = {P | P.IsPrime} :=
  by
  refine (subset_antisymm ?_ ?_).trans vanishingIdeal_isIrreducible
  · exact Set.image_mono fun _ ↦ And.right
  rintro _ ⟨s, hs, rfl⟩
  exact ⟨closure s, ⟨isClosed_closure, hs.closure⟩, vanishingIdeal_closure s⟩

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