English
For any two-sided ideal I of a ring R, the Jacobson radical commutes with the matrix construction: (I.matrix n).jacobson = I.jacobson.matrix n.
Русский
Для любой двусторонней идеал I кольца R радикал Якобсона коммутирует с матричной конструкцией: (I.matrix n).jacobson = I.jacobson.matrix n.
LaTeX
$$$$ (I^{\\mathrm{matrix}}_n).\\mathrm{jacobson} = I^{\\mathrm{jacobson}}_{\\mathrm{matrix}}^{(n)}. $$$$
Lean4
/-- For any two-sided ideal $I ≤ R$, we have $J(Mₙ(I)) = Mₙ(J(I))$. -/
theorem jacobson_matrix (I : TwoSidedIdeal R) : (I.matrix n).jacobson = I.jacobson.matrix n :=
by
apply le_antisymm
· apply jacobson_matrix_le
· change asIdeal (I.matrix n).jacobson ≥ asIdeal (I.jacobson.matrix n)
simp [asIdeal_jacobson, asIdeal_matrix, Ideal.matrix_jacobson_le]
