Semi-direct products

This file defines the semi-direct sum of Lie algebras. These are the infinitesimal counterpart of semidirect products of (Lie) groups. Given two Lie algebras K and L over R as well as a Lie algebra homomorphism ψ : L → LieDerivation R K K, the underlying set of the semidirect sum is K × L, however the bracket is twisted by ψ. In this file we show that SemiDirectSum K L ψ is itself a Lie algebra and that it fits into an exact sequence H → (SemiDirectSum K L ψ) → L, i.e. forms an extension of L.

References

• https://en.wikipedia.org/wiki/Lie_algebra_extension#By_semidirect_sum

structure LieAlgebra.SemiDirectSum {R : Type u_1} [CommRing R] (K : Type u_2) [LieRing K] [LieAlgebra R K] (L : Type u_3) [LieRing L] [LieAlgebra R L] : (L →ₗ⁅R⁆ LieDerivation R K K) → Type (max u_2 u_3)

The semi-direct sum of two Lie algebras K and L over R, relative to a Lie algebra homomorphism ψ: L → Liederivation R K K. As a set it just K × L, however the Lie bracket is twisted by ψ.

• left : K

  The element of K

• right : L

  The element of L

theorem LieAlgebra.SemiDirectSum.ext {R : Type u_1} {inst✝ : CommRing R} {K : Type u_2} {inst✝¹ : LieRing K} {inst✝² : LieAlgebra R K} {L : Type u_3} {inst✝³ : LieRing L} {inst✝⁴ : LieAlgebra R L} {x✝ : L →ₗ⁅R⁆ LieDerivation R K K} {x y : K ⋊⁅x✝⁆ L} (left : x.left = y.left) (right : x.right = y.right) : x = y

theorem LieAlgebra.SemiDirectSum.ext_iff {R : Type u_1} {inst✝ : CommRing R} {K : Type u_2} {inst✝¹ : LieRing K} {inst✝² : LieAlgebra R K} {L : Type u_3} {inst✝³ : LieRing L} {inst✝⁴ : LieAlgebra R L} {x✝ : L →ₗ⁅R⁆ LieDerivation R K K} {x y : K ⋊⁅x✝⁆ L} : x = y ↔ x.left = y.left ∧ x.right = y.right

def LieAlgebra.«term_⋊⁅_⁆_» : Lean.TrailingParserDescr

The semi-direct sum of two Lie algebras K and L over R, relative to a Lie algebra homomorphism ψ: L → Liederivation R K K. As a set it just K × L, however the Lie bracket is twisted by ψ.

Equations

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

def LieAlgebra.SemiDirectSum.toProd {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] {ψ : L →ₗ⁅R⁆ LieDerivation R K K} : K ⋊⁅ψ⁆ L ≃ K × L

As raw types, the semidirect product is just a product.

Equations

• LieAlgebra.SemiDirectSum.toProd = { toFun := fun (x : K ⋊⁅ψ⁆ L) => (x.left, x.right), invFun := fun (x : K × L) => { left := x.1, right := x.2 }, left_inv := ⋯, right_inv := ⋯ }

@[implicit_reducible]

instance LieAlgebra.SemiDirectSum.instAddCommGroup {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : AddCommGroup (K ⋊⁅ψ⁆ L)

Equations

• LieAlgebra.SemiDirectSum.instAddCommGroup ψ = LieAlgebra.SemiDirectSum.toProd.addCommGroup

@[implicit_reducible]

instance LieAlgebra.SemiDirectSum.instModule {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : Module R (K ⋊⁅ψ⁆ L)

Equations

• LieAlgebra.SemiDirectSum.instModule ψ = Equiv.module R LieAlgebra.SemiDirectSum.toProd

def LieAlgebra.SemiDirectSum.toProdl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : (K ⋊⁅ψ⁆ L) ≃ₗ[R] K × L

LieAlgebra.SemiDirectSum.toProd as a linear equivalence.

Equations

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

@[implicit_reducible]

instance LieAlgebra.SemiDirectSum.instBracket {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : Bracket (K ⋊⁅ψ⁆ L) (K ⋊⁅ψ⁆ L)

Equations

• LieAlgebra.SemiDirectSum.instBracket ψ = { bracket := fun (x y : K ⋊⁅ψ⁆ L) => { left := ⁅x.left, y.left⁆ + (ψ x.right) y.left - (ψ y.right) x.left, right := ⁅x.right, y.right⁆ } }

@[simp]

theorem LieAlgebra.SemiDirectSum.zero_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : 0 = { left := 0, right := 0 }

@[simp]

theorem LieAlgebra.SemiDirectSum.add_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x y : K ⋊⁅ψ⁆ L) : x + y = { left := x.left + y.left, right := x.right + y.right }

@[simp]

theorem LieAlgebra.SemiDirectSum.sub_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x y : K ⋊⁅ψ⁆ L) : x - y = { left := x.left - y.left, right := x.right - y.right }

@[simp]

theorem LieAlgebra.SemiDirectSum.neg_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L) : -x = { left := -x.left, right := -x.right }

