Theorems · Inductive type · nonassociative algebras

LieAlgebra.SemiDirectSum

{R : Type u_1} →
  [inst : CommRing R] →
    (K : Type u_2) →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          (L : Type u_3) →
            [inst_3 : LieRing L] → [inst_4 : 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 is just K × L, however the Lie bracket is twisted by ψ.

Defined in

Mathlib.Algebra.Lie.SemiDirect

Cited by

26 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebra