The Cartan generators of a Lie algebra basis as a module basis

A LieAlgebra.Basis ι H carries a family h : ι → H of Cartan generators which is linearly independent and spans H. This file packages that data as a Module.Basis of H and reads off the dimension of H.

Main definitions

• LieAlgebra.Basis.cartanBasis: the Cartan generators as a module basis of the Cartan subalgebra.

noncomputable def LieAlgebra.Basis.cartanBasis {ι : Type u_1} {R : Type u_2} {L : Type u_3} [Finite ι] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) : Module.Basis ι R ↥H

The Cartan generators of a Lie algebra basis form a module basis of its Cartan subalgebra.

Equations

• b.cartanBasis = (Module.Basis.span ⋯).map (LinearEquiv.ofEq H.toSubmodule (Submodule.span R (Set.range b.h)) ⋯).symm

@[simp]

theorem LieAlgebra.Basis.coe_cartanBasis {ι : Type u_1} {R : Type u_2} {L : Type u_3} [Finite ι] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} (b : Basis ι H) (i : ι) : ↑(b.cartanBasis i) = b.h i

The vectors of LieAlgebra.Basis.cartanBasis are the Cartan generators.

theorem LieAlgebra.Basis.finrank_cartan {ι : Type u_1} {R : Type u_2} {L : Type u_3} [Finite ι] [CommRing R] [LieRing L] [LieAlgebra R L] {H : LieSubalgebra R L} [StrongRankCondition R] (b : Basis ι H) : Module.finrank R ↥H = Nat.card ι

The Cartan subalgebra has dimension the cardinality of the basis's index type.