Theorems · Inductive type · nonassociative algebras

IsLieTower

(L₁ : Type u_1) → (L₂ : Type u_2) → (M : Type u_3) → [Bracket L₁ L₂] → [Bracket L₁ M] → [Bracket L₂ M] → [Add M] → Prop

A tower of Lie bracket actions encapsulates the Leibniz rule for Lie bracket actions. More precisely, it does so in a relative setting: Let L₁ and L₂ be two types with Lie bracket actions on a type M endowed with an addition, and additionally assume a Lie bracket action of L₁ on L₂. Then the Leibniz rule asserts for all x : L₁, y : L₂, and m : M that ⁅x, ⁅y, m⁆⁆ = ⁅⁅x, y⁆, m⁆ + ⁅y, ⁅x, m⁆⁆ holds. Common examples include the case where L₁ is a Lie subalgebra of L₂ and the case where L₂ is a Lie ideal of L₁.

Defined in

Mathlib.Algebra.Lie.Basic

Cited by

4 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms

Assumes

BracketBracketBracketAdd