English
A variant of the Jacobson ring criterion using a supremum over maximal ideals with a different ordering of the maximal elements.
Русский
Вариант критерия Якобсонова кольца через супермножество максимальных идеалов с иной упорядоченностью.
LaTeX
$$isJacobsonRing_iff_sInf_maximal' : IsJacobsonRing R ↔ ∀ {I}, I.IsPrime → ∃ M, (∀ J ∈ M, ∀ (K), J < K → K = ⊤) ∧ I = sInf M$$
Lean4
/-- A variant of `isJacobsonRing_iff_sInf_maximal` with a different spelling of "maximal or `⊤`". -/
theorem isJacobsonRing_iff_sInf_maximal' :
IsJacobsonRing R ↔
∀ {I : Ideal R}, I.IsPrime → ∃ M : Set (Ideal R), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M :=
⟨fun H _I h => eq_jacobson_iff_sInf_maximal'.1 (H.out h.isRadical), fun H =>
isJacobsonRing_iff_prime_eq.2 fun _P hP => eq_jacobson_iff_sInf_maximal'.2 (H hP)⟩
