English
For an IsJacobsonRing R, every ideal I satisfies radical(I) = jacobson(I).
Русский
Для кольца IsJacobsonRing R каждый идеал I удовлетворяет radical(I) = jacobson(I).
LaTeX
$$$\\text{Ideal.radical}(I) = I.jacobson$ for IsJacobsonRing R.$$
Lean4
/-- A ring `R` is Jacobson if and only if for every prime ideal `I`,
`I` can be written as the infimum of some collection of maximal ideals.
Allowing ⊤ in the set `M` of maximal ideals is equivalent, but makes some proofs cleaner. -/
theorem isJacobsonRing_iff_sInf_maximal :
IsJacobsonRing R ↔ ∀ {I : Ideal R}, I.IsPrime → ∃ M : Set (Ideal R), (∀ J ∈ M, IsMaximal J ∨ J = ⊤) ∧ 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)⟩
