4.3. Witt algebra 2-cohomology
Witt algebra 2-cocycle condition for basis.
For any Witt algebra 2-cocycle \gamma \in \Coc^2(\witt,\bbk) with coefficients
in \bbk, we have
\begin{aligned}
(m-k) \, \gamma \big( \ell_n , \ell_{m+k} \big)
+ (k-n) \, \gamma \big( \ell_{m} , \ell_{n+k} \big)
+ (n-m) \, \gamma \big( \ell_k , \ell_{n+m} \big)
\; = \; 0
\end{aligned}
for all n,m,k \in \bZ.
Lean code for Lemma4.3.1●1 theorem
Associated Lean declarations
-
theoremdefined in VirasoroProject/WittAlgebraCohomology.leancomplete
theorem VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero.{u_1} {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) (n m k : ℤ) : (↑m - ↑k) * (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) n)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (m + k)) + (↑k - ↑n) * (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) m)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (n + k)) + (↑n - ↑m) * (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) k)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (n + m)) = 0
theorem VirasoroProject.WittAlgebra.add_lieTwoCocycle_apply_lgen_lgen_lgen_eq_zero.{u_1} {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) (n m k : ℤ) : (↑m - ↑k) * (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) n)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (m + k)) + (↑k - ↑n) * (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) m)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (n + k)) + (↑n - ↑m) * (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) k)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (n + m)) = 0
The 2-cocycle equation in the standard basis `ℓₙ` of the Witt algebra: `0 = (m-k) * γ(n,m+k) + (k-n) * γ(m,n+k) + (n-m) * γ(k,n+m)`.
Direct calculation, using Definition 4.1.1 and Definition 2.3.
Witt algebra 2-cocycle support assuming normalization.
Let \gamma \in \Coc^2(\witt,\bbk) be a Witt algebra 2-cocycle such that
\gamma (\ell_0 , \ell_n) = 0 for all n \in \bZ.
Then for any n,m \in \bZ with n+m \ne 0, we have
\begin{aligned}
\gamma(\ell_n , \ell_m) = 0.
\end{aligned}
Lean code for Lemma4.3.2●1 theorem
Associated Lean declarations
-
theoremdefined in VirasoroProject/WittAlgebraCohomology.leancomplete
theorem VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero.{u_1} {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) {n m : ℤ} (ne_zero : n + m ≠ 0) (hγ : (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) 0)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (n + m)) = 0) : (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) n)) ((VirasoroProject.WittAlgebra.lgen 𝕜) m) = 0
theorem VirasoroProject.WittAlgebra.lieTwoCocycle_apply_lgen_lgen_eq_zero_of_add_ne_zero.{u_1} {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) {n m : ℤ} (ne_zero : n + m ≠ 0) (hγ : (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) 0)) ((VirasoroProject.WittAlgebra.lgen 𝕜) (n + m)) = 0) : (γ ((VirasoroProject.WittAlgebra.lgen 𝕜) n)) ((VirasoroProject.WittAlgebra.lgen 𝕜) m) = 0
Apply Lemma 4.3.1 with k=0. The last term
vanishes, and by skew-symmetry of \gamma, the first two terms simplify to yield
\begin{aligned}
(m+n) \, \gamma (\ell_n , \ell_m) = 0 ,
\end{aligned}
which, assuming n+m \ne 0, yields the asserted equation
\gamma (\ell_n , \ell_m) = 0.
Normalization of Witt algebra 2-cocycles.
For any 2-cocycle \gamma \in \Coc^2(\witt,\bbk), there exists
a coboundary \partial \beta with \beta \in \Coch^1(\witt,\bbk)
such that
\begin{aligned}
\gamma + \partial \beta \; = \; r \cdot {\gamma}_{\vir}
\end{aligned}
for some scalar r \in \bbk.
Lean code for Lemma4.3.3●1 theorem
Associated Lean declarations
-
theoremdefined in VirasoroProject/WittAlgebraCohomology.leancomplete
theorem VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle.{u_1} {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) : ∃ r, γ + (VirasoroProject.WittAlgebra.normalizingCochain γ).bdry = r • VirasoroProject.WittAlgebra.virasoroCocycle 𝕜
theorem VirasoroProject.WittAlgebra.exists_add_bdry_eq_smul_virasoroCocycle.{u_1} {𝕜 : Type u_1} [Field 𝕜] [CharZero 𝕜] (γ : VirasoroProject.LieTwoCocycle 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) : ∃ r, γ + (VirasoroProject.WittAlgebra.normalizingCochain γ).bdry = r • VirasoroProject.WittAlgebra.virasoroCocycle 𝕜
Let \gamma \in \Coc^2(\witt,\bbk) be a Witt algebra 2-cocycle.
Define a Witt algebra 1-cochain \beta \in \Coch^1(\witt,\bbk) by linear extension of
\begin{aligned}
\beta (\ell_n) =
\begin{cases}
-\frac{1}{2} \gamma(\ell_1, \ell_{-1}) & \text{ if } n = 0 \\
\frac{1}{n} \gamma(\ell_0, \ell_n) & \text{ if } n \ne 0 .
\end{cases}
\end{aligned}
For any n \ne 0, we calculate
\begin{aligned}
\big( \gamma + \partial \beta \big) (\ell_0 , \ell_n)
= \; & \gamma (\ell_0 , \ell_n) + \beta ([\ell_0,\ell_n]) \\
= \; & \gamma (\ell_0 , \ell_n) - n \, \beta (\ell_n) \\
= \; & \gamma (\ell_0 , \ell_n) - n \, \frac{1}{n}\gamma(\ell_0, \ell_n) = 0 .
\end{aligned}
This property and Lemma 4.3.2 imply that
\begin{aligned}
\big( \gamma + \partial \beta \big) (\ell_0 , \ell_n) = 0
\end{aligned}
whenever n+m \ne 0.
We will show the asserted equation with
\begin{aligned}
r = 2 \, \big( \gamma + \partial \beta \big) ( \ell_2, \ell_{-2}) .
\end{aligned}
By comparison with the Virasoro cocycle {\gamma}_{\vir}
of Definition 4.2.1, and using skew-symmetry,
it remains to show that for any n \in \bN we have
\begin{aligned}
\big( \gamma + \partial \beta \big) (\ell_n , \ell_{-n})
= r \; \frac{n^3 - n}{12} .
\end{aligned}
The case n = 0 is a direct consequence of antisymmetry.
The case n = 1 follows
using the definition of \beta and the calculation
\begin{aligned}
\big( \gamma + \partial \beta \big) (\ell_1 , \ell_{-1})
= \; & \gamma (\ell_1 , \ell_{-1}) + \beta ([\ell_1,\ell_{-1}]) \\
= \; & \gamma (\ell_1 , \ell_{-1}) + 2 \, \beta (\ell_0) \\
= \; & \gamma (\ell_1 , \ell_{-1}) - 2 \, \frac{1}{2} \gamma(\ell_1, \ell_{-1}) = 0 .
\end{aligned}
The case n = 2 follows directly by the choice of r.
We prove the equality in the cases n \ge 3 by induction on n.
Assume the equation for smaller values of n.
Apply Lemma 4.3.1 to \gamma + \partial \beta
with m = 1-n and k = -1 to get
\begin{aligned}
0 = \; & (2-n) \, \big( \gamma + \partial \beta \big) (\ell_n , \ell_{-n})
+ (-1-n) \, \big( \gamma + \partial \beta \big) (\ell_{1-n} , \ell_{n-1})
+ (2 n - 1) \, \big( \gamma + \partial \beta \big) (\ell_1 , \ell_{-1}) \\
= \; & (2-n) \, \big( \gamma + \partial \beta \big) (\ell_n , \ell_{-n})
- (-1-n) \, r \frac{(n-1)^3 - (n-1)}{12} \\
= \; & (2-n) \, \big( \gamma + \partial \beta \big) (\ell_n , \ell_{-n})
+ \frac{r}{12} (n+1) n (n-1) (n-2) .
\end{aligned}
where in the seciond step we used the induction hypothesis. Since 2-n \ne 0, this can
be solved for
\begin{aligned}
\big( \gamma + \partial \beta \big) (\ell_n , \ell_{-n})
= \; & - \frac{r}{12} \frac{(n+1) n (n-1) (n-2)}{2-n} = r \frac{n^3 - n}{12} ,
\end{aligned}
completing the induction step.
Witt algebra 2-cohomology is spanned by the Virasoro cocycle.
The Lie algebra 2-cohomology \Coh^2(\witt,\bbk) of the Witt
algebra \witt with coefficients in \bbk is one-dimensional
and spanned by the class of the Virasoro cocycle {\gamma}_{\vir},
\begin{aligned}
\Coh^2(\witt,\bbk) \; = \; \bbk \cdot [{\gamma}_{\vir}] .
\end{aligned}
Lean code for Lemma4.3.4●1 theorem
Associated Lean declarations
-
theoremdefined in VirasoroProject/WittAlgebraCohomology.leancomplete
theorem VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.rank 𝕜 (VirasoroProject.LieTwoCohomology 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) = 1
theorem VirasoroProject.WittAlgebra.rank_lieTwoCohomology_eq_one.{u_1} (𝕜 : Type u_1) [Field 𝕜] [CharZero 𝕜] : Module.rank 𝕜 (VirasoroProject.LieTwoCohomology 𝕜 (VirasoroProject.WittAlgebra 𝕜) 𝕜) = 1
The Lie algebra 2-cohomology of the Witt algebra is one-dimensional, `dim H²(WittAlgebra, 𝕜) = 1`.
This follows directly from Lemma 4.3.3 and Lemma 4.2.3.