English
The Jacobson radical of a two-sided ideal is two-sided: I.jacobson is two-sided.
Русский
Радикал Якобиана двухсоставного идеала является двухсторонним.
LaTeX
$$$I^{\mathrm{jacobson}} \text{ is two-sided}$$$
Lean4
/-- The Jacobson radical of a two-sided ideal is two-sided. -/
instance {I : Ideal R} [I.IsTwoSided] : I.jacobson.IsTwoSided where
-- Proof generalized from
-- https://ysharifi.wordpress.com/2022/08/16/the-jacobson-radical-definition-and-basic-results/
mul_mem_of_left {x} r
xJ := by
apply mem_sInf.mpr
intro 𝔪 𝔪_mem
by_cases r𝔪 : r ∈ 𝔪
· apply 𝔪.smul_mem _ r𝔪
let 𝔪₀ : Ideal R := Submodule.comap (DistribMulAction.toLinearMap R (S := Rᵐᵒᵖ) R (.op r)) 𝔪
suffices x ∈ 𝔪₀ by simpa [𝔪₀] using this
have I𝔪₀ : I ≤ 𝔪₀ := fun i iI => 𝔪_mem.left (I.mul_mem_right _ iI)
have 𝔪₀_maximal : IsMaximal 𝔪₀ :=
by
refine isMaximal_iff.mpr ⟨fun h => r𝔪 (by simpa [𝔪₀] using h), fun J b 𝔪₀J b𝔪₀ bJ => ?_⟩
let K : Ideal R := Ideal.span {b * r} ⊔ 𝔪
have ⟨s, y, y𝔪, sbyr⟩ :=
mem_span_singleton_sup.mp <|
mul_mem_left _ r <|
(isMaximal_iff.mp 𝔪_mem.right).right K (b * r) le_sup_right b𝔪₀ (mem_sup_left <| mem_span_singleton_self _)
have : 1 - s * b ∈ 𝔪₀ := by
rw [mul_one, add_comm, ← eq_sub_iff_add_eq] at sbyr
rw [sbyr, ← mul_assoc] at y𝔪
simp [𝔪₀, sub_mul, y𝔪]
have : 1 - s * b + s * b ∈ J := by apply add_mem (𝔪₀J this) (J.mul_mem_left _ bJ)
simpa using this
exact mem_sInf.mp xJ ⟨I𝔪₀, 𝔪₀_maximal⟩
