The root space decomposition of gl n R

Let gl n R = Matrix n n R carry the commutator bracket and let diagonalCartan R n be its diagonal Cartan subalgebra. This file computes the weight spaces of gl n R for that Cartan subalgebra: over a domain, a matrix lies in the root space of a functional χ exactly when it is supported on the pairs (a, b) with εₐ - ε_b = χ. Since the matrix unit Eₐ_b lies in the root space of εₐ - ε_b and every matrix is a sum of matrix units, those root spaces span gl n R (TauCeti.iSup_rootSpace_glWeightSub_eq_top), and hence so do all the root spaces (TauCeti.iSup_rootSpace_eq_top); those two spanning statements need no hypothesis on R beyond commutativity. Over a domain Mathlib's LieModule.iSupIndep_genWeightSpace makes the latter supremum direct, exhibiting gl n R as the direct sum of its root spaces.

The pairs (a, b) do not index those root spaces injectively, so the finer decomposition of gl n R into the matrix-unit lines R · Eₐ_b is not the root space decomposition. Every εₐ - ε_a is the zero functional, and the zero root space contains every diagonal matrix rather than just the line R · Eₐ_a: that is TauCeti.glWeightSub_self together with TauCeti.single_mem_rootSpace, and over a Noetherian base Mathlib's LieAlgebra.rootSpace_zero_eq identifies the zero root space with the whole diagonal Cartan subalgebra, as it does for any Cartan subalgebra. In characteristic two εᵢ - εⱼ = εⱼ - εᵢ, so the pairs (i, j) and (j, i) share a root space as well. Only for i ≠ j, over a domain, and away from characteristic two, is a root space the line spanned by a single matrix unit (TauCeti.rootSpace_glWeightSub_eq_span).

Everything rests on one computation, TauCeti.lie_apply_of_mem_diagonalCartan: the adjoint action of a diagonal matrix scales the (a, b) entry by A a a - A b b. Equivalently ad A is the diagonal operator on the matrix-unit basis with entries A a a - A b b (TauCeti.toEnd_diagonalCartan_eq_toLin_diagonal), which is what puts Mathlib's theory of diagonal operators at our disposal: over a reduced ring the generalized weight spaces are honest simultaneous eigenspaces (TauCeti.rootSpace_diagonalCartan_eq_weightSpace), and the diagonal Cartan is split, so triangularizability holds over an arbitrary commutative ring with no algebraic closure hypothesis (TauCeti.instIsTriangularizableMatrixDiagonalCartan).

Main results

• TauCeti.toEnd_diagonalCartan_eq_toLin_diagonal: ad A is a diagonal operator in the matrix-unit basis, for A in the diagonal Cartan subalgebra.
• TauCeti.rootSpace_diagonalCartan_eq_weightSpace: over a reduced ring, the generalized weight spaces are honest simultaneous eigenspaces.
• TauCeti.mem_rootSpace_diagonalCartan_iff: over a domain, a matrix lies in the root space of χ exactly when its (a, b) entry vanishes for every pair with εₐ - ε_b ≠ χ.
• TauCeti.iSup_rootSpace_glWeightSub_eq_top: over any commutative ring, gl n R is spanned by the root spaces of the weights εₐ - ε_b; TauCeti.iSup_rootSpace_eq_top is the same statement indexed by the weights themselves, where each root space occurs once and the supremum is the root space decomposition.
• TauCeti.instIsTriangularizableMatrixDiagonalCartan: over any commutative ring, gl n R is triangularizable over its diagonal Cartan subalgebra, so Mathlib's weight space machinery applies over any field, not only an algebraically closed one.
• TauCeti.rootSpace_glWeightSub_eq_span: over a domain and away from characteristic two the root space of εᵢ - εⱼ, for i ≠ j, is the line spanned by the matrix unit Eᵢⱼ, and TauCeti.finrank_rootSpace_glWeightSub_eq_one records the resulting dimension over a field.
• TauCeti.rootSpace_diagonalCartan_eq_bot: over a domain, a functional that is not one of the εₐ - ε_b has trivial root space, so the roots of gl n R are exactly the εᵢ - εⱼ with i ≠ j (TauCeti.exists_glWeightSub_eq_of_rootSpace_ne_bot).

Implementation notes

The spanning statements TauCeti.iSup_rootSpace_glWeightSub_eq_top and TauCeti.iSup_rootSpace_eq_top, the diagonal-operator identification TauCeti.toEnd_diagonalCartan_eq_toLin_diagonal and triangularizability hold over an arbitrary commutative ring. Collapsing a generalized eigenspace of a diagonal operator to the eigenspace needs [IsReduced R], and no more: that is the hypothesis of TauCeti.rootSpace_diagonalCartan_eq_weightSpace. Everything that then computes a root space, rather than merely placing an element in one, assumes [IsDomain R], which is what cancels a nonzero difference of weights.

