The centre and the derived ideal of gl n R

The general linear Lie algebra gl n R is Matrix n n R with the commutator bracket. It is the basic reductive — as opposed to semisimple — example: it splits as its centre plus its derived ideal as soon as Fintype.card n is invertible in R. This file identifies both pieces.

The centre of gl n R is the scalar matrices, for any commutative ring R and any finite index type. The derived ideal ⁅gl n R, gl n R⁆ is the trace-zero ideal sl n R, again over any commutative ring and any finite index type: one inclusion is the vanishing of the trace of a commutator, and the other writes a trace-zero matrix as a combination of the commutators Eᵢⱼ = ⁅Eᵢᵢ, Eᵢⱼ⁆ (for i ≠ j) and Eᵢᵢ - Eⱼⱼ = ⁅Eᵢⱼ, Eⱼᵢ⁆.

The two pieces are complementary whenever the size of the matrices is invertible in R: the intersection is cut out by Fintype.card n * r = 0, and the projection onto the centre divides the trace by Fintype.card n. Under that hypothesis gl n R is the direct sum of its centre and its derived ideal, which is the linear half of the reductivity criterion radical = center. Only this sufficiency is proved here; the hypothesis is not necessary in general, since for an empty index type gl n R is the zero Lie algebra and the decomposition is vacuous. It cannot simply be dropped either: over ZMod p the identity matrix of gl p (ZMod p) has trace zero, so there the centre sits inside the derived ideal and the two are not complementary.

Main definitions

• Ado.slIdeal R n: the trace-zero matrices, as a LieIdeal R (Matrix n n R). Mathlib's LieAlgebra.SpecialLinear.sl n R is the same subspace packaged only as a Lie subalgebra, and Ado.slIdeal_toLieSubalgebra_eq_sl identifies the two.

Main results

• Ado.lie_single_self_sub_single_self_single and Ado.lie_single_lie_single_of_ne: over any ring, ⁅Eₚₚ - E_qq, Eₚq c⁆ = Eₚq (2c) for p ≠ q, and (ad Eⱼᵢ)² x = Eⱼᵢ (-2 xᵢⱼ) for i ≠ j; these produce matrix units inside a Lie ideal of gl n R.
• Ado.mem_of_trace_eq_zero_of_single_mem: a submodule of gl n R containing the off-diagonal matrix units and the differences of the diagonal ones contains every trace-zero matrix. This is the spanning core shared by the derived-ideal computation below and by the ideal-generation argument of TauCeti/Algebra/Lie/GeneralLinear/Radical.lean.
• Ado.mem_center_matrix_iff: an element of gl n R is central exactly when it is a scalar matrix; Ado.one_mem_center_matrix records that the identity is central, Ado.center_matrix_toSubmodule_eq_span_one records the centre as the span of 1, and Ado.center_matrix_eq_top records that gl n R is abelian when n has at most one element.
• Ado.derivedSeries_one_eq_slIdeal: the derived ideal of gl n R is Ado.slIdeal R n, so by Ado.mem_slIdeal_iff it consists of the trace-zero matrices, and Ado.derivedSeries_one_toLieSubalgebra_eq_sl reads this as LieAlgebra.SpecialLinear.sl n R.
• LieAlgebra.SpecialLinear.mem_sl_iff: membership in LieAlgebra.SpecialLinear.sl n R is the vanishing of the trace.
• Ado.isCompl_center_derivedSeries_one_matrix: when Fintype.card n is invertible in R, the centre and the derived ideal are complementary submodules of gl n R.
• Ado.exists_sl_add_smul_one_eq: every matrix is a trace-zero matrix plus a scalar matrix when the cardinality is a unit, with the empty case included.
• Ado.derivedSeries_one_matrix_ne_top: for nonempty n over a nontrivial R, gl n R is not perfect.
• Ado.not_hasTrivialRadical_matrix: for nonempty n over a nontrivial R, gl n R is not semisimple, since its centre is then a nonzero abelian ideal (Ado.center_matrix_ne_bot).

Implementation notes

Every result about gl n R is stated over an arbitrary commutative ring R; no field, characteristic, or algebraic closure hypothesis is used. The bundled complement carries invertibility of Fintype.card n as an Invertible hypothesis, while its elementwise consequence asks only that the cardinality be a unit when the index type is nonempty. Two groups of declarations ask for less: the matrix-unit bracket identities and the spanning theorem for trace-zero matrices need only a ring, and the decomposition of a trace-zero matrix into matrix units needs only an additive commutative group, no multiplication at all.

