Abstract central extensions of Lie algebras (characteristic predicate)

This file defines the short exact sequence characteristic predicate for a central extension of a Lie algebra. It is proven that central extension defined by a 2-cocycle satisfy this characteristic predicate.

Main definitions

• LieAlgebra.IsCentralExtension: The abstract definition (characteristic predicate) of a central extension of a Lie algebra 𝓰 by an abelian Lie algebra 𝓪: there exists a short exact sequence 0 ⟶ 𝓪 ⟶ 𝓮 ⟶ 𝓰 ⟶ 0 of Lie algebras, where the image of 𝓪 is contained in the centre of 𝓮.
• LieTwoCocycle.CentralExtension.emb: Given a 2-cocycle γ ∈ Z²(𝓰,𝓪) and the correspondingly constructed central extension 𝓮, this is the map 𝓪 ⟶ 𝓮 in the short exact sequence.
• LieTwoCocycle.CentralExtension.proj: Given a 2-cocycle γ ∈ Z²(𝓰,𝓪) and the correspondingly constructed central extension 𝓮, this is the map 𝓮 ⟶ 𝓰 in the short exact sequence.

Main statements

• LieTwoCocycle.CentralExtension.isCentralExtension: The central extension defined by a 2-cocycle is a central extension in the abstract sense (it satisfies the characteristic predicate).

Tags

Lie algebra, central extension, short exact sequence

Lie algebra central extensions defined by short exact sequences

