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.

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.

TODO

• IsCentral - central extensions
• Equiv - equivalence of extensions
• ofTwoCocycle - construction of extensions from 2-cocycles

References

• 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

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_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✝

@[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_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_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

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.