Theorems · Inductive type · nonassociative algebras

LieAlgebra.Extension

(R : Type u_1) →
  (N : Type u_2) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [LieAlgebra R N] → [inst_3 : 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.

Defined in

Mathlib.Algebra.Lie.Extension

Cited by

20 results in Mathlib

Foundations

Depth 2 from the axioms · uses no axioms

Assumes

CommRingLieRingLieAlgebraLieRingLieAlgebra