Documentation

LeanPool.VirasoroProject.LieCohomologySmallDegree

Lie algebra cohomology in degree two (for central extensions) #

(WARNING: This file needs cleaning up. It was not the main goal and it was the first time I tried to use multilinear maps in Lean.)

This file defines Lie algebra 2-cocycles and 2-coboundaries and constructs the Lie algebra cohomology in degree two, with coefficients in a vector space (an Abelian Lie algebra).

Main definitions #

LieOneCochain: The set C¹(𝓰,𝓪) of 1-cochains of a Lie algebra 𝓰 with coefficients in a vector space 𝓪.
LieTwoCocycle: The set Z²(𝓰,𝓪) of 2-cocycles of a Lie algebra 𝓰 with coefficients in a vector space 𝓪.
LieTwoCoboundary: The subspace B²(𝓰,𝓪) ⊆ Z²(𝓰,𝓪) of 2-coboundaries.
LieTwoCohomology: The 2-cohomology H²(𝓰,𝓪) := Z²(𝓰,𝓪) ⧸ B²(𝓰,𝓪) of a Lie algebra 𝓰 with coefficients in a vector space 𝓪.

Main statements #

LieTwoCocycle.toLieTwoCohomologyEquiv: If 𝓰 is abelian, then the canonical projection from 2-cocycles to 2-cohomologies is a linear isomorphism.

Implementation notes #

This file needs some clean-up! (But it works for the purposes of concrete calculations of central extensions etc.)

A reasonable thing to do would be to define Lie algebra cohomology in general degrees. But for concrete applications, the special case of degree two probably deserves its own API. Once a general definition is made, the API for the degree 2 case (especially central extensions) could be refactored.

Tags #

Lie algebra, cohomology

Lie algebra 1-cochains #

