The defining representation of a matrix Lie subalgebra

A Lie subalgebra of square matrices acts faithfully on coordinate vectors. This file extends that action to the universal enveloping algebra and records its values on Lie generators. It also transports nilpotency of an underlying matrix to nilpotency of the resulting endomorphism.

Main definitions and results

• LieSubalgebra.matrixRepresentation: the defining representation extended to the universal enveloping algebra.
• LieSubalgebra.matrixRepresentation_ι_injective: faithfulness on the Lie algebra.
• LieSubalgebra.isNilpotent_matrixRepresentation_ι: nilpotency transport.

def LieSubalgebra.matrixRepresentation {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (K : LieSubalgebra R (Matrix n n R)) : UniversalEnvelopingAlgebra R ↥K →ₐ[R] Module.End R (n → R)

The defining action of a matrix Lie subalgebra, extended to its universal enveloping algebra.

Equations

• K.matrixRepresentation = (UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R (↥K) (n → R))

theorem LieSubalgebra.matrixRepresentation_def {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (K : LieSubalgebra R (Matrix n n R)) : K.matrixRepresentation = (UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R (↥K) (n → R))

The defining representation is the universal-enveloping extension of the matrix Lie-module action.

theorem LieSubalgebra.matrixRepresentation_ι {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (K : LieSubalgebra R (Matrix n n R)) (x : ↥K) : K.matrixRepresentation ((UniversalEnvelopingAlgebra.ι R) x) = Matrix.toLinAlgEquiv' ↑x

A Lie generator acts through its underlying matrix.

theorem LieSubalgebra.matrixRepresentation_ι_apply {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (K : LieSubalgebra R (Matrix n n R)) (x : ↥K) (v : n → R) : (K.matrixRepresentation ((UniversalEnvelopingAlgebra.ι R) x)) v = (↑x).mulVec v

Pointwise, a Lie generator acts by matrix-vector multiplication.

theorem LieSubalgebra.matrixRepresentation_ι_injective {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (K : LieSubalgebra R (Matrix n n R)) : Function.Injective fun (x : ↥K) => K.matrixRepresentation ((UniversalEnvelopingAlgebra.ι R) x)

The defining representation of a matrix Lie subalgebra is faithful on the Lie algebra.

theorem LieSubalgebra.isNilpotent_matrixRepresentation_ι {R : Type u_1} {n : Type u_2} [CommRing R] [Fintype n] [DecidableEq n] (K : LieSubalgebra R (Matrix n n R)) (x : ↥K) (hx : IsNilpotent ↑x) : IsNilpotent (K.matrixRepresentation ((UniversalEnvelopingAlgebra.ι R) x))

A nilpotent matrix acts nilpotently in the defining representation.