The diagonal Cartan subalgebra of gl n R

The general linear Lie algebra gl n R is Matrix n n R with the commutator bracket. This file builds its diagonal Cartan subalgebra: the diagonal matrices form an abelian, self-normalizing Lie subalgebra, hence a Cartan subalgebra in the sense of LieSubalgebra.IsCartanSubalgebra. It also records the resulting dictionary between n-tuples and weights, and computes the adjoint action of the diagonal on the matrix units, which places each matrix unit in the root space of a difference of coordinate functionals.

This development cannot assume LieAlgebra.IsKilling for gl n R: whenever R is nontrivial and n is nonempty the identity matrix is a nonzero element of the radical of the Killing form of gl n R, since it is central and so has vanishing adjoint action. So none of Mathlib's LieAlgebra.IsKilling machinery (in particular LieAlgebra.IsKilling.rootSystem) is available here, and the Cartan subalgebra has to be produced by hand.

Main definitions

• TauCeti.diagonalCartan R n: the diagonal matrices, as a LieSubalgebra R (Matrix n n R).
• TauCeti.diagonalEquiv R n: the linear equivalence (n → R) ≃ₗ[R] diagonalCartan R n given by Matrix.diagonal.
• TauCeti.diagonalCartanBasis R n: the basis of diagonalCartan R n by the diagonal matrix units, whence TauCeti.finrank_diagonalCartan.
• TauCeti.glWeightEquiv R n: the linear equivalence between n-tuples and weights, sending μ : n → R to the functional A ↦ ∑ i, μ i * A i i on the diagonal Cartan.
• TauCeti.glWeightSub R n i j: the weight εᵢ - εⱼ of gl n R.

Main results

• TauCeti.instIsCartanSubalgebraDiagonalCartan: diagonalCartan R n is a Cartan subalgebra.
• TauCeti.diagonalCartan_normalizer_eq_self: the diagonal Cartan is self-normalizing.
• TauCeti.lie_apply_of_mem_diagonalCartan: the adjoint action of a diagonal matrix is entrywise scaling, by A a a - A b b in the (a, b) entry.
• TauCeti.lie_single_of_mem_diagonalCartan: for diagonal A, the matrix unit Eᵢⱼ is an eigenvector of ad A with eigenvalue the difference A i i - A j j.
• TauCeti.single_mem_rootSpace: consequently Eᵢⱼ lies in the root space for the weight εᵢ - εⱼ.
• TauCeti.mem_weightSpace_glWeightEquiv_iff: membership in a weight space is equivalent to the coordinate eigenvalue equations for the diagonal matrix units.

Implementation notes

Everything here is stated over an arbitrary commutative ring R and an arbitrary finite index type n; no field, characteristic, or algebraic closure hypothesis is used. The self-normalizing argument needs only the single matrix unit Eᵢᵢ as a test element, and abelianness is Matrix.commute_diagonal.

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

This implements the opening gl n targets (diagonalCartan, mem_diagonalCartan_iff, its IsCartanSubalgebra instance, and glWeightEquiv) of Layer 9 of TauCetiRoadmap/RepresentationTheory/LieHighestWeight/README.md.