Mathlib does not register LieRing.ofAssociativeRing as a global instance, so, as in Mathlib/Algebra/Lie/Matrix.lean, it is a local instance here.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Springer GTM 9 (1972), Section 1.2 (the classical linear Lie algebras).

Trace-zero matrices as sums of matrix units

theorem Ado.mem_of_trace_eq_zero_of_single_mem {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Ring R] {N : Submodule R (Matrix n n R)} (hoff : ∀ {p q : n}, p ≠ q → ∀ (c : R), Matrix.single p q c ∈ N) (hdiag : ∀ (p q : n) (c : R), Matrix.single p p c - Matrix.single q q c ∈ N) {A : Matrix n n R} (hA : A.trace = 0) : A ∈ N

Trace-zero matrices are generated by the off-diagonal matrix units and the differences of the diagonal ones. A submodule of gl n R containing every Eₚq c with p ≠ q and every Eₚₚ c - E_qq c contains every trace-zero matrix.

This is the spanning fact behind both halves of the reductive structure of gl n R: the derived ideal is sl n R because each of those generators is a commutator (Ado.derivedSeries_one_eq_slIdeal), and a Lie ideal containing a non-central element contains all of them, hence all of sl n R.

Matrix units as commutators

@[simp]

theorem Ado.lie_single_single {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Ring R] (a b i j : n) (c d : R) : ⁅Matrix.single a b c, Matrix.single i j d⁆ = (if b = i then Matrix.single a j (c * d) else 0) - if j = a then Matrix.single i b (d * c) else 0

The commutator of two single-entry matrices is the difference of the two possible composites.

theorem Ado.lie_single_self_single_of_ne {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Ring R] {i j : n} (hij : i ≠ j) (c : R) : ⁅Matrix.single i i 1, Matrix.single i j c⁆ = Matrix.single i j c

An off-diagonal matrix unit is a commutator: Eᵢⱼ = ⁅Eᵢᵢ, Eᵢⱼ⁆ when i ≠ j.

theorem Ado.lie_single_single_eq_sub {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Ring R] (i j : n) (c : R) : ⁅Matrix.single i j c, Matrix.single j i 1⁆ = Matrix.single i i c - Matrix.single j j c

A difference of diagonal matrix units is a commutator: Eᵢᵢ - Eⱼⱼ = ⁅Eᵢⱼ, Eⱼᵢ⁆.

theorem Ado.lie_single_self_sub_single_self_single {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Ring R] {p q : n} (hpq : p ≠ q) (c : R) : ⁅Matrix.single p p 1 - Matrix.single q q 1, Matrix.single p q c⁆ = Matrix.single p q (2 * c)

A difference of diagonal matrix units doubles the matrix unit between them.