structure VirasoroProject.LieOneCochain (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Lie algebra 1-cochains.

toLinearMap : 𝓰 →ₗ[𝕜] 𝓪
The underlying linear map of a Lie algebra 1-cochain.

Instances For

theorem VirasoroProject.LieOneCochain.ext {𝕜 : Type u_1} {inst✝ : CommRing 𝕜} {𝓰 𝓪 : Type u} {inst✝¹ : LieRing 𝓰} {inst✝² : AddCommGroup 𝓪} {inst✝³ : LieAlgebra 𝕜 𝓰} {inst✝⁴ : Module 𝕜 𝓪} {x y : LieOneCochain 𝕜 𝓰 𝓪} (toLinearMap : x.toLinearMap = y.toLinearMap) :

x = y

theorem VirasoroProject.LieOneCochain.ext_iff {𝕜 : Type u_1} {inst✝ : CommRing 𝕜} {𝓰 𝓪 : Type u} {inst✝¹ : LieRing 𝓰} {inst✝² : AddCommGroup 𝓪} {inst✝³ : LieAlgebra 𝕜 𝓰} {inst✝⁴ : Module 𝕜 𝓪} {x y : LieOneCochain 𝕜 𝓰 𝓪} :

x = y ↔ x.toLinearMap = y.toLinearMap

@[implicit_reducible]

instance VirasoroProject.instZeroLieOneCochain (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Zero (LieOneCochain 𝕜 𝓰 𝓪)

Equations

VirasoroProject.instZeroLieOneCochain 𝕜 𝓰 𝓪 = { zero := { toLinearMap := 0 } }

@[implicit_reducible]

instance VirasoroProject.instAddLieOneCochain (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Add (LieOneCochain 𝕜 𝓰 𝓪)

Equations

VirasoroProject.instAddLieOneCochain 𝕜 𝓰 𝓪 = { add := fun (β β' : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪) => { toLinearMap := β.toLinearMap + β'.toLinearMap } }

@[implicit_reducible]

instance VirasoroProject.instSMulLieOneCochain (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

SMul 𝕜 (LieOneCochain 𝕜 𝓰 𝓪)

Equations

VirasoroProject.instSMulLieOneCochain 𝕜 𝓰 𝓪 = { smul := fun (c : 𝕜) (β : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪) => { toLinearMap := c • β.toLinearMap } }

@[simp]

theorem VirasoroProject.LieOneCochain.toLinearMap_zero (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

toLinearMap 0 = 0

@[simp]

theorem VirasoroProject.LieOneCochain.toLinearMap_add (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (β β' : LieOneCochain 𝕜 𝓰 𝓪) :

(β + β').toLinearMap = β.toLinearMap + β'.toLinearMap

@[simp]

theorem VirasoroProject.LieOneCochain.toLinearMap_smul (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (c : 𝕜) (β : LieOneCochain 𝕜 𝓰 𝓪) :

(c • β).toLinearMap = c • β.toLinearMap

@[implicit_reducible]

instance VirasoroProject.LieOneCochain.instAddCommMonoid (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

AddCommMonoid (LieOneCochain 𝕜 𝓰 𝓪)

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VirasoroProject.LieOneCochain.instModule (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Module 𝕜 (LieOneCochain 𝕜 𝓰 𝓪)

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VirasoroProject.LieOneCochain.instAddCommGroup (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

AddCommGroup (LieOneCochain 𝕜 𝓰 𝓪)

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VirasoroProject.LieOneCochain.instFunLike {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

FunLike (LieOneCochain 𝕜 𝓰 𝓪) 𝓰 𝓪

Equations

VirasoroProject.LieOneCochain.instFunLike = { coe := fun (β : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪) (X : 𝓰) => β.toLinearMap X, coe_injective := ⋯ }

instance VirasoroProject.LieOneCochain.instLinearMapClass {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

LinearMapClass (LieOneCochain 𝕜 𝓰 𝓪) 𝕜 𝓰 𝓪

Lie algebra 2-cocycles #

structure VirasoroProject.LieTwoCocycle (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Lie algebra 2-cocycles.

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⁆

Instances For

theorem VirasoroProject.LieTwoCocycle.ext {𝕜 : Type u_1} {inst✝ : CommRing 𝕜} {𝓰 𝓪 : Type u} {inst✝¹ : LieRing 𝓰} {inst✝² : AddCommGroup 𝓪} {inst✝³ : LieAlgebra 𝕜 𝓰} {inst✝⁴ : Module 𝕜 𝓪} {x y : LieTwoCocycle 𝕜 𝓰 𝓪} (toBilin : x.toBilin = y.toBilin) :

x = y

theorem VirasoroProject.LieTwoCocycle.ext_iff {𝕜 : Type u_1} {inst✝ : CommRing 𝕜} {𝓰 𝓪 : Type u} {inst✝¹ : LieRing 𝓰} {inst✝² : AddCommGroup 𝓪} {inst✝³ : LieAlgebra 𝕜 𝓰} {inst✝⁴ : Module 𝕜 𝓪} {x y : LieTwoCocycle 𝕜 𝓰 𝓪} :

x = y ↔ x.toBilin = y.toBilin

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instFunLikeLinearMapId (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

FunLike (LieTwoCocycle 𝕜 𝓰 𝓪) 𝓰 (𝓰 →ₗ[𝕜] 𝓪)

Equations

VirasoroProject.LieTwoCocycle.instFunLikeLinearMapId 𝕜 𝓰 𝓪 = { coe := fun (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) (X : 𝓰) => γ.toBilin X, coe_injective := ⋯ }

instance VirasoroProject.LieTwoCocycle.instLinearMapClassLinearMapId (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

LinearMapClass (LieTwoCocycle 𝕜 𝓰 𝓪) 𝕜 𝓰 (𝓰 →ₗ[𝕜] 𝓪)

@[simp]

theorem VirasoroProject.LieTwoCocycle.self {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) {X : 𝓰} :

(γ X) X = 0

theorem VirasoroProject.LieTwoCocycle.leibniz {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) {X Y Z : 𝓰} :

(γ X) ⁅Y, Z⁆ = (γ ⁅X, Y⁆) Z + (γ Y) ⁅X, Z⁆

theorem VirasoroProject.LieTwoCocycle.apply_add {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (X₁ X₂ Y : 𝓰) :

(γ (X₁ + X₂)) Y = (γ X₁) Y + (γ X₂) Y

theorem VirasoroProject.LieTwoCocycle.apply_add₂ {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (X Y₁ Y₂ : 𝓰) :

(γ X) (Y₁ + Y₂) = (γ X) Y₁ + (γ X) Y₂

theorem VirasoroProject.LieTwoCocycle.apply_smul {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (c : 𝕜) (X Y : 𝓰) :

(γ (c • X)) Y = c • (γ X) Y

theorem VirasoroProject.LieTwoCocycle.apply_smul₂ {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (c : 𝕜) (X Y : 𝓰) :

(γ X) (c • Y) = c • (γ X) Y

theorem VirasoroProject.LieTwoCocycle.skew {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (X Y : 𝓰) :

-(γ Y) X = (γ X) Y

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instZero {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Zero (LieTwoCocycle 𝕜 𝓰 𝓪)

Equations

VirasoroProject.LieTwoCocycle.instZero = { zero := { toBilin := 0, self' := ⋯, leibniz' := ⋯ } }

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instAdd {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Add (LieTwoCocycle 𝕜 𝓰 𝓪)

Equations

VirasoroProject.LieTwoCocycle.instAdd = { add := fun (γ γ' : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) => { toBilin := γ.toBilin + γ'.toBilin, self' := ⋯, leibniz' := ⋯ } }

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instSMul {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

SMul 𝕜 (LieTwoCocycle 𝕜 𝓰 𝓪)

Equations

VirasoroProject.LieTwoCocycle.instSMul = { smul := fun (c : 𝕜) (γ : VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪) => { toBilin := c • γ.toBilin, self' := ⋯, leibniz' := ⋯ } }

@[simp]

theorem VirasoroProject.LieTwoCocycle.toBilin_zero {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

@[simp]

theorem VirasoroProject.LieTwoCocycle.toBilin_add {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ γ' : LieTwoCocycle 𝕜 𝓰 𝓪) :

(γ + γ').toBilin = γ.toBilin + γ'.toBilin

@[simp]

theorem VirasoroProject.LieTwoCocycle.toBilin_smul {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (c : 𝕜) (γ : LieTwoCocycle 𝕜 𝓰 𝓪) :

(c • γ).toBilin = c • γ.toBilin

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instAddCommMonoid {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

AddCommMonoid (LieTwoCocycle 𝕜 𝓰 𝓪)

Equations

One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instModule {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Module 𝕜 (LieTwoCocycle 𝕜 𝓰 𝓪)

Equations

VirasoroProject.LieTwoCocycle.instModule = { toSMul := VirasoroProject.LieTwoCocycle.instSMul, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

@[implicit_reducible]

instance VirasoroProject.LieTwoCocycle.instAddCommGroup {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

AddCommGroup (LieTwoCocycle 𝕜 𝓰 𝓪)

Equations

One or more equations did not get rendered due to their size.

theorem VirasoroProject.LieTwoCocycle.add_apply {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ₁ γ₂ : LieTwoCocycle 𝕜 𝓰 𝓪) (X Y : 𝓰) :

((γ₁ + γ₂) X) Y = (γ₁ X) Y + (γ₂ X) Y

theorem VirasoroProject.LieTwoCocycle.smul_apply {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (c : 𝕜) (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (X Y : 𝓰) :

((c • γ) X) Y = c • (γ X) Y

theorem VirasoroProject.LieTwoCocycle.sub_apply {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ₁ γ₂ : LieTwoCocycle 𝕜 𝓰 𝓪) (X Y : 𝓰) :

((γ₁ - γ₂) X) Y = (γ₁ X) Y - (γ₂ X) Y

@[simp]

theorem VirasoroProject.LieTwoCocycle.zero_apply {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (X Y : 𝓰) :

(0 X) Y = 0

@[simp]

theorem VirasoroProject.LieTwoCocycle.zero_apply' {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (X : 𝓰) :

0 X = 0

Lie algebra 2-coboundaries #

def VirasoroProject.LieOneCochain.bdry' {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (β : LieOneCochain 𝕜 𝓰 𝓪) :

𝓰 →ₗ[𝕜] 𝓰 →ₗ[𝕜] 𝓪

A Lie algebra 1-cochain determines a bilinear map via the differential.

Equations

β.bdry' = { toFun := fun (X : 𝓰) => ↑β ∘ₗ (LieAlgebra.bracketHom 𝕜 𝓰) X, map_add' := ⋯, map_smul' := ⋯ }

Instances For

def VirasoroProject.LieOneCochain.bdryHom' {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

LieOneCochain 𝕜 𝓰 𝓪 →ₗ[𝕜] 𝓰 →ₗ[𝕜] 𝓰 →ₗ[𝕜] 𝓪

A Lie algebra 1-cochain linearly determines a bilinear map via the differential.

Equations

VirasoroProject.LieOneCochain.bdryHom' = { toFun := fun (β : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪) => β.bdry', map_add' := ⋯, map_smul' := ⋯ }

Instances For

def VirasoroProject.LieOneCochain.bdry {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (β : LieOneCochain 𝕜 𝓰 𝓪) :

LieTwoCocycle 𝕜 𝓰 𝓪

The ∂ of a Lie algebra 1-cochain as a Lie algebra 2-cocycle.

Equations

β.bdry = { toBilin := VirasoroProject.LieOneCochain.bdryHom' β, self' := ⋯, leibniz' := ⋯ }

Instances For

def VirasoroProject.LieOneCochainBdryHom (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

LieOneCochain 𝕜 𝓰 𝓪 →ₗ[𝕜] LieTwoCocycle 𝕜 𝓰 𝓪

The ∂ as a linear map from Lie algebra 1-cochains to Lie algebra 2-cocycles.

Equations

VirasoroProject.LieOneCochainBdryHom 𝕜 𝓰 𝓪 = { toFun := fun (β : VirasoroProject.LieOneCochain 𝕜 𝓰 𝓪) => β.bdry, map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[simp]

theorem VirasoroProject.LieOneCochain.neg_bdry (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (β : LieOneCochain 𝕜 𝓰 𝓪) :

(-β).bdry = -β.bdry

theorem VirasoroProject.LieOneCochain.bdry_apply (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (β : LieOneCochain 𝕜 𝓰 𝓪) (X Y : 𝓰) :

(β.bdry X) Y = β ⁅X, Y⁆

@[reducible, inline]

abbrev VirasoroProject.LieTwoCoboundary (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Submodule 𝕜 (LieTwoCocycle 𝕜 𝓰 𝓪)

Lie algebra 2-coboundaries as a vector space.

Equations

VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪 = (VirasoroProject.LieOneCochainBdryHom 𝕜 𝓰 𝓪).range

Instances For

Lie algebra 2-cohomology #

def VirasoroProject.LieTwoCohomology (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

The 2-cohomology H²(𝓰,𝓪) of a Lie algebra 𝓰 with coefficients in 𝓪.

Equations

VirasoroProject.LieTwoCohomology 𝕜 𝓰 𝓪 = (VirasoroProject.LieTwoCocycle 𝕜 𝓰 𝓪 ⧸ VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪)

Instances For

@[implicit_reducible]

instance VirasoroProject.LieTwoCohomology.instAddCommGroup (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

AddCommGroup (LieTwoCohomology 𝕜 𝓰 𝓪)

The 2-cohomology H²(𝓰,𝓪) is an additive commutative group.

Equations

VirasoroProject.LieTwoCohomology.instAddCommGroup 𝕜 𝓰 𝓪 = Submodule.Quotient.addCommGroup (VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪)

@[implicit_reducible]

instance VirasoroProject.LieTwoCohomology.instModule (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

Module 𝕜 (LieTwoCohomology 𝕜 𝓰 𝓪)

The 2-cohomology H²(𝓰,𝓪) is a module over the scalar ring 𝕜.

Equations

VirasoroProject.LieTwoCohomology.instModule 𝕜 𝓰 𝓪 = Submodule.Quotient.module' (VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪)

def VirasoroProject.LieTwoCocycle.toLieTwoCohomology (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

LieTwoCocycle 𝕜 𝓰 𝓪 →ₗ[𝕜] LieTwoCohomology 𝕜 𝓰 𝓪

The linear map from 2-cocycles to 2-cohomologies of a Lie algebra 𝓰 with coefficients in 𝓪.

Equations

VirasoroProject.LieTwoCocycle.toLieTwoCohomology 𝕜 𝓰 𝓪 = (VirasoroProject.LieTwoCoboundary 𝕜 𝓰 𝓪).mkQ

Instances For

theorem VirasoroProject.LieTwoCocycle.range_toLieTwoCohomology_eq_top (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] :

(toLieTwoCohomology 𝕜 𝓰 𝓪).range = ⊤

def VirasoroProject.LieTwoCocycle.cohomologyClass {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) :

LieTwoCohomology 𝕜 𝓰 𝓪

The projection to 2-cohomologies from 2-cocycles of a Lie algebra 𝓰 with coefficients in 𝓪. (This definition is to enable dot notation, while the linear map version doesn't.)

Equations

γ.cohomologyClass = (VirasoroProject.LieTwoCocycle.toLieTwoCohomology 𝕜 𝓰 𝓪) γ

Instances For

theorem VirasoroProject.LieTwoCocycle.cohomologyClass_add_bdry {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (β : LieOneCochain 𝕜 𝓰 𝓪) :

(γ + β.bdry).cohomologyClass = γ.cohomologyClass

Adding a coboundary does not change the cohomology class.

theorem VirasoroProject.LieTwoCocycle.exists_eq_bdry {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (hγ : γ.cohomologyClass = 0) :

∃ (β : LieOneCochain 𝕜 𝓰 𝓪), γ = β.bdry

A cocycle representing a trivial cohomology class is a coboundary.

theorem VirasoroProject.LieOneCochain.bdry_apply_eq_zero_of_isLieAbelian {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] [IsLieAbelian 𝓰] (β : LieOneCochain 𝕜 𝓰 𝓪) (X Y : 𝓰) :

(β.bdry X) Y = 0

For abelian Lie algebras, a 2-coboundary is necessarily zero.

theorem VirasoroProject.LieTwoCoboundary.eq_bot_of_isLieAbelian (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] [IsLieAbelian 𝓰] :

LieTwoCoboundary 𝕜 𝓰 𝓪 = ⊥

For abelian Lie algebras, the space of 2-coboundaries is the zero vector space.

theorem VirasoroProject.LieTwoCocycle.ker_toLieTwoCohomology_eq_bot_of_isLieAbelian (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] [IsLieAbelian 𝓰] :

(toLieTwoCohomology 𝕜 𝓰 𝓪).ker = ⊥

For abelian Lie algebras, the map from 2-cocycles to their cohomology classes has trivial kernel.

noncomputable def VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] [IsLieAbelian 𝓰] :

LieTwoCocycle 𝕜 𝓰 𝓪 ≃ₗ[𝕜] LieTwoCohomology 𝕜 𝓰 𝓪

For abelian Lie algebras, the map from 2-cocycles to their cohomology classes is a linear equivalence.

Equations

VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv 𝕜 𝓰 𝓪 = LinearEquiv.ofBijective (VirasoroProject.LieTwoCocycle.toLieTwoCohomology 𝕜 𝓰 𝓪) ⋯

Instances For

theorem VirasoroProject.LieTwoCocycle.toLieTwoCohomologyEquiv_toLinearMap (𝕜 : Type u_1) [CommRing 𝕜] (𝓰 𝓪 : Type u) [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] [IsLieAbelian 𝓰] :

↑(toLieTwoCohomologyEquiv 𝕜 𝓰 𝓪) = toLieTwoCohomology 𝕜 𝓰 𝓪