English
A standard basis matrix with a single potentially nonzero entry x belongs to the Jacobson radical of I.matrix n whenever x ∈ I.jacobson.
Русский
Стандартная базисная матрица с единственной возможно ненулевой записью x принадлежит радикалу Якобсона матрицы I, если x ∈ I.jacobson.
LaTeX
$$∀ x ∈ I.jacobson, ∀ i j, single i j x ∈ (I.matrix n).jacobson$$
Lean4
/-- A standard basis matrix is in $J(Mₙ(I))$
as long as its one possibly non-zero entry is in $J(I)$. -/
theorem single_mem_jacobson_matrix (I : Ideal R) :
∀ x ∈ I.jacobson, ∀ (i j : n), single i j x ∈ (I.matrix n).jacobson := by
-- Proof generalized from example 8 in
-- https://ysharifi.wordpress.com/2022/08/16/the-jacobson-radical-basic-examples/
simp_rw [Ideal.mem_jacobson_iff]
intro x xIJ p q M
have ⟨z, zMx⟩ := xIJ (M q p)
let N : Matrix n n R := 1 - ∑ i, single i q (if i = q then 1 - z else (M i p) * x * z)
use N
intro i j
obtain rfl | qj := eq_or_ne q j
· by_cases iq : i = q
· simp [iq, N, zMx, single, mul_apply, sum_apply, ite_and, sub_mul]
· convert I.mul_mem_left (-M i p * x) zMx
simp [iq, N, single, mul_apply, sum_apply, ite_and, sub_mul]
simp [sub_add, mul_add, mul_sub, mul_assoc]
· simp [N, qj, sum_apply, mul_apply]
