VirasoroProject

2. Lie algebra cohomology in degree two🔗

Let \bbk be a field and let \gLie be a Lie algebra over \bbk. Fix also a vector space \aLie over \bbk, (interpreted, when necessary, as an abelian Lie algebra, i.e., all Lie brackets in \aLie are taken to be zero).

Definition2.1
uses 0used by 1✓L∃∀N

Cyclic triple sum. TO BE WRITTEN

Lean code for Definition2.1●2 definitions
  • defdefined in VirasoroProject/CyclicTripleSum.lean
    complete
    def VirasoroProject.cyclicTripleSum.{u_1, u_2} {V : Type u_1} {W : Type u_2}
  [Add W] (β : V → V → V) (φ : V → V → W) (x y z : V) : W
    def VirasoroProject.cyclicTripleSum.{u_1, u_2}
  {V : Type u_1} {W : Type u_2} [Add W]
  (β : V → V → V) (φ : V → V → W)
  (x y z : V) : W
    An auxiliary function for proofs of Jacobi identities etc.

Given functions β : V × V → V and φ : V × V → W where W has additive structure,
`cyclicTripleSum β φ` is the function of three variables on V defined by:
⟨x,y,z⟩ ↦ φ(x,β(y,z)) + φ(y,β(z,x)) + φ(z,β(x,y)).
  • defdefined in VirasoroProject/CyclicTripleSum.lean
    complete
    def VirasoroProject.cyclicTripleSumHom.{u_1, u_2, u_3} {V : Type u_1}
  {W : Type u_2} [AddCommMonoid V] [AddCommMonoid W] {𝕜 : Type u_3}
  [CommSemiring 𝕜] [Module 𝕜 V] [Module 𝕜 W] (β : V →ₗ[𝕜] V →ₗ[𝕜] V)
  (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) : V →ₗ[𝕜] V →ₗ[𝕜] V →ₗ[𝕜] W
    def VirasoroProject.cyclicTripleSumHom.{u_1,
    u_2, u_3}
  {V : Type u_1} {W : Type u_2}
  [AddCommMonoid V] [AddCommMonoid W]
  {𝕜 : Type u_3} [CommSemiring 𝕜]
  [Module 𝕜 V] [Module 𝕜 W]
  (β : V →ₗ[𝕜] V →ₗ[𝕜] V)
  (φ : V →ₗ[𝕜] V →ₗ[𝕜] W) :
  V →ₗ[𝕜] V →ₗ[𝕜] V →ₗ[𝕜] W
    An auxiliary trilinear map for proofs of Jacobi identities.

Given bilinear functions β : V × V → V and φ : V × V → W, `cyclicTripleSumHom β φ` is the
trilinear function on V defined by: ⟨x,y,z⟩ ↦ φ(x,β(y,z)) + φ(y,β(z,x)) + φ(z,β(x,y)).
Definition2.2
uses 0used by 1✓L∃∀N

Lie algebra 1-cochain. A 1-cochain of the Lie algebra \gLie with coefficients in the vector space \aLie is a linear map

\begin{aligned} \beta \colon \gLie \to \aLie . \end{aligned}

The set of all such 1-cochains is denoted by \Coch^1(\gLie, \aLie).

Lean code for Definition2.2●1 definition
  • structure(1 field)defined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    structure VirasoroProject.LieOneCochain.{u, u_1} (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] : Type u
    structure VirasoroProject.LieOneCochain.{u, u_1}
  (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] : Type u
    Lie algebra 1-cochains.

    Fields

    toLinearMap : 𝓰 →ₗ[𝕜] 𝓪
    The underlying linear map of a Lie algebra 1-cochain.
Definition2.3
uses 0
Used by 7
Reverse dependency previews
Preview
Lemma 2.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Lie algebra 2-cocycle. A 2-cocycle of the Lie algebra \gLie with coefficients in the vector space \aLie is a bilinear map

\begin{aligned} \gamma \colon \gLie \times \gLie \to \aLie \end{aligned}

