This project is a Lean-formalization of topics related to the Virasoro algebra. The current scope is 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 the Sugawara construction, by which one can equip positive energy representations of the Heisenberg algebra with a representation of the Virasoro algebra also. But so far I have not had time to teach that to Lean.