theorem TauCeti.lie_eq_zero_of_isDiag {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {A B : Matrix n n R} (hA : A.IsDiag) (hB : B.IsDiag) : ⁅A, B⁆ = 0

Two diagonal matrices commute, so their Lie bracket vanishes.

def TauCeti.diagonalCartan (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : LieSubalgebra R (Matrix n n R)

The diagonal matrices, as a Lie subalgebra of gl n R = Matrix n n R.

This is the standard Cartan subalgebra of gl n R; see TauCeti.instIsCartanSubalgebraDiagonalCartan.

Equations

• TauCeti.diagonalCartan R n = { carrier := {A : Matrix n n R | A.IsDiag}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯, lie_mem' := ⋯ }

@[simp]

theorem TauCeti.mem_diagonalCartan_iff_isDiag {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {A : Matrix n n R} : A ∈ diagonalCartan R n ↔ A.IsDiag

Membership in the diagonal Cartan subalgebra is Matrix.IsDiag.

theorem TauCeti.mem_diagonalCartan_iff {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {A : Matrix n n R} : A ∈ diagonalCartan R n ↔ ∀ (i j : n), i ≠ j → A i j = 0

The entrywise description of the diagonal Cartan subalgebra.

theorem TauCeti.diagonal_mem_diagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (d : n → R) : Matrix.diagonal d ∈ diagonalCartan R n

Every diagonal matrix lies in the diagonal Cartan subalgebra.

theorem TauCeti.single_self_mem_diagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (i : n) (c : R) : Matrix.single i i c ∈ diagonalCartan R n

The diagonal matrix units lie in the diagonal Cartan subalgebra.

instance TauCeti.instIsLieAbelianSubtypeMatrixMemLieSubalgebraDiagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] : IsLieAbelian ↥(diagonalCartan R n)

The adjoint action of the diagonal

theorem TauCeti.lie_apply_of_mem_diagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {A : Matrix n n R} (hA : A ∈ diagonalCartan R n) (B : Matrix n n R) (a b : n) : ⁅A, B⁆ a b = (A a a - A b b) * B a b

The adjoint action of a diagonal matrix is entrywise scaling: ⁅A, B⁆ has (a, b) entry (A a a - A b b) * B a b. Every statement about weight spaces of gl n R for the diagonal Cartan subalgebra ultimately comes from this formula.

theorem TauCeti.lie_single_of_mem_diagonalCartan {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] {A : Matrix n n R} (hA : A ∈ diagonalCartan R n) (i j : n) (c : R) : ⁅A, Matrix.single i j c⁆ = (A i i - A j j) • Matrix.single i j c

The matrix unit Eᵢⱼ is an eigenvector of ad A for every diagonal A, with eigenvalue the difference A i i - A j j of the corresponding diagonal entries. This is the computation underlying TauCeti.single_mem_rootSpace.

Self-normalizing, and the Cartan subalgebra instance

@[simp]

theorem TauCeti.diagonalCartan_normalizer_eq_self (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : (diagonalCartan R n).normalizer = diagonalCartan R n

The diagonal Cartan subalgebra is self-normalizing: a matrix normalizing the diagonal matrices is itself diagonal.

instance TauCeti.instIsCartanSubalgebraDiagonalCartan (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : (diagonalCartan R n).IsCartanSubalgebra

The diagonal matrices form a Cartan subalgebra of gl n R: they are nilpotent (indeed abelian) and self-normalizing.

Coordinates on the diagonal Cartan

def TauCeti.diagonalEquiv (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : (n → R) ≃ₗ[R] ↥(diagonalCartan R n)

The diagonal matrices are the image of n → R under Matrix.diagonal, as a linear equivalence.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.diagonalEquiv_apply (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] (d : n → R) : ↑((diagonalEquiv R n) d) = Matrix.diagonal d

diagonalEquiv sends a tuple to the corresponding diagonal matrix.

@[simp]

theorem TauCeti.diagonalEquiv_symm_apply (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] (A : ↥(diagonalCartan R n)) : (diagonalEquiv R n).symm A = (↑A).diag

The inverse of diagonalEquiv reads off the diagonal of a matrix.

noncomputable def TauCeti.diagonalCartanBasis (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : Module.Basis n R ↥(diagonalCartan R n)

The diagonal matrix units form a basis of the diagonal Cartan subalgebra.

Equations

• TauCeti.diagonalCartanBasis R n = Module.Basis.ofEquivFun (TauCeti.diagonalEquiv R n).symm

@[simp]

theorem TauCeti.diagonalCartanBasis_apply (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] (i : n) : ↑((diagonalCartanBasis R n) i) = Matrix.single i i 1

The i-th vector of diagonalCartanBasis is the diagonal matrix unit Eᵢᵢ.

@[simp]

theorem TauCeti.diagonalCartanBasis_repr_apply (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] (A : ↥(diagonalCartan R n)) (i : n) : ((diagonalCartanBasis R n).repr A) i = ↑A i i

The coordinates of a diagonal matrix in diagonalCartanBasis are its diagonal entries.

instance TauCeti.instFreeSubtypeMatrixMemLieSubalgebraDiagonalCartan (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : Module.Free R ↥(diagonalCartan R n)

instance TauCeti.instFiniteSubtypeMatrixMemLieSubalgebraDiagonalCartan (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : Module.Finite R ↥(diagonalCartan R n)

theorem TauCeti.finrank_diagonalCartan (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] [StrongRankCondition R] : Module.finrank R ↥(diagonalCartan R n) = Fintype.card n

The diagonal Cartan subalgebra of gl n R has rank the number of indices.

theorem TauCeti.sum_smul_diagonalCartanBasis {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (A : ↥(diagonalCartan R n)) : ∑ i : n, ↑A i i • (diagonalCartanBasis R n) i = A

A diagonal matrix is the combination of the diagonal matrix units with its diagonal entries as coefficients.

Weights of gl n R are n-tuples

noncomputable def TauCeti.glWeightEquiv (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] : (n → R) ≃ₗ[R] Module.Dual R ↥(diagonalCartan R n)

Weights of gl n R are n-tuples: the linear equivalence sending μ : n → R to the functional A ↦ ∑ i, μ i * A i i on the diagonal Cartan subalgebra, obtained by transporting the self-duality Module.Basis.toDualEquiv of diagonalCartanBasis along diagonalEquiv.

Equations

• TauCeti.glWeightEquiv R n = (TauCeti.diagonalEquiv R n).trans (TauCeti.diagonalCartanBasis R n).toDualEquiv

@[simp]

theorem TauCeti.glWeightEquiv_apply {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (mu : n → R) (A : ↥(diagonalCartan R n)) : ((glWeightEquiv R n) mu) A = ∑ i : n, mu i * ↑A i i

The weight attached to μ : n → R pairs μ with the diagonal entries.

@[simp]

theorem TauCeti.glWeightEquiv_symm_apply {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (f : Module.Dual R ↥(diagonalCartan R n)) (i : n) : (glWeightEquiv R n).symm f i = f ((diagonalCartanBasis R n) i)

The tuple attached to a weight reads it off on the diagonal matrix units.

@[simp]

theorem TauCeti.mem_weightSpace_glWeightEquiv_iff {K : Type u_3} {M : Type u_4} {n : Type u_5} [CommRing K] [Fintype n] [DecidableEq n] [AddCommGroup M] [Module K M] [LieRingModule (Matrix n n K) M] [LieModule K (Matrix n n K) M] (mu : n → K) (x : M) : x ∈ LieModule.weightSpace M ⇑((glWeightEquiv K n) mu) ↔ ∀ (i : n), ⁅Matrix.single i i 1, x⁆ = mu i • x

A vector has general-linear weight μ if and only if each diagonal matrix unit acts on it by the corresponding coordinate μ i.

noncomputable def TauCeti.glWeightSub (R : Type u_1) [CommRing R] (n : Type u_2) [DecidableEq n] [Fintype n] (i j : n) : Module.Dual R ↥(diagonalCartan R n)

The weight εᵢ - εⱼ of gl n R, as a functional on the diagonal Cartan subalgebra. This is a weight, not a root: for i = j the functional is zero, and the zero weight is never a root. For i ≠ j over a nontrivial ring it is a root, since TauCeti.single_mem_rootSpace places the nonzero matrix unit Eᵢⱼ in the root space.

Equations

• TauCeti.glWeightSub R n i j = (TauCeti.glWeightEquiv R n) (Pi.single i 1 - Pi.single j 1)

@[simp]

theorem TauCeti.glWeightSub_apply {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (i j : n) (A : ↥(diagonalCartan R n)) : (glWeightSub R n i j) A = ↑A i i - ↑A j j

The functional εᵢ - εⱼ reads off the difference of two diagonal entries.

@[simp]

theorem TauCeti.glWeightSub_self {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (i : n) : glWeightSub R n i i = 0

The functionals εᵢ - εᵢ vanish.

theorem TauCeti.single_mem_rootSpace {R : Type u_1} [CommRing R] {n : Type u_2} [DecidableEq n] [Fintype n] (i j : n) (c : R) : Matrix.single i j c ∈ LieAlgebra.rootSpace (diagonalCartan R n) ⇑(glWeightSub R n i j)

The matrix unit Eᵢⱼ lies in the root space of gl n R, relative to the diagonal Cartan, for the weight εᵢ - εⱼ. For i = j this says that the diagonal Cartan lies in the zero root space.