Extensions of Lie algebras

This file defines extensions of Lie algebras, given by short exact sequences of Lie algebra homomorphisms. They are implemented in two ways: IsExtension is a Prop-valued class taking two homomorphisms as parameters, and Extension is a structure that includes the middle Lie algebra.

Because our sign convention for differentials is opposite that of Chevalley-Eilenberg, there is a change of signs in the "action" part of the Lie bracket.

Main definitions

• LieAlgebra.IsExtension: A Prop-valued class characterizing an extension of Lie algebras.
• LieAlgebra.Extension: A bundled structure giving an extension of Lie algebras.
• LieAlgebra.IsExtension.extension: A function that builds the bundled structure from the class.
• LieAlgebra.ofTwoCocycle: The Lie algebra built from a direct product, but whose bracket product is sheared by a 2-cocycle.
• LieAlgebra.Extension.ofTwoCocycle - The Lie algebra extension constructed from a 2-cocycle.

TODO

• IsCentral - central extensions
• Equiv - equivalence of extensions
• The 2-cocycle given by a linear splitting of an extension.
• The 2-coboundary from two linear splittings of an extension.

References

• Chevalley, Eilenberg, Cohomology Theory of Lie Groups and Lie Algebras
• N. Bourbaki, Lie Groups and Lie Algebras, Chapters 1--3

class LieAlgebra.IsExtension {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : Prop

A sequence of two Lie algebra homomorphisms is an extension if it is short exact.

• ker_eq_bot : i.ker = ⊥
• range_eq_top : p.range = ⊤
• exact : i.range = LieIdeal.toLieSubalgebra R L p.ker

theorem LieHom.range_eq_ker_iff {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] (i : N →ₗ⁅R⁆ L) (p : L →ₗ⁅R⁆ M) : i.range = LieIdeal.toLieSubalgebra R L p.ker ↔ Function.Exact ⇑i ⇑p

structure LieAlgebra.Extension (R : Type u_1) (N : Type u_2) (M : Type u_4) [CommRing R] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] : Type (max (max (max u_1 u_2) u_4) (u_5 + 1))

The type of all Lie extensions of M by N. That is, short exact sequences of R-Lie algebra homomorphisms 0 → N → L → M → 0 where R, M, and N are fixed.

• L : Type u_5

  The middle object in the sequence.

• instLieRing : LieRing self.L

  L is a Lie ring.

• instLieAlgebra : LieAlgebra R self.L

  L is a Lie algebra over R.

• incl : N →ₗ⁅R⁆ self.L

  The inclusion homomorphism N →ₗ⁅R⁆ L

• proj : self.L →ₗ⁅R⁆ M

  The projection homomorphism L →ₗ⁅R⁆ M

• IsExtension : LieAlgebra.IsExtension self.incl self.proj