structure VirasoroProject.LieAlgebra.IsExtension {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 𝓮 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [LieRing 𝓮] [LieAlgebra 𝕜 𝓮] (i : 𝓪 →ₗ⁅𝕜⁆ 𝓮) (p : 𝓮 →ₗ⁅𝕜⁆ 𝓰) : Prop

An extension 𝓮 of a Lie algebra 𝓰 by a Lie algebra 𝓪 is a short exact sequence 0 ⟶ 𝓪 ⟶ 𝓮 ⟶ 𝓰 ⟶ 0. The structure LieAlgebra.IsExtension bundles the maps 𝓪 ⟶ 𝓮 and 𝓮 ⟶ 𝓰 together with their trivial kernel and full range, respectively, and the exactness in the middle.

• ker_eq_bot : i.ker = ⊥
• range_eq_top : p.range = ⊤
• exact : i.range = LieIdeal.toLieSubalgebra 𝕜 𝓮 p.ker

structure VirasoroProject.LieAlgebra.IsCentralExtension {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] {𝓮 : Type u} [LieRing 𝓮] [LieAlgebra 𝕜 𝓮] (i : 𝓪 →ₗ⁅𝕜⁆ 𝓮) (p : 𝓮 →ₗ⁅𝕜⁆ 𝓰) extends VirasoroProject.LieAlgebra.IsExtension i p : Prop

A central extension 𝓮 of a Lie algebra 𝓰 by a Lie algebra 𝓪 is an extension 0 ⟶ 𝓪 ⟶ 𝓮 ⟶ 𝓰 ⟶ 0 where the image of 𝓪 is contained in the centre of 𝓮.

• ker_eq_bot : i.ker = ⊥
• range_eq_top : p.range = ⊤
• exact : i.range = LieIdeal.toLieSubalgebra 𝕜 𝓮 p.ker
• central (A : 𝓪) (E : 𝓮) : ⁅i A, E⁆ = 0

Lie algebra central extensions defined by 2-cocycles

def VirasoroProject.LieTwoCocycle.CentralExtension.emb {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) [IsLieAbelian 𝓪] : 𝓪 →ₗ⁅𝕜⁆ γ.CentralExtension

If 𝓮 is the (central) extension of 𝓰 by 𝓪 defined by a 2-cocycle γ ∈ Z²(𝓰,𝓪), then LieTwoCocycle.CentralExtension.emb gives the corresponding embedding 𝓪 ⟶ 𝓮.

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.emb γ = { toFun := fun (A : 𝓪) => (0, A), map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

def VirasoroProject.LieTwoCocycle.CentralExtension.proj {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : γ.CentralExtension →ₗ⁅𝕜⁆ 𝓰

If 𝓮 is the (central) extension of 𝓰 by 𝓪 defined by a 2-cocycle γ ∈ Z²(𝓰,𝓪), then LieTwoCocycle.CentralExtension.proj gives the corresponding projection 𝓮 ⟶ 𝓰.

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.proj γ = { toFun := fun (x : γ.CentralExtension) => match x with | (X, snd) => X, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

theorem VirasoroProject.LieTwoCocycle.CentralExtension.range_proj_eq_top {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : (proj γ).range = ⊤

theorem VirasoroProject.LieTwoCocycle.CentralExtension.ker_emb_eq_bot {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) [IsLieAbelian 𝓪] : (emb γ).ker = ⊥

theorem VirasoroProject.LieTwoCocycle.CentralExtension.mem_range_emb_iff {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) [IsLieAbelian 𝓪] (Z : γ.CentralExtension) : Z ∈ (emb γ).range ↔ Z.1 = 0

theorem VirasoroProject.LieTwoCocycle.CentralExtension.mem_ker_proj_iff {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) (Z : γ.CentralExtension) : Z ∈ (proj γ).ker ↔ Z.1 = 0

theorem VirasoroProject.LieTwoCocycle.CentralExtension.range_emb_eq_ker_proj {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) [IsLieAbelian 𝓪] : (emb γ).range = LieIdeal.toLieSubalgebra 𝕜 γ.CentralExtension (proj γ).ker

theorem VirasoroProject.LieTwoCocycle.CentralExtension.isExtension {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) [IsLieAbelian 𝓪] : LieAlgebra.IsExtension (emb γ) (proj γ)

If 𝓮 is the (central) extension of 𝓰 by 𝓪 defined by a 2-cocycle γ ∈ Z²(𝓰,𝓪), then 𝓮 is an 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.

theorem VirasoroProject.LieTwoCocycle.CentralExtension.isCentralExtension {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [IsLieAbelian 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : LieAlgebra.IsCentralExtension (emb γ) (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 𝓮.

noncomputable def VirasoroProject.LieTwoCocycle.CentralExtension.stdSection {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : 𝓰 →ₗ[𝕜] γ.CentralExtension

A standard section of a Lie algebra central extension associated to a Lie 2-cocycle.

Equations

• VirasoroProject.LieTwoCocycle.CentralExtension.stdSection γ = { toFun := fun (X : 𝓰) => (X, 0), map_add' := ⋯, map_smul' := ⋯ }

theorem VirasoroProject.LieTwoCocycle.CentralExtension.stdSection_prop {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] (γ : LieTwoCocycle 𝕜 𝓰 𝓪) : ↑(proj γ) ∘ₗ stdSection γ = 1

noncomputable def VirasoroProject.LieAlgebra.IsExtension.basis {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 𝓮 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [LieRing 𝓮] [LieAlgebra 𝕜 𝓮] {i : 𝓪 →ₗ⁅𝕜⁆ 𝓮} {p : 𝓮 →ₗ⁅𝕜⁆ 𝓰} (ex : IsExtension i p) (σ : 𝓰 →ₗ[𝕜] 𝓮) (hσ : ↑p ∘ₗ σ = 1) {ιA ιG : Type u'} (basA : Module.Basis ιA 𝕜 𝓪) (basG : Module.Basis ιG 𝕜 𝓰) : Module.Basis (ιA ⊕ ιG) 𝕜 𝓮

A basis of a central extension of Lie algebras constructed from a section and bases of the extending Lie algebras.

Equations

• ex.basis σ hσ basA basG = sesBasis basA basG ⋯ ⋯ hσ

@[simp]

theorem VirasoroProject.LieAlgebra.IsExtension.basis_eq_of_left {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 𝓮 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [LieRing 𝓮] [LieAlgebra 𝕜 𝓮] {i : 𝓪 →ₗ⁅𝕜⁆ 𝓮} {p : 𝓮 →ₗ⁅𝕜⁆ 𝓰} (ex : IsExtension i p) (σ : 𝓰 →ₗ[𝕜] 𝓮) (hσ : ↑p ∘ₗ σ = 1) {ιA ιG : Type u'} (basA : Module.Basis ιA 𝕜 𝓪) (basG : Module.Basis ιG 𝕜 𝓰) (ia : ιA) : (ex.basis σ hσ basA basG) (Sum.inl ia) = i (basA ia)

@[simp]

theorem VirasoroProject.LieAlgebra.IsExtension.basis_eq_of_right {𝕜 : Type u} [CommRing 𝕜] {𝓰 𝓪 𝓮 : Type u} [LieRing 𝓰] [LieAlgebra 𝕜 𝓰] [LieRing 𝓪] [LieAlgebra 𝕜 𝓪] [LieRing 𝓮] [LieAlgebra 𝕜 𝓮] {i : 𝓪 →ₗ⁅𝕜⁆ 𝓮} {p : 𝓮 →ₗ⁅𝕜⁆ 𝓰} (ex : IsExtension i p) (σ : 𝓰 →ₗ[𝕜] 𝓮) (hσ : ↑p ∘ₗ σ = 1) {ιA ιG : Type u'} (basA : Module.Basis ιA 𝕜 𝓪) (basG : Module.Basis ιG 𝕜 𝓰) (ig : ιG) : (ex.basis σ hσ basA basG) (Sum.inr ig) = σ (basG ig)