Central extensions of Lie algebras defined by 2-cocycles

This file defines the central extension of a Lie algebra determined by a 2-cocycle. It is proven that two central extensions are isomorphic if the corresponding cocycles differ by a coboundary.

Main definitions

• LieTwoCocycle.CentralExtension: The central extension of a Lie algebra 𝓰 by an abelian Lie algebra 𝓪 defined by a 2-cocycle γ ∈ H²(𝓰,𝓪).
• LieTwoCocycle.CentralExtension.equivOfLieTwoCoboundary: An isomorphism between the central extensions defined by two 2-cocycles which differ by a coboundary.

Main statements

• LieTwoCocycle.CentralExtension.instLieAlgebra: The central extension defined by a 2-cocycle is a Lie algebra.

Implementation notes

LieTwoCocycle.CentralExtension is the concrete construction of a central extension. The defining property (characteristic predicate) of central extensions is IsCentralExtension (see the file IsCentralExtension.lean.)

Tags

Lie algebra, central extension, 2-cocycle

Lie algebra central extensions determined by 2-cocycles

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

The underlying type of the central extension of Lie algebras determined by a Lie algebra 2-cocycle.

Equations

• γ.CentralExtension = (𝓰 × 𝓪)

theorem VirasoroProject.LieTwoCocycle.CentralExtension.ext {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} {Z W : γ.CentralExtension} (hX : Z.1 = W.1) (hA : Z.2 = W.2) : Z = W

theorem VirasoroProject.LieTwoCocycle.CentralExtension.ext_iff {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} {Z W : γ.CentralExtension} : Z = W ↔ Z.1 = W.1 ∧ Z.2 = W.2

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

Coercion of an element in a central extension to a pair.

Equations

• Z.coeProd = Z

@[implicit_reducible]

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

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.instAddCommGroup = Prod.instAddCommGroup

@[implicit_reducible]

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

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.instModule = Prod.instModule

theorem VirasoroProject.LieTwoCocycle.CentralExtension.add_def {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} (Z₁ Z₂ : γ.CentralExtension) : Z₁ + Z₂ = (Z₁.1 + Z₂.1, Z₁.2 + Z₂.2)

theorem VirasoroProject.LieTwoCocycle.CentralExtension.smul_def {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} (c : 𝕜) (Z : γ.CentralExtension) : c • Z = (c • Z.1, c • Z.2)

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.add_fst {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} (Z W : γ.CentralExtension) : (Z + W).1 = Z.1 + W.1

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.add_snd {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} (Z W : γ.CentralExtension) : (Z + W).2 = Z.2 + W.2

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.smul_fst {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} (c : 𝕜) (Z : γ.CentralExtension) : (c • Z).1 = c • Z.1

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.smul_snd {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ : LieTwoCocycle 𝕜 𝓰 𝓪} (c : 𝕜) (Z : γ.CentralExtension) : (c • Z).2 = c • Z.2

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

The Lie bracket in a central extension defined by a Lie algebra 2-cocycle.

Equations

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

@[simp]

theorem VirasoroProject.LieTwoCocycle.bracket_apply {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z W : γ.CentralExtension) : (γ.bracket Z) W = (⁅Z.1, W.1⁆, (γ Z.1) W.1)

theorem VirasoroProject.LieTwoCocycle.bracket_self {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z : γ.CentralExtension) : (γ.bracket Z) Z = 0