such that for all X \in \gLie we have the antisymmetry condition

\begin{aligned} \gamma(X,X) = \; & 0 \end{aligned}

and for all X,Y,Z \in \gLie we have the Leibnitz rule

\begin{aligned} \gamma(X,[Y,Z]) = \; & \gamma([X,Y],Z) + \gamma(Y,[X,Z]) . \end{aligned}

The set of all such 2-cocycles is denoted by \Coc^2(\gLie, \aLie).

Lean code for Definition2.3●1 definition
  • structure(3 fields)defined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    structure VirasoroProject.LieTwoCocycle.{u, u_1} (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] : Type u
    structure VirasoroProject.LieTwoCocycle.{u, u_1}
  (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] : Type u
    Lie algebra 2-cocycles.

    Fields

    toBilin : 𝓰 →ₗ[𝕜] 𝓰 →ₗ[𝕜] 𝓪
    The underlying bilinear map of a Lie algebra 2-cocycle. 
    self' : ∀ (X : 𝓰), (self.toBilin X) X = 0
    leibniz' : ∀ (X Y Z : 𝓰), (self.toBilin X) ⁅Y, Z⁆ = (self.toBilin ⁅X, Y⁆) Z + (self.toBilin Y) ⁅X, Z⁆
Lemma2.4
uses 1used by 1✓L∃∀N

Skew-symmetry of 2-cocycles. For any \gamma \in \Coc^2(\gLie,\aLie) and any X,Y \in \gLie, we have the skew-symmetry property

\begin{aligned} \gamma(X,Y) = - \gamma(Y,X) . \end{aligned}

Lean code for Lemma2.4●1 theorem
  • theoremdefined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    theorem VirasoroProject.LieTwoCocycle.skew.{u, u_1} {𝕜 : Type u_1} [CommRing 𝕜]
  {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) (X Y : 𝓰) :
  -(γ Y) X = (γ X) Y
    theorem VirasoroProject.LieTwoCocycle.skew.{u,
    u_1}
  {𝕜 : Type u_1} [CommRing 𝕜]
  {𝓰 𝓪 : Type u} [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪]
  (γ :
    VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪)
  (X Y : 𝓰) : -(γ Y) X = (γ X) Y
Proof for Lemma 2.4
uses 0

The Leibnitz rule applied to X+Y gives

\begin{aligned} 0 = \; & \gamma(X+Y,X+Y) \\ = \; & \gamma(X,X) + \gamma(X,Y) + \gamma(Y,X) + \gamma(Y,Y) \end{aligned}

by bilinearity of \gamma. The first and the last terms in the last expression vanish by antisymmetry, and the asserted skew-symmetry equation follows.

Lemma2.5
uses 1used by 1✓L∃∀N

Lie algebra 1-cochains form a vector space. The set \Coch^1(\gLie, \aLie) of 1-cochains of \gLie with coefficients in \aLie forms a vector space over \bbk.

