English
Characterization: x belongs to jacobson(I) iff for all y there exists z with z*y*x + z − 1 ∈ I.
Русский
Х принадлежит Jacobson(I) тогда и только тогда, когда для всех y существует z such that z·y·x + z − 1 ∈ I.
LaTeX
$$$x \in \operatorname{jacobson}(I) \iff \forall y, \exists z, \; z y x + z - 1 \in I$$$
Lean4
theorem mem_jacobson_iff {x : R} : x ∈ jacobson I ↔ ∀ y, ∃ z, z * y * x + z - 1 ∈ I :=
⟨fun hx y =>
by_cases
(fun hxy : I ⊔ span {y * x + 1} = ⊤ =>
let ⟨p, hpi, q, hq, hpq⟩ := Submodule.mem_sup.1 ((eq_top_iff_one _).1 hxy)
let ⟨r, hr⟩ := mem_span_singleton'.1 hq
⟨r, by
rw [mul_assoc, ← mul_add_one, hr, ← hpq, ← neg_sub, add_sub_cancel_right]
exact I.neg_mem hpi⟩)
fun hxy : I ⊔ span {y * x + 1} ≠ ⊤ =>
let ⟨M, hm1, hm2⟩ := exists_le_maximal _ hxy
suffices x ∉ M from (this <| mem_sInf.1 hx ⟨le_trans le_sup_left hm2, hm1⟩).elim
fun hxm =>
hm1.1.1 <|
(eq_top_iff_one _).2 <|
add_sub_cancel_left (y * x) 1 ▸ M.sub_mem (le_sup_right.trans hm2 <| subset_span rfl) (M.mul_mem_left _ hxm),
fun hx =>
mem_sInf.2 fun M ⟨him, hm⟩ =>
by_contradiction fun hxm =>
let ⟨y, i, hi, df⟩ := hm.exists_inv hxm
let ⟨z, hz⟩ := hx (-y)
hm.1.1 <|
(eq_top_iff_one _).2 <|
sub_sub_cancel (z * -y * x + z) 1 ▸
M.sub_mem
(by
rw [mul_assoc, ← mul_add_one, neg_mul, ← sub_eq_iff_eq_add.mpr df.symm, neg_sub, sub_add_cancel]
exact M.mul_mem_left _ hi) <|
him hz⟩