The hypothesis (2 : R) ≠ 0 in TauCeti.rootSpace_glWeightSub_eq_span is not an artefact. In characteristic two εᵢ - εⱼ = εⱼ - εᵢ, so Eᵢⱼ and Eⱼᵢ share a root space and that root space is a plane rather than a line. The statements that do not separate εᵢ - εⱼ from εⱼ - εᵢ, in particular TauCeti.mem_rootSpace_diagonalCartan_iff and TauCeti.iSup_rootSpace_glWeightSub_eq_top, need no such hypothesis.

LieAlgebra.IsKilling is unavailable for gl n R: whenever R is nontrivial and n is nonempty the identity matrix is central, hence a nonzero element of the radical of the Killing form, so that form is degenerate. With LieAlgebra.IsKilling goes all of Mathlib's LieAlgebra.IsKilling.rootSystem machinery, including finrank_rootSpace_eq_one; the analogues here are proved from scratch. See the module documentation of TauCeti.Algebra.Lie.GeneralLinear.DiagonalCartan.

References

This implements the root space decomposition of gl n supporting the diagonal Cartan targets of Layer 9 (and the Layer 1 root space vocabulary, transported to the reductive case) of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

The adjoint action of the diagonal Cartan as a diagonal operator

theorem TauCeti.toEnd_diagonalCartan_eq_toLin_diagonal {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (A : ↥(diagonalCartan R n)) : (LieModule.toEnd R (↥(diagonalCartan R n)) (Matrix n n R)) A = (Matrix.toLin (Matrix.stdBasis R n n) (Matrix.stdBasis R n n)) (Matrix.diagonal fun (p : n × n) => ↑A p.1 p.1 - ↑A p.2 p.2)

ad A is a diagonal operator for A in the diagonal Cartan subalgebra: in the matrix-unit basis it is the diagonal matrix whose (a, b) entry is A a a - A b b. This identification is what makes Mathlib's theory of diagonal operators, in particular Matrix.iSup_eigenspace_toLin_diagonal_eq_top and Matrix.maxGenEigenspace_toLin_diagonal_eq_eigenspace, available for the adjoint action.

Triangularizability: the diagonal Cartan of gl n R is split

instance TauCeti.instIsTriangularizableMatrixDiagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] : LieModule.IsTriangularizable R (↥(diagonalCartan R n)) (Matrix n n R)

gl n R is triangularizable over its diagonal Cartan subalgebra: the matrix units are a simultaneous eigenbasis. No field, characteristic or algebraic closure hypothesis is needed, so this is the statement that the diagonal Cartan subalgebra is split.

The weight spaces of gl n R