Lean code for Lemma2.5●1 definition
  • defdefined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    def VirasoroProject.LieOneCochain.instModule.{u, u_1} (𝕜 : Type u_1)
  [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪]
  [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :
  Module 𝕜 (VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪)
    def VirasoroProject.LieOneCochain.instModule.{u,
    u_1}
  (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] :
  Module 𝕜
    (VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪)
Proof for Lemma 2.5
uses 0

By definition, \Coch^1(\gLie, \aLie) is the space of linear maps \gLie \to \aLie, and such linear maps form a vector space.

Lemma2.6
uses 1used by 1✓L∃∀N

Lie algebra 2-cocycles form a vector space. The set \Coc^2(\gLie, \aLie) of 2-cocycles of \gLie with coefficients in \aLie forms a vector space over \bbk.

Lean code for Lemma2.6●1 definition
  • defdefined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    def VirasoroProject.LieTwoCocycle.instModule.{u, u_1} {𝕜 : Type u_1}
  [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪]
  [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :
  Module 𝕜 (VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪)
    def VirasoroProject.LieTwoCocycle.instModule.{u,
    u_1}
  {𝕜 : Type u_1} [CommRing 𝕜]
  {𝓰 𝓪 : Type u} [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] :
  Module 𝕜
    (VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪)
Proof for Lemma 2.6
uses 0

The conditions defining \Coc^2(\gLie, \aLie) are linear, so this is staightforward.

Definition2.7
Statement uses 2
Statement dependency previews
Preview
Lemma 2.5
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Definition 2.8
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Lie algebra 2-coboundary. Given a 1-cochain \beta \in \Coch^1(\gLie, \aLie), we define the coboundary \partial \beta of \beta to be the bilinear map

\begin{aligned} \partial \beta \colon \; & \gLie \times \gLie \to \aLie \\ \end{aligned}

given by

\begin{aligned} \partial \beta (X, Y) = \; & \beta ([X,Y]) . \end{aligned}

We then have \partial \beta \in \Coc^2(\gLie,\aLie). The mapping \partial \colon \Coch^1(\gLie,\aLie) \to \Coc^2(\gLie,\aLie) is linear. Its range is denoted \Cob^2(\gLie,\aLie) \subset \Coc^2(\gLie,\aLie) and called the set of 2-coboundaries of the Lie algebra \gLie with coefficients in \aLie.

Lean code for Definition2.7●1 definition
  • defdefined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    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.
Definition2.8
uses 1
Used by 5
Reverse dependency previews
Preview
Lemma 2.9
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Lie algebra 2-cohomology. The vector space

\begin{aligned} \Coh^2(\gLie,\aLie) := \Coc^2(\gLie,\aLie) \, / \, \Cob^2(\gLie,\aLie) \end{aligned}

is called the Lie algebra cohomology in degree 2 of \gLie with coefficients in \aLie.

Lean code for Definition2.8●1 definition
  • defdefined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    def VirasoroProject.LieTwoCohomology.{u, u_1} (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] : Type u
    def VirasoroProject.LieTwoCohomology.{u, u_1}
  (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] : Type u
    The 2-cohomology `H²(𝓰,𝓪)` of a Lie algebra `𝓰` with coefficients in `𝓪`.
Lemma2.9
uses 1used by 0✓L∃∀N

Cohomology of abelian Lie algebras. If \gLie is abelian, i.e., [\gLie,\gLie] = 0, then the canonical projection

\begin{aligned} \Coc^2(\gLie,\aLie) \to \Coh^2(\gLie,\aLie) \end{aligned}

is a linear isomorphism.

Lean code for Lemma2.9●1 theorem
  • theoremdefined in VirasoroProject/LieCohomologySmallDegree.lean
    complete
    theorem VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap.{u,
    u_1}
  (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] [IsLieAbelian 𝓰] :
  ↑(VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv 𝕜 𝓰 𝓪) =
    VirasoroProject.LieTwoCocycle.toLieTwoCohomology 𝕜 𝓰 𝓪
    theorem VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap.{u,
    u_1}
  (𝕜 : Type u_1) [CommRing 𝕜]
  (𝓰 𝓪 : Type u) [LieRing 𝓰]
  [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰]
  [Module 𝕜 𝓪] [IsLieAbelian 𝓰] :
  ↑(VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv
        𝕜 𝓰 𝓪) =
    VirasoroProject.LieTwoCocycle.toLieTwoCohomology
      𝕜 𝓰 𝓪
Proof for Lemma 2.9
uses 0

The projection is surjective by construction, so it suffices to show that it is also injective. The kernel of the projection is \Cob^2(\gLie,\aLie) = \Ima \; \partial. In view of Definition 2.7, abelianity of \gLie implies \partial \beta = 0 for any \beta \in \Coch^1(\gLie,\aLie). Therefore \Cob^2(\gLie,\aLie) = 0, and the kernel of the projection is trivial, so the projection is indeed injective.