The radicals of gl n K and sl n K

TauCeti/Algebra/Lie/GeneralLinear/Basic.lean identifies the centre of gl n R (the scalar matrices) and its derived ideal (sl n R), and shows that the two are complementary submodules as soon as the size of the matrices is invertible. This file proves the reductivity criterion itself, Mathlib's LieAlgebra.HasCentralRadical: over a field in which 2 ≠ 0, the solvable radical of gl n K is its centre. This makes the reductive vocabulary applicable to gl n, whose Killing form is degenerate.

The same structure shows that sl n K has trivial radical when 2 and the nonempty matrix size are nonzero. In characteristic zero this is registered as an instance, so Cartan's criterion makes the Killing-form API available by typeclass synthesis.

The proof is the structure of the Lie ideals of gl n K. The centre is always an abelian, hence solvable, ideal, so it is contained in the radical. For the other inclusion, every solvable ideal must consist of scalar matrices, and that is a consequence of the sharper statement TauCeti.slIdeal_le_of_notMem_center: a Lie ideal containing a single non-central matrix already contains all of sl n K. Since sl n K is perfect (TauCeti.lie_slIdeal_slIdeal) and nonzero as soon as there are two indices, it is not solvable, so no solvable ideal reaches outside the centre.

The ideal-generation argument runs through matrix units, and only two brackets are needed. Bracketing against a diagonal matrix rescales a matrix unit, ⁅diagonal d, Eₚq c⁆ = Eₚq ((dₚ - d_q) c) (TauCeti.lie_single_of_mem_diagonalCartan, from the diagonal Cartan subalgebra file), which extracts Eₚq from any diagonal element separating the indices p and q. Bracketing twice against Eⱼᵢ annihilates everything except one entry, (ad Eⱼᵢ)² x = Eⱼᵢ (-2 xᵢⱼ) (TauCeti.lie_single_lie_single_of_ne), which extracts Eⱼᵢ from any element with a nonzero (i, j) entry. A non-central matrix is either non-diagonal, and then the second bracket applies, or diagonal with two distinct entries, and then the first does. Once one off-diagonal matrix unit lies in the ideal, so does the difference of diagonal units E_bb - Eₐₐ = ⁅E_bₐ, Eₐb⁆, which separates b from every other index; that produces every unit in the row and the column of b, then every difference of diagonal units, and finally, by the first bracket again, all the remaining units.

Main results

• TauCeti.slIdeal_le_of_notMem_center: a Lie ideal of gl n K containing a non-central matrix contains sl n K; equivalently TauCeti.slIdeal_le_or_le_center, every Lie ideal of gl n K either contains sl n K or consists of scalar matrices.
• TauCeti.lie_slIdeal_slIdeal: sl n R is perfect, ⁅sl n R, sl n R⁆ = sl n R, whenever 2 is invertible in R, whence TauCeti.not_isSolvable_slIdeal: it is not solvable when R is nontrivial and there are at least two indices.
• TauCeti.radical_matrix_eq_center and TauCeti.hasCentralRadical_matrix: gl n K is reductive, its radical being its centre.
• TauCeti.hasTrivialRadical_sl: sl n K has trivial radical when 2 and the nonempty matrix size are nonzero; the characteristic-zero case is a named instance.

Implementation notes

The hypothesis (2 : K) ≠ 0 is genuinely needed, and not an artefact of the bracket computations: in gl 2 (ZMod 2) the span of E₁₂ and the identity matrix is a Lie ideal containing a non-central element but not E₂₁, and there sl 2 (ZMod 2) is nilpotent, so it is a solvable ideal strictly larger than the centre. No invertibility of the size of the matrices is needed, however: the statement is proved uniformly in the index type, the case of at most one index being the abelian one, where the radical and the centre are both everything.

Only the results about ideals are stated over a field, because the generation argument divides by an arbitrary nonzero matrix entry. The two bracket identities in Basic.lean need only a ring, and perfectness of sl n R — which divides by 2 alone — is stated over a commutative ring in which 2 is a unit, non-solvability adding only Nontrivial R; the radical computation specialises these to a field.

The bracket against a diagonal matrix comes from TauCeti.lie_single_of_mem_diagonalCartan. The matrix-unit bracket identities live alongside the other ring-level computations in TauCeti/Algebra/Lie/GeneralLinear/Basic.lean.

References

• J. Dixmier, Enveloping Algebras, AMS GSM 11 (1996), Section 1.6 (reductive Lie algebras).
• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Springer GTM 9 (1972), Section 1.2 (the ideals of the classical linear Lie algebras).

Matrix units inside a Lie ideal

