English
The special linear Lie algebra sl_n(R) is not abelian when n > 1 and R is nontrivial.
Русский
Специальная линейная алгебра Ли sl_n(R) не абелева при n > 1 и R не тривиален.
LaTeX
$$$$ (1 < \#\mathrm{card}(n)) \land \text{Nontrivial}(R) \Rightarrow \neg \operatorname{IsLieAbelian}(\mathrm{sl}_n(R)). $$$$
Lean4
theorem sl_non_abelian [Fintype n] [Nontrivial R] (h : 1 < Fintype.card n) : ¬IsLieAbelian (sl n R) :=
by
rcases Fintype.exists_pair_of_one_lt_card h with ⟨i, j, hij⟩
let A := single i j hij (1 : R)
let B := single j i hij.symm (1 : R)
intro c
have c' : A.val * B.val = B.val * A.val := by rw [← sub_eq_zero, ← sl_bracket, c.trivial, ZeroMemClass.coe_zero]
simpa [A, B, Matrix.single, Matrix.mul_apply, hij.symm] using congr_fun (congr_fun c' i) i
