Loop Lie algebras and their central extensions

Given a Lie algebra L, the loop algebra is the Lie algebra of maps from a circle into L. This can mean many different things, e.g., continuous maps, smooth maps, polynomial maps. In this file, we consider the simplest case of polynomial maps, meaning we take a base change with the ring of Laurent polynomials.

Loop Lie algebras admit central extensions attached to invariant inner products on the base Lie algebra. When the base Lie algebra is finite dimensional and simple, the corresponding central extension (with an outer derivation attached) admits an infinite root system with affine Weyl group. These extended Lie algebras are called untwisted affine Kac-Moody Lie algebras.

We implement the basic theory using AddMonoidAlgebra instead of LaurentPolynomial for flexibility. The classical loop algebra is then written loopAlgebra R ℤ L.

Main definitions

• LieAlgebra.loopAlgebra: The tensor product of a Lie algebra with an AddMonoidAlgebra.
• LieAlgebra.loopAlgebra.toFinsupp: A linear equivalence from the loop algebra to the space of finitely supported functions.
• LieAlgebra.loopAlgebra.twoCochainOfBilinear: The 2-cochain for a loop algebra with trivial coefficients attached to a symmetric bilinear form on the base Lie algebra.
• LieAlgebra.loopAlgebra.twoCocycleOfBilinear: The 2-cocycle for a loop algebra with trivial coefficients attached to a symmetric invariant bilinear form on the base Lie algebra.

TODO

• Evaluation representations
• Construction of central extensions from invariant forms.
• Positive energy representations induced from a fixed central character

Tags

lie ring, lie algebra, base change, Laurent polynomial

@[reducible, inline]

abbrev LieAlgebra.loopAlgebra (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] : Type (max (max u_2 u_1) u_3)

A loop algebra is the base change of a Lie algebra L over R by R[z,z⁻¹]. We make a slightly more general definition which coincides with the Laurent polynomial construction when A = ℤ

Equations

• LieAlgebra.loopAlgebra R A L = TensorProduct R (AddMonoidAlgebra R A) L

def LieAlgebra.loopAlgebraEquivLaurent (R : Type u_1) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] : loopAlgebra R ℤ L ≃ₗ⁅R⁆ TensorProduct R (LaurentPolynomial R) L

An Lie algebra isomorphism between the Loop algebra (with A = ℤ) and the tensor product with Laurent polynomials.

Equations

• LieAlgebra.loopAlgebraEquivLaurent R L = LieEquiv.refl

def LieAlgebra.LoopAlgebra.toFinsupp (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] : loopAlgebra R A L ≃ₗ[R] A →₀ L

A linear isomorphism to finitely supported functions.

Equations

• LieAlgebra.LoopAlgebra.toFinsupp R A L = TensorProduct.equivFinsuppOfBasisLeft (AddMonoidAlgebra.basis A R)

@[simp]

theorem LieAlgebra.LoopAlgebra.toFinsupp_symm_single (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (c : A) (z : L) : (toFinsupp R A L).symm (Finsupp.single c z) = AddMonoidAlgebra.single c 1 ⊗ₜ[R] z

@[simp]

theorem LieAlgebra.LoopAlgebra.toFinsupp_single_tmul (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] (c : A) (z : L) : (toFinsupp R A L) (AddMonoidAlgebra.single c 1 ⊗ₜ[R] z) = Finsupp.single c z

def LieAlgebra.LoopAlgebra.residuePairing (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup A] [DistribSMul A R] [SMulCommClass A R R] (Φ : LinearMap.BilinForm R L) : LinearMap.BilinForm R (loopAlgebra R A L)

The residue pairing on the loop algebra. When A = ℤ and the elements are viewed as Laurent polynomials with coefficients in L, the pairing is interpreted as (f, g) ↦ Res f dg.

Equations

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

@[simp]

theorem LieAlgebra.LoopAlgebra.residuePairing_apply_apply (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup A] [DistribSMul A R] [SMulCommClass A R R] (Φ : LinearMap.BilinForm R L) (f g : loopAlgebra R A L) : ((residuePairing R A L Φ) f) g = ((toFinsupp R A L) g).sum fun (a : A) (v : L) => a • (Φ (((toFinsupp R A L) f) (-a))) v

def LieAlgebra.LoopAlgebra.twoCochainOfBilinear (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [CommRing A] [IsAddTorsionFree R] [Algebra A R] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) : ↥(LieModule.Cohomology.twoCochain R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))

A 2-cochain on a loop algebra given by an invariant bilinear form. When A = ℤ, the alternating condition amounts to the fact that Res f df = 0.

Equations

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

@[simp]

theorem LieAlgebra.LoopAlgebra.twoCochainOfBilinear_apply_apply (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [CommRing A] [IsAddTorsionFree R] [Algebra A R] (Φ : LinearMap.BilinForm R L) (hΦ : Φ.IsSymm) (x y : loopAlgebra R A L) : ((twoCochainOfBilinear R A L Φ hΦ) x) y = (TrivialLieModule.equiv R (loopAlgebra R A L) R).symm (((residuePairing R A L Φ) x) y)

def LieAlgebra.LoopAlgebra.twoCocycleOfBilinear (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [CommRing A] [IsAddTorsionFree R] [Algebra A R] (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) : ↥(LieModule.Cohomology.twoCocycle R (loopAlgebra R A L) (TrivialLieModule R (loopAlgebra R A L) R))

A 2-cocycle on a loop algebra given by an invariant bilinear form.

Equations

• LieAlgebra.LoopAlgebra.twoCocycleOfBilinear R A L Φ hΦ hΦs = ⟨LieAlgebra.LoopAlgebra.twoCochainOfBilinear R A L Φ hΦs, ⋯⟩

@[simp]

theorem LieAlgebra.LoopAlgebra.twoCocycleOfBilinear_coe (R : Type u_1) (A : Type u_2) (L : Type u_3) [CommRing R] [LieRing L] [LieAlgebra R L] [CommRing A] [IsAddTorsionFree R] [Algebra A R] (Φ : LinearMap.BilinForm R L) (hΦ : LinearMap.BilinForm.lieInvariant L Φ) (hΦs : Φ.IsSymm) : ↑(twoCocycleOfBilinear R A L Φ hΦ hΦs) = twoCochainOfBilinear R A L Φ hΦs