3.2. Central extensions determined by 2-cocycles
Central extension determined by a cocycle.
Given a Lie algebra 2-cocycle \gamma \in C^2(\gLie,\aLie),
on the vector space
\begin{aligned}
\egLie_\gamma = \gLie \oplus \aLie
\end{aligned}
define a bracket by
\begin{aligned}
[(X, A), (Y, B)]_{\gamma} := \big([X, Y]_{\gLie}, \gamma(X, Y) \big) .
\end{aligned}
Then \egLie_\gamma becomes a Lie algebra with the Lie bracket
[\cdot,\cdot]_{\gamma}.
Lean code for Definition3.2.1●2 definitions
Associated Lean declarations
-
defdefined in VirasoroProject/CentralExtension.leancomplete
def VirasoroProject.LieTwoCocycle.CentralExtension.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) : Type u
def VirasoroProject.LieTwoCocycle.CentralExtension.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) : Type u
The underlying type of the central extension of Lie algebras determined by a Lie algebra 2-cocycle.
-
defdefined in VirasoroProject/CentralExtension.leancomplete
def VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) : LieAlgebra 𝕜 γ.CentralExtension
def VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) : LieAlgebra 𝕜 γ.CentralExtension
The central extension is a Lie algebra.
Central extension determined by cohomologous cocycles.
Let \gamma_1, \gamma_2 \in C^2(\gLie,\aLie) be two Lie algebra 2-cocycles
and \egLie_{\gamma_1}, \egLie_{\gamma_2} the central extensions corresponding
to these according to Definition 3.2.1.
If the two 2-cocycles differ by a coboundary,
\gamma_2 - \gamma_1 = \partial \beta with some \beta \in C^1(\gLie,\aLie),
then the mapping \egLie_{\gamma_1} \to \egLie_{\gamma_2} given by
\begin{aligned}
(X,A) \mapsto \big( X, A + \beta(X) \big)
\end{aligned}
is an isomophism of Lie algebras \egLie_{\gamma_1} \cong \egLie_{\gamma_2}.
Lean code for Lemma3.2.2●2 definitions
Associated Lean declarations
-
defdefined in VirasoroProject/LieCohomologySmallDegree.leancomplete
def VirasoroProject.LieOneCochain_bdryHom.{u, u_1} (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪 →ₗ[𝕜] VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪
def VirasoroProject.LieOneCochain_bdryHom.{u, u_1} (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪 →ₗ[𝕜] VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪
The `∂` as a linear map from Lie algebra 1-cochains to Lie algebra 2-cocycles.
-
defdefined in VirasoroProject/CentralExtension.leancomplete
def VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) {γ' : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪} (h : γ' - γ ∈ VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪) : γ.CentralExtension ≃ₗ⁅𝕜⁆ γ'.CentralExtension
def VirasoroProject.LieTwoCocycle.CentralExtension.equiv_of_lieTwoCoboundary.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) {γ' : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪} (h : γ' - γ ∈ VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪) : γ.CentralExtension ≃ₗ⁅𝕜⁆ γ'.CentralExtension
A Lie algebra isomorphism between two central extensions determined by cocycles which differ by a coboundary.
The mapping \phi_\beta \colon \egLie_1 \to \egLie_2 given by
\begin{aligned}
\phi_\beta\big((X,A)\big) := \big( X, A + \beta(X) \big)
\end{aligned}
is clearly linear. It is also bijective, since the similarly defined mapping
\phi_{-\beta} \colon \egLie_2 \to \egLie_1,
\phi_{-\beta}\big((X,A)\big) := \big( X, A - \beta(X) \big),
is a two-sided inverse to \phi_\beta.
So it remains to verify that this bijective linear map
\phi_\beta \colon \egLie_1 \to \egLie_2 is in fact a
homomorphism Lie algebras.
Let (X, A), (Y, B) \in \gLie \oplus \aLie = \egLie_{\gamma_1}.
The bracket in \egLie_{\gamma_1} of these is, by definition,
\begin{aligned}
[(X, A), (Y, B)]_{\gamma_1} := \big([X, Y]_{\gLie}, \gamma_1(X, Y) \big) .
\end{aligned}
Applying the mapping \phi_\beta to this, we get
\begin{aligned}
\phi_\beta \Big([(X, A), (Y, B)]_{\gamma_1} \Big)
= \big([X, Y]_{\gLie}, \gamma_1(X, Y) + \beta([X, Y]_{\gLie}) \big) .
\end{aligned}
On the other hand the Lie bracket in \egLie_2 of the images is
\begin{aligned}
& \big[ \phi_\beta\big(((X, A)\big), \phi_\beta\big((Y, B)\big) \big]_{\gamma_2} \\
= \; & \big[ \big( X, A + \beta(X) \big), \big( Y, B + \beta(Y) \big) \big]_{\gamma_2} \\
= \; & \Big( [X,Y]_{\gLie} , \gamma_2(X,Y) \Big) \\
= \; & \Big( [X,Y]_{\gLie} , \gamma_1(X,Y) + \beta([X, Y]_{\gLie}) \Big) .
\end{aligned}
From the equality of these two expressions we see that \phi_\beta
indeed is also a Lie algebra homomorphism.
Central extension determined by a cocycle is a central extension.
Given a Lie algebra 2-cocycle \gamma \in C^2(\gLie,\aLie),
consider the Lie algebra \egLie_\gamma = \gLie \oplus \aLie as
in Definition 3.2.1.
With the inclusion \iota \colon \aLie \to \gLie \oplus \aLie
in the second direct summand and the
projection \pi \colon \gLie \oplus \aLie \to \gLie to the first direct
summand, the Lie algebra \egLie_\gamma = \gLie \oplus \aLie becomes a central
extension of \gLie by \aLie, i.e., we have the short exact sequence
of Lie algebras
\begin{aligned}
0 \longrightarrow \aLie
\overset{\iota}{\longrightarrow} \egLie_\gamma
\overset{\pi}{\longrightarrow} \gLie
\longrightarrow 0 .
\end{aligned}
Lean code for Lemma3.2.3●1 theorem
Associated Lean declarations
-
theoremdefined in VirasoroProject/IsCentralExtension.leancomplete
theorem VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension.{u} {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [IsLieAbelian 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) : VirasoroProject.LieAlgebra.IsCentralExtension (VirasoroProject.LieTwoCocycle.CentralExtension.emb γ) (VirasoroProject.LieTwoCocycle.CentralExtension.proj γ)
theorem VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension.{u} {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [IsLieAbelian 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) : VirasoroProject.LieAlgebra.IsCentralExtension (VirasoroProject.LieTwoCocycle.CentralExtension.emb γ) (VirasoroProject.LieTwoCocycle.CentralExtension.proj γ)
If `𝓮` is the central extension of `𝓰` by `𝓪` defined by a 2-cocycle `γ ∈ Z²(𝓰,𝓪)`, then `𝓮` is a central extension of `𝓰` by `𝓪` in the sense that there is a short exact sequence `0 ⟶ 𝓪 ⟶ 𝓮 ⟶ 𝓰 ⟶ 0` where the two maps are `LieTwoCocycle.CentralExtension.emb` and `LieTwoCocycle.CentralExtension.proj` and the image of `𝓪` is contained in the centre of `𝓮`.
Clearly
\begin{aligned}
0 \longrightarrow \aLie
\overset{\iota}{\longrightarrow} \egLie_\gamma
\overset{\pi}{\longrightarrow} \gLie
\longrightarrow 0
\end{aligned}
is an exact sequence of vector spaces, and it is straightforward
to check with Definition 3.2.1
that \iota and \pi are Lie algebra homomorphisms.
Every cohomology class in H^2(\gLie, \aLie) determines a well-defined
isomorphism class of central extensions of the Lie algebra \gLie
by \aLie by the rule that the class [\gamma] \in H^2(\gLie, \aLie) of
a cocycle \gamma \in C^2(\gLie, \aLie) corresponds to the isomorphism
class of \egLie_\gamma (Definition 3.2.1).
This follows from Lemma 3.2.3 and Lemma 3.2.2.