theorem Ado.lie_single_lie_single_of_ne {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [Ring R] {i j : n} (hij : i ≠ j) (x : Matrix n n R) : ⁅Matrix.single j i 1, ⁅Matrix.single j i 1, x⁆⁆ = Matrix.single j i (-(2 * x i j))

Bracketing twice against an off-diagonal matrix unit isolates the transposed entry.

The centre of gl n R

theorem Ado.mem_center_matrix_iff {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R} : A ∈ LieAlgebra.center R (Matrix n n R) ↔ ∃ (r : R), A = r • 1

The centre of gl n R is the scalar matrices. The Lie centre and the ring centre agree here, since a commutator vanishes exactly when the two factors commute.

This is deliberately not a simp lemma: simp rewrites the left-hand side with LieModule.mem_maxTrivSubmodule to ∀ X, ⁅X, A⁆ = 0, so tagging it @[simp] violates simpNF.

@[simp]

theorem Ado.center_matrix_eq_top {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] [Subsingleton n] : LieAlgebra.center R (Matrix n n R) = ⊤

With at most one index, every matrix is central.

theorem Ado.one_mem_center_matrix (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] : 1 ∈ LieAlgebra.center R (Matrix n n R)

The identity matrix is central in gl n R.

theorem Ado.center_matrix_toSubmodule_eq_span_one (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] : ↑(LieAlgebra.center R (Matrix n n R)) = R ∙ 1

The centre of gl n R is the R-span of the identity matrix.

The special linear ideal

def Ado.slIdeal (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] : LieIdeal R (Matrix n n R)

The trace-zero matrices, as a Lie ideal of gl n R.

Mathlib's LieAlgebra.SpecialLinear.sl n R is the same subspace, packaged only as a Lie subalgebra; Ado.slIdeal_toLieSubalgebra_eq_sl identifies the two. The ideal packaging is what the derived series of gl n R lives in.

Equations

• Ado.slIdeal R n = { carrier := {A : Matrix n n R | A.trace = 0}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem := ⋯ }

@[simp]

theorem Ado.mem_slIdeal_iff {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R} : A ∈ slIdeal R n ↔ A.trace = 0

theorem Ado.slIdeal_toLieSubalgebra_eq_sl (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] : LieIdeal.toLieSubalgebra R (Matrix n n R) (slIdeal R n) = LieAlgebra.SpecialLinear.sl n R

The special linear ideal of gl n R is Mathlib's special linear subalgebra.

@[simp]

theorem LieAlgebra.SpecialLinear.mem_sl_iff {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] {A : Matrix n n R} : A ∈ sl n R ↔ A.trace = 0

Membership in Mathlib's special linear Lie algebra sl n R is the vanishing of the trace.

The derived ideal of gl n R

theorem Ado.derivedSeries_one_eq_slIdeal (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] : LieAlgebra.derivedSeries R (Matrix n n R) 1 = slIdeal R n

The derived ideal of gl n R is the special linear ideal: ⁅gl n R, gl n R⁆ = sl n R.

One inclusion is the vanishing of the trace of a commutator. For the other, a trace-zero matrix is the sum of its off-diagonal matrix units Eᵢⱼ (Aᵢⱼ), commutators by Ado.lie_single_self_single_of_ne, and of the differences Eᵢᵢ (Aᵢᵢ) - E₀₀ (Aᵢᵢ), commutators by Ado.lie_single_single_eq_sub; the discrepancy between the two sums is E₀₀ (trace A), which vanishes. For an empty index type both sides are the zero ideal.

theorem Ado.derivedSeries_one_toLieSubalgebra_eq_sl (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] : LieIdeal.toLieSubalgebra R (Matrix n n R) (LieAlgebra.derivedSeries R (Matrix n n R) 1) = LieAlgebra.SpecialLinear.sl n R

The derived ideal of gl n R is Mathlib's special linear Lie algebra sl n R.

gl n R is the direct sum of its centre and its derived ideal

theorem Ado.isCompl_center_derivedSeries_one_matrix (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] [Invertible ↑(Fintype.card n)] : IsCompl ↑(LieAlgebra.center R (Matrix n n R)) ↑(LieAlgebra.derivedSeries R (Matrix n n R) 1)

When the size of the matrices is invertible in R, the centre and the derived ideal of gl n R are complementary: gl n R = R·1 ⊕ sl n R. This is the linear half of the reductivity criterion radical = center, made concrete for gl n R.

The invertibility hypothesis cannot simply be dropped: in gl p (ZMod p) the identity matrix has trace 0, so there the centre is contained in the derived ideal and the two are not complementary. It is not necessary either, since for an empty index type gl n R is the zero Lie algebra.

theorem Ado.exists_sl_add_smul_one_eq {R : Type u_1} {n : Type u_2} [DecidableEq n] [Fintype n] [CommRing R] (hn : Nonempty n → IsUnit ↑(Fintype.card n)) (A : Matrix n n R) : ∃ (X : ↥(LieAlgebra.SpecialLinear.sl n R)) (r : R), ↑X + r • 1 = A

Every square matrix is the sum of a trace-zero matrix and a scalar matrix, as soon as the rank is a unit in R. This is the elementwise form of Ado.isCompl_center_derivedSeries_one_matrix; the separate rank-zero branch is why the hypothesis is an implication rather than a global invertibility assumption.

theorem Ado.derivedSeries_one_matrix_ne_top (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] [Nonempty n] [Nontrivial R] : LieAlgebra.derivedSeries R (Matrix n n R) 1 ≠ ⊤

gl n R is not perfect: for nonempty n over a nontrivial ring its derived ideal misses the diagonal matrix unit Eᵢᵢ, whose trace is 1.

gl n R is not semisimple, for nonempty n over a nontrivial ring

theorem Ado.center_matrix_ne_bot (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] [Nonempty n] [Nontrivial R] : LieAlgebra.center R (Matrix n n R) ≠ ⊥

The centre of gl n R is nonzero: it contains the identity matrix.

theorem Ado.not_hasTrivialRadical_matrix (R : Type u_1) (n : Type u_2) [DecidableEq n] [Fintype n] [CommRing R] [Nonempty n] [Nontrivial R] : ¬LieAlgebra.HasTrivialRadical R (Matrix n n R)

For nonempty n over a nontrivial ring, gl n R is not semisimple: its centre is then a nonzero abelian ideal, so its radical is nonzero. This is why the highest-weight theory of gl n R cannot be read off Mathlib's IsKilling machinery, and has to be developed through the reductive decomposition instead.