Constructing representations of Lie algebras from operators corresponding to a basis

This file contains a construction of a Lie algebra representation from a basis and operators satisfying the corresponding commutation relations. (It is used in particular in the Sugawara constructions.)

Main definitions

• LieAlgebra.representationOfBasis: Given a basis B of a Lie algebra 𝓰 and a collection of linear operators on a vector space V satisfying the commutation relations specified by the Lie brackets of the basis elements, construct a representation of 𝓰 on the vector space V.

@[reducible, inline]

abbrev LieAlgebra.Representation (𝕜 : Type u_1) (𝕂 : Type u_2) [CommRing 𝕜] [CommRing 𝕂] (𝓰 : Type u_3) [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] (V : Type u_4) [AddCommGroup V] [Module 𝕂 V] [Module 𝕜 V] [SMul 𝕜 𝕂] [IsScalarTower 𝕜 𝕂 V] [SMulCommClass 𝕂 𝕜 V] : Type (max u_3 u_4)

A representation of a 𝕜-Lie algebra 𝓰 on a 𝕂-vector space V.

Equations

• LieAlgebra.Representation 𝕜 𝕂 𝓰 V = (𝓰 →ₗ⁅𝕜⁆ V →ₗ[𝕂] V)

theorem LieAlgebra.Representation.apply_bracket_eq_commutator {𝕜 : Type u_1} {𝕂 : Type u_2} [CommRing 𝕜] [CommRing 𝕂] {𝓰 : Type u_3} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] {V : Type u_4} [AddCommGroup V] [Module 𝕂 V] [Module 𝕜 V] [SMul 𝕜 𝕂] [IsScalarTower 𝕜 𝕂 V] [SMulCommClass 𝕂 𝕜 V] (ρ : Representation 𝕜 𝕂 𝓰 V) (X Y : 𝓰) : ρ ⁅X, Y⁆ = (ρ X).commutator (ρ Y)

noncomputable def LieAlgebra.representationOfBasisAux {𝕂 : Type u_1} [Field 𝕂] {V : Type u_2} [AddCommGroup V] [Module 𝕂 V] {𝓰 : Type u_3} [LieRing 𝓰] [LieAlgebra 𝕂 𝓰] {ι : Type u_4} (B : Module.Basis ι 𝕂 𝓰) (genOper : ι → V →ₗ[𝕂] V) : 𝓰 →ₗ[𝕂] V →ₗ[𝕂] V

An auxiliary definition for constructing representation of Lie algebras from a basis and a corresponding collection of operators; representationOfBasisAux is just a linear map from the Lie algebra to the space of operators (not yet a morphism of Lie algebras).

Equations

• LieAlgebra.representationOfBasisAux B genOper = (B.constr 𝕂) fun (i : ι) => genOper i

@[simp]

theorem LieAlgebra.representationOfBasisAux_apply_basis {𝕂 : Type u_1} [Field 𝕂] {V : Type u_2} [AddCommGroup V] [Module 𝕂 V] {𝓰 : Type u_3} [LieRing 𝓰] [LieAlgebra 𝕂 𝓰] {ι : Type u_4} (B : Module.Basis ι 𝕂 𝓰) (genOper : ι → V →ₗ[𝕂] V) (i : ι) : (representationOfBasisAux B genOper) (B i) = genOper i

theorem LieAlgebra.representationOfBasisAux_property {𝕂 : Type u_5} [Field 𝕂] {V : Type u_6} [AddCommGroup V] [Module 𝕂 V] {𝓰 : Type u_7} [LieRing 𝓰] [LieAlgebra 𝕂 𝓰] {ι : Type u_8} (B : Module.Basis ι 𝕂 𝓰) {genOper : ι → V →ₗ[𝕂] V} (genComm : ∀ (i j : ι), (genOper i).commutator (genOper j) = (representationOfBasisAux B genOper) ⁅B i, B j⁆) : LinearMap.compRight 𝕂 (representationOfBasisAux B genOper) ∘ₗ bracketHom 𝕂 𝓰 = (LinearMap.commutatorBilin V).compl₁₂ (representationOfBasisAux B genOper) (representationOfBasisAux B genOper)

noncomputable def LieAlgebra.representationOfBasis {𝕂 : Type u_5} [Field 𝕂] {V : Type u_6} [AddCommGroup V] [Module 𝕂 V] {𝓰 : Type u_7} [LieRing 𝓰] [LieAlgebra 𝕂 𝓰] {ι : Type u_8} (B : Module.Basis ι 𝕂 𝓰) {genOper : ι → V →ₗ[𝕂] V} (genComm : ∀ (i j : ι), (genOper i).commutator (genOper j) = (representationOfBasisAux B genOper) ⁅B i, B j⁆) : Representation 𝕂 𝕂 𝓰 V

A representation of a Lie algebra 𝓰 with basis B constructed from a collection of operators satisfying the commutation relations specified by the Lie brackets of the basis elements.

Equations

• LieAlgebra.representationOfBasis B genComm = { toFun := ⇑(LieAlgebra.representationOfBasisAux B genOper), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

theorem LieAlgebra.representationOfBasis_property {𝕂 : Type u_1} [Field 𝕂] {V : Type u_2} [AddCommGroup V] [Module 𝕂 V] {𝓰 : Type u_3} [LieRing 𝓰] [LieAlgebra 𝕂 𝓰] {ι : Type u_4} (B : Module.Basis ι 𝕂 𝓰) {genOper : ι → V →ₗ[𝕂] V} (genComm : ∀ (i j : ι), (genOper i).commutator (genOper j) = (representationOfBasisAux B genOper) ⁅B i, B j⁆) : LinearMap.compRight 𝕂 ↑(representationOfBasis B genComm) ∘ₗ bracketHom 𝕂 𝓰 = (LinearMap.commutatorBilin V).compl₁₂ ↑(representationOfBasis B genComm) ↑(representationOfBasis B genComm)