def LieAlgebra.IsExtension.extension {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : Extension R N M

The bundled LieAlgebra.Extension corresponding to LieAlgebra.IsExtension

Equations

• h.extension = { L := L, instLieRing := inst✝⁵, instLieAlgebra := inst✝⁴, incl := i, proj := p, IsExtension := h }

@[simp]

theorem LieAlgebra.IsExtension.extension_L {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.L = L

@[simp]

theorem LieAlgebra.IsExtension.extension_proj {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.proj = p

@[simp]

theorem LieAlgebra.IsExtension.extension_instLieRing {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.instLieRing = inst✝

@[simp]

theorem LieAlgebra.IsExtension.extension_incl {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.incl = i

@[simp]

theorem LieAlgebra.IsExtension.extension_instLieAlgebra {R : Type u_1} {N : Type u_2} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing N] [LieAlgebra R N] [LieRing M] [LieAlgebra R M] {i : N →ₗ⁅R⁆ L} {p : L →ₗ⁅R⁆ M} (h : IsExtension i p) : h.extension.instLieAlgebra = inst✝

theorem LieAlgebra.isExtension_of_surjective {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] (f : L →ₗ⁅R⁆ M) (hf : Function.Surjective ⇑f) : IsExtension f.ker.incl f

A surjective Lie algebra homomorphism yields an extension.

structure LieAlgebra.ofTwoCocycle {R : Type u_5} {L : Type u_6} {M : Type u_7} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : Type (max u_6 u_7)

A one-field structure giving a type synonym for a direct product. We use this to describe an alternative Lie algebra structure on the product, where the bracket is shifted by a 2-cocycle.

• carrier : L × M

  The underlying type.

def LieAlgebra.ofProd {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : L × M ≃ ofTwoCocycle c

An equivalence between the direct product and the corresponding one-field structure. This is used to transfer the additive and scalar-multiple structure on the direct product to the type synonym.

Equations

• LieAlgebra.ofProd c = { toFun := fun (a : L × M) => { carrier := a }, invFun := fun (a : LieAlgebra.ofTwoCocycle c) => a.carrier, left_inv := ⋯, right_inv := ⋯ }

instance LieAlgebra.instAddCommGroupOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : AddCommGroup (ofTwoCocycle c)

Equations

• LieAlgebra.instAddCommGroupOfTwoCocycle c = (LieAlgebra.ofProd c).symm.addCommGroup

instance LieAlgebra.instModuleOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : Module R (ofTwoCocycle c)

Equations

• LieAlgebra.instModuleOfTwoCocycle c = Equiv.module R (LieAlgebra.ofProd c).symm

@[simp]

theorem LieAlgebra.of_zero {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : (ofProd c) 0 = 0

@[simp]

theorem LieAlgebra.of_add {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : L × M) : (ofProd c) (x + y) = (ofProd c) x + (ofProd c) y

@[simp]

theorem LieAlgebra.of_smul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (r : R) (x : L × M) : (ofProd c) (r • x) = r • (ofProd c) x

@[simp]

theorem LieAlgebra.of_symm_zero {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : (ofProd c).symm 0 = 0

@[simp]

theorem LieAlgebra.of_symm_add {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : ofTwoCocycle c) : (ofProd c).symm (x + y) = (ofProd c).symm x + (ofProd c).symm y

@[simp]

theorem LieAlgebra.of_symm_smul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (r : R) (x : ofTwoCocycle c) : (ofProd c).symm (r • x) = r • (ofProd c).symm x

@[simp]

theorem LieAlgebra.of_nsmul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (n : ℕ) (x : L × M) : (ofProd c) (n • x) = n • (ofProd c) x

@[simp]

theorem LieAlgebra.of_symm_nsmul {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (n : ℕ) (x : ofTwoCocycle c) : (ofProd c).symm (n • x) = n • (ofProd c).symm x

instance LieAlgebra.instLieRingOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieRing (ofTwoCocycle c)

Equations

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

theorem LieAlgebra.bracket_ofTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {c : ↥(LieModule.Cohomology.twoCocycle R L M)} (x y : ofTwoCocycle c) : ⁅x, y⁆ = (ofProd c) (⁅((ofProd c).symm x).1, ((ofProd c).symm y).1⁆, (↑↑c ((ofProd c).symm x).1) ((ofProd c).symm y).1 + ⁅((ofProd c).symm x).1, ((ofProd c).symm y).2⁆ - ⁅((ofProd c).symm y).1, ((ofProd c).symm x).2⁆)

instance LieAlgebra.instOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieAlgebra R (ofTwoCocycle c)

Equations

• LieAlgebra.instOfTwoCocycle c = { toModule := LieAlgebra.instModuleOfTwoCocycle c, lie_smul := ⋯ }

def LieAlgebra.Extension.ofTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : Extension R M L

The extension of Lie algebras defined by a 2-cocycle.

Equations

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

instance LieAlgebra.Extension.instLieRingLOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieRing (ofTwoCocycle c).L

Equations

• LieAlgebra.Extension.instLieRingLOfTwoCocycle c = (LieAlgebra.Extension.ofTwoCocycle c).instLieRing

instance LieAlgebra.Extension.instLOfTwoCocycle {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieAlgebra R (ofTwoCocycle c).L

Equations

• LieAlgebra.Extension.instLOfTwoCocycle c = (LieAlgebra.Extension.ofTwoCocycle c).instLieAlgebra

def LieAlgebra.Extension.ofAlg {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) : LieAlgebra.ofTwoCocycle c ≃ₗ⁅R⁆ (ofTwoCocycle c).L

The Lie algebra isomorphism given by the type synonym.

Equations

• LieAlgebra.Extension.ofAlg c = LieEquiv.refl

theorem LieAlgebra.Extension.bracket {R : Type u_1} {L : Type u_3} {M : Type u_4} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing M] [LieAlgebra R M] [IsLieAbelian M] [LieRingModule L M] [LieModule R L M] (c : ↥(LieModule.Cohomology.twoCocycle R L M)) (x y : (ofTwoCocycle c).L) : ⁅x, y⁆ = (ofAlg c) ⁅(ofAlg c).symm x, (ofAlg c).symm y⁆