English
Jac(I) equals I iff I is the infimum of some set of maximal ideals.
Русский
Jac(I) равен I тогда и только тогда, когда I является инфимумом некоторого семейства максимальных идеалов.
LaTeX
$$$\operatorname{jacobson}(I) = I \iff \exists M : \text{Set}(\text{Ideal}(R)), I = \bigcap M \text{ and each } J\in M \text{ maximal}$$$
Lean4
/-- An ideal equals its Jacobson radical iff it is the intersection of a set of maximal ideals.
Allowing the set to include ⊤ is equivalent, and is included only to simplify some proofs. -/
theorem eq_jacobson_iff_sInf_maximal :
I.jacobson = I ↔ ∃ M : Set (Ideal R), (∀ J ∈ M, IsMaximal J ∨ J = ⊤) ∧ I = sInf M :=
by
use fun hI => ⟨{J : Ideal R | I ≤ J ∧ J.IsMaximal}, ⟨fun _ hJ => Or.inl hJ.right, hI.symm⟩⟩
rintro ⟨M, hM, hInf⟩
refine le_antisymm (fun x hx => ?_) le_jacobson
rw [hInf, mem_sInf]
intro I hI
rcases hM I hI with is_max | is_top
· exact (mem_sInf.1 hx) ⟨le_sInf_iff.1 (le_of_eq hInf) I hI, is_max⟩
· exact is_top.symm ▸ Submodule.mem_top