theorem TauCeti.single_mem_of_diagonal_mem {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (I : LieIdeal K (Matrix n n K)) {d : n → K} (hd : Matrix.diagonal d ∈ I) {p q : n} (hpq : d p ≠ d q) (c : K) : Matrix.single p q c ∈ I

A diagonal element of a Lie ideal separating two indices contributes their matrix unit.

theorem TauCeti.single_mem_of_apply_ne_zero {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (I : LieIdeal K (Matrix n n K)) (htwo : 2 ≠ 0) {x : Matrix n n K} (hx : x ∈ I) {i j : n} (hij : i ≠ j) (hxij : x i j ≠ 0) (c : K) : Matrix.single j i c ∈ I

An element of a Lie ideal with a nonzero off-diagonal entry contributes the transposed matrix unit there.

theorem TauCeti.slIdeal_le_of_single_mem {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (I : LieIdeal K (Matrix n n K)) (htwo : 2 ≠ 0) {a b : n} (hab : a ≠ b) (hmem : Matrix.single a b 1 ∈ I) : slIdeal K n ≤ I

One off-diagonal matrix unit generates sl n K: a Lie ideal of gl n K containing Eₐb for some a ≠ b contains every trace-zero matrix.

theorem TauCeti.slIdeal_le_of_notMem_center {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (I : LieIdeal K (Matrix n n K)) (htwo : 2 ≠ 0) {x : Matrix n n K} (hxI : x ∈ I) (hx : x ∉ LieAlgebra.center K (Matrix n n K)) : slIdeal K n ≤ I

A Lie ideal of gl n K containing a non-central matrix contains sl n K.

theorem TauCeti.slIdeal_le_or_le_center {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (I : LieIdeal K (Matrix n n K)) (htwo : 2 ≠ 0) : slIdeal K n ≤ I ∨ I ≤ LieAlgebra.center K (Matrix n n K)

The Lie ideals of gl n K are the scalar ones and those containing sl n K.

sl n K is perfect, hence not solvable

theorem TauCeti.lie_slIdeal_slIdeal {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (htwo : IsUnit 2) : ⁅slIdeal R n, slIdeal R n⁆ = slIdeal R n

sl n R is perfect whenever 2 is invertible in R: ⁅sl n R, sl n R⁆ = sl n R.

Each off-diagonal matrix unit is Eₚq c = ⁅Eₚₚ - E_qq, Eₚq (t c)⁆ for an inverse t of 2, and each difference of diagonal units is Eₚₚ c - E_qq c = ⁅Eₚq c, E_qₚ⁆; all four factors have trace zero.

theorem TauCeti.slIdeal_ne_bot {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] [Nontrivial n] [Nontrivial R] : slIdeal R n ≠ ⊥

sl n R is nonzero over a nontrivial ring as soon as there are two indices.

theorem TauCeti.not_isSolvable_slIdeal {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] [Nontrivial n] [Nontrivial R] (htwo : IsUnit 2) : ¬LieAlgebra.IsSolvable ↥(slIdeal R n)

sl n R is not solvable when 2 is invertible in a nontrivial R and there are at least two indices: it is perfect and nonzero, so its derived series is constant.

The radical of gl n K

theorem TauCeti.radical_matrix_eq_center {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (htwo : 2 ≠ 0) : LieAlgebra.radical K (Matrix n n K) = LieAlgebra.center K (Matrix n n K)

The radical of gl n K is its centre, for any field in which 2 ≠ 0: gl n K is reductive.

Every solvable Lie ideal consists of scalar matrices, since an ideal containing a non-central matrix contains the non-solvable sl n K (TauCeti.slIdeal_le_of_notMem_center), and conversely the centre is itself a solvable ideal.

theorem TauCeti.hasCentralRadical_matrix {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (htwo : 2 ≠ 0) : LieAlgebra.HasCentralRadical K (Matrix n n K)

gl n K is reductive, for any field in which 2 ≠ 0.

instance TauCeti.instHasCentralRadicalMatrixOfCharZero_tauCeti {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] [CharZero K] : LieAlgebra.HasCentralRadical K (Matrix n n K)

Over a field of characteristic zero — the setting of the reductive structure theory — gl n K is reductive with no side hypothesis.

Semisimplicity of the special linear Lie algebra

theorem TauCeti.hasTrivialRadical_sl (K : Type u_3) [Field K] (n : Type u_4) [Fintype n] [DecidableEq n] (htwo : 2 ≠ 0) (hn : Nonempty n → ↑(Fintype.card n) ≠ 0) : LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.SpecialLinear.sl n K)

The special linear Lie algebra has trivial radical. If 2 and, for nonempty n, the cardinality of n are nonzero, a solvable ideal of sl n maps to a solvable ideal of gl n, hence lies in the scalar matrices. Its image also lies in the complementary derived ideal sl n, so the original ideal vanishes.

instance TauCeti.instHasTrivialRadicalSl (K : Type u_3) [Field K] (n : Type u_4) [Fintype n] [DecidableEq n] [CharZero K] : LieAlgebra.HasTrivialRadical K ↥(LieAlgebra.SpecialLinear.sl n K)

In characteristic zero, sl n has trivial radical.