Virasoro algebra (and cohomology of the Witt algebra)

Stream: maths

[Kalle Kytölä]

Hello fellow Lean enthusiasts, and happy New Year!

It had been a long time since I had time to play Lean, but during the holidays I found a bit of time. I thought I'd make the result public, in case others are interested in the same theme. (I might even write a small blueprint soon to help see what is in there.)

What I set out to do was to formalize something related to the Virasoro algebra. I did not (yet) get to where I really wanted, but I did get the construction of the Virasoro algebra as the unique 1-dimensional central extension of the Witt algebra.

This involved writing some basics of Lie algebra cohomology in degree two, central extensions constructed (concretely) from 2-cocycles, and the (abstract) "characteristic predicate" of central extensions as short exact sequences.

The main part so far was, however, the explicit calculation of a specific 2-cohomology, namely that of the Witt algebra. I had never done Lean projects which involve calculations, so this was one of the main reasons why I chose this game instead of something else; I wanted to get a feeling of how is it to do calculations (in an explicitly chosen basis :scream:) in Lean. I expected this to be slightly awkward, but at least it wasn't worse than I expected. In the end the (current) main result is the proof that the 2-cohomology (with coefficients in the scalar field) of the Witt algebra is 1-dimensional and generated by the class of the Virasoro cocycle.

With the cocycle and the central extension API, I defined the Virasoro algebra. As another (more trivial) example application I constructed the Heisenberg (Lie) algebra as the 1-dimensional central extension of an infinite-dimensional abelian Lie algebra associated with an explicit nonzero 2-cocycle. The main motivation for this second (quite boring in its own right) application is that I actually wanted to work towards the Sugawara construction (in conformal field theory, which is my own area), which equips positive energy representations of the Heisenberg algebra with a representation of the Virasoro algebra. But I ran out of holiday days and I thought I should at least put what I have so far in public in case someone else finds it interesting.

[Yoh Tanimoto]

very nice! maybe there is some intersection with what @Scott Carnahan is doing? #20206

[Kalle Kytölä]

Oh, there absolutely seems to be! Thanks! I hadn't noticed this PR (I have not really had time to follow Mathlib development recently).

The part of my project that was in the most urgent need of cleaning up was anyway the general theory; I set it up only so that I got to doing the concrete calculation. So I will be happy to try to refactor if Scott's PRs set up that general theory and they land in Mathlib.

But a question to @Scott Carnahan: have you done also the calculation of the Witt algebra 2-cohomology to define the Virasoro algebra and is your plan to PR that?

[Kalle Kytölä]

(Btw, Yoh, Scott, and I may have somewhat similar reasons in our own research themes to be interested in central extensions etc... :grinning_face_with_smiling_eyes:)

[Scott Carnahan]

@Kalle Kytölä I have not done any cohomology calculations, but I have a construction of central extensions from 2-cocycles.

[Kevin Buzzard]

@Yudai Yamazaki does this overlap with your summer project?

[Kalle Kytölä]

Scott Carnahan said:

Kalle Kytölä I have not done any cohomology calculations, but I have a construction of central extensions from 2-cocycles.

Ok! I'd love to see you PR the construction; you can ping me for review (although I have varying amounts of lack of time). If you PR it, I would then try to refactor my concrete calculation to use your (i.e., Mathlib's) 2-cohomology and central extensions.

Btw, do you also have the opposite: that any central extension corresponds to a 2-cocycle (well-def mod coboundary)? I spent maybe 15min on that diagram chase in Lean, but decided I don't explicitly need that direction, so I left it at that. It should not be too hard, but there was some annoyance (if I remember correctly it was about proving that the unique elements obtained by the diagram chasing depend linearly on their arguments as they of course obviously do; the annoyance could well just be my lack of familiarity with the appropriate parts of Mathlib).

I was also planning to do Sugarawa construction (the basic bosonic case), and I think here there is an obvious overlap of our interests, since the same is used in VOAs. I "need"/want a version that is at the same time slightly more general than the VOA construction and less general in that it would be restricted to the free boson case (although modifications to affine Kac-Moody algebras should then be relatively straightforward). If you have or get plans for doing that, I'd appreciate knowing; I will also let you know when (...or if...) I find the time to write Sugawara myself.

[Kalle Kytölä]

@Scott Carnahan:

I'd still be interested in the above, i.e., whether you also have that any central extension corresponds to a 2-cocycle (well-def mod coboundary)? If you already did the diagram chase, I'd be glad to save myself the trouble. But it would be nice to have (already for the purpose of constructing a basis of a central extension from bases of the original Lie algebras).

Another thing that I would like to know is whether you had a nicer way around the dependent type issues that I found annoying leading up to LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary, i.e., that two cocyles which differ by coboundaries determine isomorphic central extensions. The issues I faced are described in particular in the (apparently incomplete sentence of the) docstring for LieTwoCocycle.CentralExtension.congr.

[Scott Carnahan]

@Kalle Kytölä

I haven't worked anything out, but I would suggest a function that, instead of the hypothesis (h : γ' - γ ∈ LieTwoCoboundary 𝕜 𝓖 𝓐), used an explicit 1-cochain x, and the hypothesis that γ' = γ + dx.

[Kalle Kytölä]

Thanks, that seems like a potential improvement, although it also seems like a natural alternative to go in the opposite direction and use (h : γ.cohomologyClass = γ'.cohomologyClass) as the hypothesis. :thinking: [UPDATE: Ah, I now realize you were probably referring to my crime of constructing data in tactic mode. Yes, for that your suggestion looks clearly better! This was a secondary issue to me compared with the dependent type issue, but should absolutely be fixed, too.]

In any case, this does not seem to affect the dependent type issue, unless I am missing something... Perhaps the lemmas in between LieTwoCocycle.CentralExtension.congr and LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary are just necessary. (Mathematically it just feels strange to me to be saying that if I know that two 2-cocycles are literally the same then the central extensions they determine are isomorphic.)

I guess the main thing about the diagram chase was something a bit similarly frustrating; obviously there was a unique thing (and I constructed it), so I just got lazy proving the obvious fact that the unique thing determined by a linear condition on the input depends linearly on its input (and satisfies the 2-cocycle equation)... My guess was that someone has encountered a similar thing before and there may be a Lean-idiom that handles it less brutally than what I would have done if I hadn't gotten lazy as I did not need it right away.