subsingleton_primeSpectrum_of_mem_minimalPrimes

English

If p is a minimal prime of R and S is the localization of R away from p, then the prime spectrum of S is a singleton.

Русский

Если p — минимальный простой в R, и S — локализация R вдали от p, то спектр простых идеалов S состоит из единственного элемента.

LaTeX

$$Subsingleton (PrimeSpectrum S)$$

Lean4

theorem subsingleton_primeSpectrum_of_mem_minimalPrimes {R : Type*} [CommSemiring R] (p : Ideal R)
    (hp : p ∈ minimalPrimes R) (S : Type*) [CommSemiring S] [Algebra R S] [IsLocalization.AtPrime S p (hp := hp.1.1)] :
    Subsingleton (PrimeSpectrum S) :=
  have := hp.1.1
  have : Unique (Set.Iic (⟨p, hp.1.1⟩ : PrimeSpectrum R)) :=
    ⟨⟨⟨p, hp.1.1⟩, by exact fun ⦃x⦄ a ↦ a⟩, fun i ↦
      Subtype.ext <| PrimeSpectrum.ext <| (minimalPrimes_eq_minimals (R := R) ▸ hp).eq_of_le i.1.2 i.2⟩
  (IsLocalization.AtPrime.primeSpectrumOrderIso S p).subsingleton

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