English
A strengthened equivalence: I is fixed by jacobson iff there exists a family M with a specific maximality condition and I equals the infimum over M.
Русский
Усиленное равенство: I фиксируется Якобианом тогда, когда существует Familie M и I равен инфимума по M, удовлетворяющему условиям максимальности.
LaTeX
$$$\operatorname{jacobson}(I) = I \iff \exists M : \mathrm{Set}(\mathrm{Ideal}(R)), (\forall J \in M, \forall K, J < K \rightarrow K = \top) \land I = \bigcap M$$$
Lean4
theorem eq_jacobson_iff_sInf_maximal' :
I.jacobson = I ↔ ∃ M : Set (Ideal R), (∀ J ∈ M, ∀ (K : Ideal R), J < K → K = ⊤) ∧ I = sInf M :=
eq_jacobson_iff_sInf_maximal.trans
⟨fun h =>
let ⟨M, hM⟩ := h
⟨M,
⟨fun J hJ K hK => Or.recOn (hM.1 J hJ) (fun h => h.1.2 K hK) fun h => eq_top_iff.2 (le_of_lt (h ▸ hK)), hM.2⟩⟩,
fun h =>
let ⟨M, hM⟩ := h
⟨M, ⟨fun J hJ => Or.recOn (Classical.em (J = ⊤)) (fun h => Or.inr h) fun h => Or.inl ⟨⟨h, hM.1 J hJ⟩⟩, hM.2⟩⟩⟩