@[simp]

theorem LieAlgebra.SemiDirectSum.smul_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (t : R) (x : K ⋊⁅ψ⁆ L) : t • x = { left := t • x.left, right := t • x.right }

@[simp]

theorem LieAlgebra.SemiDirectSum.lie_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x y : K ⋊⁅ψ⁆ L) : ⁅x, y⁆ = { left := ⁅x.left, y.left⁆ + (ψ x.right) y.left - (ψ y.right) x.left, right := ⁅x.right, y.right⁆ }

@[implicit_reducible]

instance LieAlgebra.SemiDirectSum.instLieRing {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : LieRing (K ⋊⁅ψ⁆ L)

Equations

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

@[implicit_reducible]

instance LieAlgebra.SemiDirectSum.inst {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : LieAlgebra R (K ⋊⁅ψ⁆ L)

Equations

• LieAlgebra.SemiDirectSum.inst ψ = { toModule := LieAlgebra.SemiDirectSum.instModule ψ, lie_smul := ⋯ }

def LieAlgebra.SemiDirectSum.inl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : K →ₗ⁅R⁆ K ⋊⁅ψ⁆ L

The canonical inclusion of K into the semi-direct sum K ⋊⁅ψ⁆ G.

Equations

• LieAlgebra.SemiDirectSum.inl ψ = { toFun := fun (x : K) => { left := x, right := 0 }, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

def LieAlgebra.SemiDirectSum.inr {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : L →ₗ⁅R⁆ K ⋊⁅ψ⁆ L

The canonical inclusion of L into the semi-direct sum K ⋊⁅ψ⁆ G.

Equations

• LieAlgebra.SemiDirectSum.inr ψ = { toFun := fun (x : L) => { left := 0, right := x }, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

@[simp]

theorem LieAlgebra.SemiDirectSum.inl_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K) : (inl ψ) x = { left := x, right := 0 }

@[simp]

theorem LieAlgebra.SemiDirectSum.inr_eq_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : L) : (inr ψ) x = { left := 0, right := x }

@[simp]

theorem LieAlgebra.SemiDirectSum.inl_injective {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : Function.Injective ⇑(inl ψ)

def LieAlgebra.SemiDirectSum.projr {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : K ⋊⁅ψ⁆ L →ₗ⁅R⁆ L

The canonical projection of the semi-direct sum K ⋊⁅ψ⁆ L to G.

Equations

• LieAlgebra.SemiDirectSum.projr ψ = { toFun := fun (x : K ⋊⁅ψ⁆ L) => x.right, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

def LieAlgebra.SemiDirectSum.projl {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : K ⋊⁅ψ⁆ L →ₗ[R] K

The canonical projection of the semi-direct sum K ⋊⁅ψ⁆ L to G. It is not, in general, a Lie algebra homomorphism, just a linear map.

Equations

• LieAlgebra.SemiDirectSum.projl ψ = { toFun := fun (x : K ⋊⁅ψ⁆ L) => x.left, map_add' := ⋯, map_smul' := ⋯ }

@[simp]

theorem LieAlgebra.SemiDirectSum.projr_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L) : (projr ψ) x = x.right

@[simp]

theorem LieAlgebra.SemiDirectSum.projl_mk {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) (x : K ⋊⁅ψ⁆ L) : (projl ψ) x = x.left

theorem LieAlgebra.SemiDirectSum.projr_inl_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : K} : (projr ψ) ((inl ψ) x) = 0

theorem LieAlgebra.SemiDirectSum.projr_inr_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : L} : (projr ψ) ((inr ψ) x) = x

theorem LieAlgebra.SemiDirectSum.projl_inr_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : L} : (projl ψ) ((inr ψ) x) = 0

theorem LieAlgebra.SemiDirectSum.projl_inl_apply {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : K} : (projl ψ) ((inl ψ) x) = x

@[simp]

theorem LieAlgebra.SemiDirectSum.projr_surjective {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : Function.Surjective ⇑(projr ψ)

instance LieAlgebra.SemiDirectSum.instIsExtensionInlProjr {R : Type u_1} [CommRing R] {K : Type u_2} [LieRing K] [LieAlgebra R K] {L : Type u_3} [LieRing L] [LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) : IsExtension (inl ψ) (projr ψ)