of_singleton_maximalSpectrum — Mathlib

English

If the maximal spectrum of a ring is a singleton, then the ring is local.

Русский

Если множество максимальных спектров кольца является единичным, тогда кольцо локально.

LaTeX

$$of_singleton_maximalSpectrum: [Subsingleton (MaximalSpectrum R)] [Nonempty (MaximalSpectrum R)] ⇒ IsLocalRing R$$

Lean4

/-- If the maximal spectrum of a ring is a singleton, then the ring is local. -/
theorem of_singleton_maximalSpectrum [Subsingleton (MaximalSpectrum R)] [Nonempty (MaximalSpectrum R)] :
    IsLocalRing R :=
  let m := Classical.arbitrary (MaximalSpectrum R)
  .of_unique_max_ideal ⟨m.asIdeal, m.isMaximal, fun I hI ↦ MaximalSpectrum.mk.inj <| Subsingleton.elim ⟨I, hI⟩ m⟩

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