theorem VirasoroProject.LieTwoCocycle.bracket_smul {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (c : 𝕜) (Z W : γ.CentralExtension) : (γ.bracket Z) (c • W) = c • (γ.bracket Z) W

theorem VirasoroProject.LieTwoCocycle.bracket_leibniz {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z W₁ W₂ : γ.CentralExtension) : (γ.bracket Z) ((γ.bracket W₁) W₂) = (γ.bracket ((γ.bracket Z) W₁)) W₂ + (γ.bracket W₁) ((γ.bracket Z) W₂)

@[implicit_reducible]

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

The central extension is a Lie ring.

Equations

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

@[implicit_reducible]

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

The central extension is a Lie algebra.

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.instLieAlgebra γ = { toModule := VirasoroProject.LieTwoCocycle.CentralExtension.instModule, lie_smul := ⋯ }

theorem VirasoroProject.LieTwoCocycle.CentralExtension.lie_def {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z W : γ.CentralExtension) : ⁅Z, W⁆ = (⁅Z.1, W.1⁆, (γ Z.1) W.1)

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.lie_fst {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z W : γ.CentralExtension) : ⁅Z, W⁆.1 = ⁅Z.1, W.1⁆

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.lie_snd {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z W : γ.CentralExtension) : ⁅Z, W⁆.2 = (γ Z.1) W.1

def VirasoroProject.LieOneCochain.bdryHom {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (β : LieOneCochain 𝕜 𝓰 𝓪) (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : γ.CentralExtension →ₗ⁅𝕜⁆ (γ + β.bdry).CentralExtension

A Lie algebra homomorphism between two central extensions determined by cocycles which differ by a coboundary.

Equations

• β.bdryHom γ = { toFun := fun (Z : γ.CentralExtension) => (Z.1, Z.2 + β Z.1), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

def VirasoroProject.LieTwoCocycle.CentralExtension.congr {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ₁ γ₂ : LieTwoCocycle 𝕜 𝓰 𝓪} (h : γ₁ = γ₂) : γ₁.CentralExtension ≃ₗ⁅𝕜⁆ γ₂.CentralExtension

Annoyingly the dependent types make it difficult to identify central extensions with equal but not definitionally equal cocycles (e.g. γ + (β₁ + β₂).bdry vs. (γ + β₁.bdry) + β₂.bdry). This isomorphism transports central extensions across equal cocycles.

Equations

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

theorem VirasoroProject.LieTwoCocycle.CentralExtension.congr_apply {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ₁ γ₂ : LieTwoCocycle 𝕜 𝓰 𝓪} (h : γ₁ = γ₂) (Z : γ₁.CentralExtension) : (congr h) Z = (Z.1, Z.2)

@[simp]

theorem VirasoroProject.LieTwoCocycle.CentralExtension.congr_trans {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ₁ γ₂ γ₃ : LieTwoCocycle 𝕜 𝓰 𝓪} (h₁₂ : γ₁ = γ₂) (h₂₃ : γ₂ = γ₃) : (congr h₁₂).trans (congr h₂₃) = congr ⋯

theorem VirasoroProject.LieTwoCocycle.CentralExtension.congr_congr_symm {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] {γ₁ γ₂ : LieTwoCocycle 𝕜 𝓰 𝓪} (h : γ₁ = γ₂) : (congr h).trans (congr ⋯) = LieEquiv.refl

theorem VirasoroProject.LieTwoCocycle.CentralExtension.hom_of_coboundary_refl {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : congr ⋯ = LieEquiv.refl

theorem VirasoroProject.LieTwoCocycle.CentralExtension.hom_of_coboundary_add {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ₁ γ₂ γ₃ : LieTwoCocycle 𝕜 𝓰 𝓪) (β₁ β₂ : LieOneCochain 𝕜 𝓰 𝓪) (h₂ : γ₁ + β₁.bdry = γ₂) (h₃ : γ₂ + β₂.bdry = γ₃) : ((congr h₃).comp (β₂.bdryHom γ₂)).comp ((congr h₂).comp (β₁.bdryHom γ₁)) = (congr ⋯).comp ((β₁ + β₂).bdryHom γ₁)

noncomputable def VirasoroProject.LieTwoCocycle.CentralExtension.equivOfLieTwoCoboundary {𝕜 : Type u_1} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [AddCommGroup 𝓪] [LieAlgebra 𝕜 𝓰] [Module 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) {γ' : LieTwoCocycle 𝕜 𝓰 𝓪} (h : γ' - γ ∈ LieTwoCoboundary 𝕜 𝓰 𝓪) : γ.CentralExtension ≃ₗ⁅𝕜⁆ γ'.CentralExtension

A Lie algebra isomorphism between two central extensions determined by cocycles which differ by a coboundary.

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.equivOfLieTwoCoboundary γ h = LieEquiv.mkOfCompEqId ⋯ ⋯