The dimension of the special linear Lie algebra

The trace-zero matrices sl n R form a finite free module over any commutative ring. For a nonempty finite index type, the entries away from one diagonal place are free coordinates: the trace-zero condition determines the remaining entry as minus the sum of the other diagonal entries. For an empty index type, sl n R is the zero module.

Over a nontrivial commutative ring, the strong rank condition gives finrank R (sl n R) = (Fintype.card n) ^ 2 - 1. Truncated subtraction includes the empty case; Ado.finrank_sl_add_one gives the untruncated formula when the index type is nonempty.

Main results

• Ado.finrank_sl: sl n R has rank (card n) ^ 2 - 1.
• Ado.finrank_sl_add_one: the untruncated form, for a nonempty index type.

The same coordinate system also gives the Module.Free and Module.Finite instances for sl n R that any rank computation involving it needs; over a commutative ring these do not come for free from finiteness of the matrices.

Implementation notes

A private linear equivalence identifies sl n R with the entries away from one diagonal place. Freeness, finiteness and dimension follow by transporting the corresponding facts about this function space. Membership is read through LieAlgebra.SpecialLinear.mem_sl_iff.

instance Ado.instFreeSubtypeMatrixMemLieSubalgebraSl_leanPool {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : Module.Free R ↥(LieAlgebra.SpecialLinear.sl n R)

sl n R is a free module. For a nonempty index type the coordinates above are a basis of it; for an empty one it is the zero module.

instance Ado.instFiniteSubtypeMatrixMemLieSubalgebraSl_leanPool {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : Module.Finite R ↥(LieAlgebra.SpecialLinear.sl n R)

sl n R is a finite module, the coordinates above being finite in number.

@[simp]

theorem Ado.finrank_sl (R : Type u_1) (n : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] [StrongRankCondition R] : Module.finrank R ↥(LieAlgebra.SpecialLinear.sl n R) = Fintype.card n ^ 2 - 1

The rank of sl n R: finrank R (sl n R) = (card n) ^ 2 - 1.

For an empty index type the matrix algebra is trivial and both sides are 0, the truncated subtraction 0 - 1 doing the work.

theorem Ado.finrank_sl_add_one (R : Type u_1) (n : Type u_2) [Fintype n] [DecidableEq n] [CommRing R] [StrongRankCondition R] [Nonempty n] : Module.finrank R ↥(LieAlgebra.SpecialLinear.sl n R) + 1 = Fintype.card n ^ 2

The untruncated codimension-one statement: sl n R is a hyperplane in the matrices.