theorem TauCeti.rootSpace_diagonalCartan_eq_weightSpace {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [IsReduced R] (χ : Module.Dual R ↥(diagonalCartan R n)) : LieAlgebra.rootSpace (diagonalCartan R n) ⇑χ = LieModule.weightSpace (Matrix n n R) ⇑χ

Over a reduced ring the weight spaces of gl n R are honest simultaneous eigenspaces, not merely generalized ones: the diagonal Cartan subalgebra acts diagonally on the matrix units, so no nilpotent part survives. For a Killing-semisimple Lie algebra the corresponding statement is the abstract Jordan decomposition; here it is a diagonal-operator computation applied to TauCeti.toEnd_diagonalCartan_eq_toLin_diagonal, one operator at a time. The hypothesis [IsReduced R] is not decorative: over a ring with nilpotents a generalized eigenspace of a diagonal operator can be strictly larger than the eigenspace.

theorem TauCeti.mem_rootSpace_diagonalCartan_of_forall {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {χ : Module.Dual R ↥(diagonalCartan R n)} {B : Matrix n n R} (h : ∀ (a b : n), glWeightSub R n a b ≠ χ → B a b = 0) : B ∈ LieAlgebra.rootSpace (diagonalCartan R n) ⇑χ

A matrix supported on the pairs (a, b) with εₐ - ε_b = χ lies in the root space of χ. It lies in the honest weight space, in fact: the matrix units are eigenvectors of the diagonal Cartan subalgebra.

@[simp]

theorem TauCeti.mem_rootSpace_diagonalCartan_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [IsDomain R] (χ : Module.Dual R ↥(diagonalCartan R n)) (B : Matrix n n R) : B ∈ LieAlgebra.rootSpace (diagonalCartan R n) ⇑χ ↔ ∀ (a b : n), glWeightSub R n a b ≠ χ → B a b = 0

The weight spaces of gl n R, over a domain: for [IsDomain R], a matrix lies in the root space of a functional χ on the diagonal Cartan subalgebra exactly when its (a, b) entry vanishes for every pair with εₐ - ε_b ≠ χ. The domain hypothesis is used only for the forward implication, where it cancels the nonzero factor εₐ - ε_b - χ; the passage to honest weight spaces that implication also invokes, TauCeti.rootSpace_diagonalCartan_eq_weightSpace, needs only [IsReduced R]. The converse is TauCeti.mem_rootSpace_diagonalCartan_of_forall, which holds over any commutative ring. No hypothesis on the characteristic is needed, since the statement does not separate εᵢ - εⱼ from εⱼ - εᵢ.

The root space decomposition

theorem TauCeti.iSup_rootSpace_glWeightSub_eq_top {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] : ⨆ (p : n × n), LieAlgebra.rootSpace (diagonalCartan R n) ⇑(glWeightSub R n p.1 p.2) = ⊤

The root spaces of the weights εₐ - ε_b span gl n R, because the matrix unit Eₐ_b lies in the root space of εₐ - ε_b.

This is a spanning statement only. The pairs (a, b) repeat root spaces: every εₐ - ε_a is the zero functional, whose root space contains the whole diagonal Cartan subalgebra, and in characteristic two εᵢ - εⱼ = εⱼ - εᵢ. So this supremum is not direct; for the supremum over the weights themselves, which over a domain is, see TauCeti.iSup_rootSpace_eq_top.

theorem TauCeti.iSup_rootSpace_eq_top {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] : ⨆ (χ : Module.Dual R ↥(diagonalCartan R n)), LieAlgebra.rootSpace (diagonalCartan R n) ⇑χ = ⊤

The root space decomposition of gl n R: the root spaces span gl n R. Over a domain Mathlib's LieModule.iSupIndep_genWeightSpace says the root spaces are independent, so this supremum is direct and gl n R is the direct sum of its root spaces.

Mathlib's LieModule.iSup_genWeightSpace_eq_top proves the same spanning statement for a triangularizable module, but only in finite dimensions over a field; here the diagonal Cartan subalgebra is split, so no hypothesis on R is needed.

The roots of gl n R, and the root spaces as lines

@[simp]

theorem TauCeti.glWeightSub_eq_glWeightSub_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (h2 : 2 ≠ 0) {i j : n} (hij : i ≠ j) (a b : n) : glWeightSub R n a b = glWeightSub R n i j ↔ a = i ∧ b = j

Away from characteristic two the weights εᵢ - εⱼ, for i ≠ j, are pairwise distinct. In characteristic two εᵢ - εⱼ = εⱼ - εᵢ, and the statement fails.

theorem TauCeti.rootSpace_glWeightSub_eq_span {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [IsDomain R] (h2 : 2 ≠ 0) {i j : n} (hij : i ≠ j) : ↑(LieAlgebra.rootSpace (diagonalCartan R n) ⇑(glWeightSub R n i j)) = R ∙ Matrix.single i j 1

The root spaces of gl n R are lines: over a domain ([IsDomain R]), away from characteristic two ((2 : R) ≠ 0), and for i ≠ j, the root space of εᵢ - εⱼ is spanned by the matrix unit Eᵢⱼ. All three hypotheses are needed: for i = j the root space is the zero root space, which contains the whole diagonal Cartan subalgebra, and in characteristic two Eᵢⱼ and Eⱼᵢ share a root space, which is then a plane. This is the gl n analogue of Mathlib's LieAlgebra.IsKilling.finrank_rootSpace_eq_one, which is unavailable here because the Killing form of gl n R is degenerate.

theorem TauCeti.finrank_rootSpace_glWeightSub_eq_one {n : Type u_2} [DecidableEq n] [Fintype n] {K : Type u_3} [Field K] (h2 : 2 ≠ 0) {i j : n} (hij : i ≠ j) : Module.finrank K ↥↑(LieAlgebra.rootSpace (diagonalCartan K n) ⇑(glWeightSub K n i j)) = 1

Over a field K of characteristic other than two ((2 : K) ≠ 0), the root space of gl n K attached to the root εᵢ - εⱼ with i ≠ j is one-dimensional. This is TauCeti.rootSpace_glWeightSub_eq_span counted, so it carries the same hypotheses.

theorem TauCeti.rootSpace_diagonalCartan_eq_bot {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [IsDomain R] {χ : Module.Dual R ↥(diagonalCartan R n)} (h : ∀ (a b : n), glWeightSub R n a b ≠ χ) : LieAlgebra.rootSpace (diagonalCartan R n) ⇑χ = ⊥

Over a domain ([IsDomain R]), a functional on the diagonal Cartan subalgebra that is not one of the εₐ - ε_b has trivial root space.

theorem TauCeti.exists_glWeightSub_eq_of_rootSpace_ne_bot {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] [IsDomain R] {χ : Module.Dual R ↥(diagonalCartan R n)} (hχ : χ ≠ 0) (h : LieAlgebra.rootSpace (diagonalCartan R n) ⇑χ ≠ ⊥) : ∃ (i : n) (j : n), i ≠ j ∧ glWeightSub R n i j = χ

The roots of gl n R: over a domain ([IsDomain R]), a nonzero functional χ with a nonzero root space is εᵢ - εⱼ for some i ≠ j. The hypothesis χ ≠ 0 is what rules out the diagonal pairs, since every εₐ - ε_a is the zero functional and the zero root space contains the whole diagonal Cartan subalgebra.