isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing

English

Let R be a Noetherian Jacobson ring and x be a point of the prime spectrum Spec(R). Then the following are equivalent: the singleton {x} is open; {x} is closed and open (clopen); {x} is closed and stable under generalization (i.e. x is both a minimal prime and a maximal ideal).

Русский

Пусть R — кольцо Безуверенного типа (Noetherian) и Якобсона; рассмотрим точку x в спектре примел Spec(R). Тогда выполняются взаимнооднозначные условия: множество {x} открыто; {x} замкнуто и открыто (clopen); {x} замкнуто и стабильно по общему обобщению (то есть x является и минимальным примаром, и максимальным идеалом).

LaTeX

$$$\\text{Open}({x}) \\iff \\text{Clopen}({x}) \\iff (\\text{Closed}({x}) \\land \\text{StableUnderGeneralization}({x}))$$$

Lean4

/-- If `R` is both Noetherian and Jacobson, then the following are equivalent for `x : Spec R`:
1. `{x}` is open (i.e. `x` is an isolated point)
2. `{x}` is clopen
3. `{x}` is both closed and stable under generalization
  (i.e. `x` is both a minimal prime and a maximal ideal)
-/
theorem isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing [IsNoetherianRing R] [IsJacobsonRing R]
    (x : PrimeSpectrum R) :
    List.TFAE [IsOpen { x }, IsClopen { x }, IsClosed { x } ∧ StableUnderGeneralization { x }] :=
  by
  tfae_have 1 → 2
    | h =>
      by
      obtain ⟨y, rfl : y = x, h'⟩ := exists_isClosed_singleton_of_isJacobsonRing _ h ⟨x, Set.mem_singleton x⟩
      exact ⟨h', h⟩
  tfae_have 2 → 3
    | h => ⟨h.isClosed, h.isOpen.stableUnderGeneralization⟩
  tfae_have 3 → 1
    | ⟨h₁, h₂⟩ => by
      rw [isClosed_singleton_iff_isMaximal, ← isMax_iff] at h₁
      suffices { x } = (⋃ p ∈ {p : PrimeSpectrum R | IsMin p ∧ p ≠ x}, closure { p })ᶜ
        by
        rw [this, isOpen_compl_iff]
        refine Set.Finite.isClosed_biUnion ?_ (fun _ _ ↦ isClosed_closure)
        exact (finite_setOf_isMin R).subset fun x h ↦ h.1
      ext p
      simp only [Set.mem_singleton_iff, ne_eq, Set.mem_setOf_eq, Set.compl_iUnion, Set.mem_iInter, Set.mem_compl_iff,
        and_imp, ← specializes_iff_mem_closure, ← le_iff_specializes, not_imp_not]
      constructor
      · rintro rfl _ _
        rw [stableUnderGeneralization_singleton, ← isMin_iff] at h₂
        exact h₂.eq_of_le
      · intro hp
        apply h₁.eq_of_ge
        obtain ⟨q, hq, hq'⟩ := Ideal.exists_minimalPrimes_le (J := p.asIdeal) bot_le
        exact (hp ⟨q, hq.1.1⟩ (isMin_iff.mpr hq) hq').ge.trans hq'
  tfae_finish

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