Virasoro Project

link to docs and blueprint

This project is a Lean-formalization of topics related to the Virasoro algebra. The original scope was mainly:

• the construction of the Virasoro algebra as the (unique) 1-dimensional central extension of the Witt algebra. («VirasoroProject».VirasoroAlgebra)

To enable the construction, the project contains API development for

• Lie algebra cohomology in degree two («VirasoroProject».LieCohomologySmallDegree)
• central extensions constructed from 2-cocycles («VirasoroProject».CentralExtension)
• the "characteristic predicate" of central extensions as short exact sequences («VirasoroProject».IsCentralExtension)

and the definition of

• the Witt algebra («VirasoroProject».WittAlgebra)
• and its 2-cocycle which defines the Virasoro algebra as its central extension («VirasoroProject».VirasoroCocycle)

and finally

• the proof (by calculation!) that the 2-cohomology of the Witt algebra is one-dimensional and is generated by the (class of the) Virasoro cocycle. («VirasoroProject».WittAlgebraCohomology)

As a rather trivial second application of the API of central extensions, the project defines also

• the Heisenberg (Lie) algebra as the 1-dimensional central extension of a countably infinite-dimensional abelian Lie algebra associated with an explicit nonzero 2-cocycle. («VirasoroProject».HeisenbergAlgebra)

The main purpose of this mathematically less interesting second case is to enable a further result, the Sugawara construction, by which one can equip positive energy representations of the Heisenberg algebra with a representation of the Virasoro algebra also. Specifically,

• it is proven (by calculation!) that the basic bosonic Sugawara construction equips any representation of the Heisenberg algebra satisfying a local truncation condition with a representation of the Virasoro algebra with central charge c=1. («VirasoroProject».Sugawara)

The project

• defines a generalized notion of Verma modules and proves their universal property. («VirasoroProject».VermaModule)

The design choices of the Verma module definition may not be entirely uncontroversial, but so far this has been successfully applied to

• construct the charged Fock space representation of the Heisenberg algebra («VirasoroProject».FockSpace)
• show that the Sugawara construction applies to the charged Fock space, making it a representation of the Virasoro algebra with central charge c=1, and the vacuum being a highest weight vector with highest weight 1/2*charge^2. («VirasoroProject».FockSpaceSugawara)