English
Let R be a commutative semiring with R nontrivial. Then the following are equivalent: (i) R is not local; (ii) the maximal spectrum of R is nontrivial; (iii) R has two distinct maximal ideals.
Русский
Пусть R — коммутативное полускольцо (полное кольцо) не тривиальное. Тогда следующее эквивалентны: R не локально; максимальный спектр R не тривиален; существуют две различные максимальные идеалы R.
LaTeX
$$$\\neg \\mathrm{IsLocalRing}(R) \\iff \\mathrm{Nontrivial}(\\mathrm{MaximalSpectrum}(R)) \\iff \\exists \\mathfrak m_1 \\mathfrak m_2 : \\mathrm{Ideal}(R), \\; \\mathfrak m_1.IsMaximal \\land \\mathfrak m_2.IsMaximal \\land \\mathfrak m_1 \\neq \\mathfrak m_2$$$
Lean4
/-- The following conditions are equivalent for a commutative (semi)ring `R`:
* `R` is not local,
* the maximal spectrum of `R` is nontrivial,
* `R` has two distinct maximal ideals.
-/
theorem not_isLocalRing_tfae {R : Type*} [CommSemiring R] [Nontrivial R] :
List.TFAE
[¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ m₁ m₂ : Ideal R, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂] :=
by
tfae_have 1 → 2
| h => not_subsingleton_iff_nontrivial.mp fun _ ↦ h of_singleton_maximalSpectrum
tfae_have 2 → 3
| ⟨⟨m₁, hm₁⟩, ⟨m₂, hm₂⟩, h⟩ => ⟨m₁, m₂, ⟨hm₁, hm₂, fun _ ↦ h (by congr)⟩⟩
tfae_have 3 → 1
| ⟨m₁, m₂, ⟨hm₁, hm₂, h⟩⟩ => fun _ ↦ h <| (eq_maximalIdeal hm₁).trans (eq_maximalIdeal hm₂).symm
tfae_finish
