instLieAlgebraGroupLieAlgebra — Mathlib

English

There is a Lie algebra structure on AddGroupLieAlgebra I G, arising from the bracket of invariant vector fields.

Русский

Существует структура Ли-алгебры на AddGroupLieAlgebra I G, возникающая из скобки инвариантных векторных полей.

LaTeX

$$$\text{LieAlgebra } 𝕜 (AddGroupLieAlgebra I G)$ with bracket defined by invariant vector fields$$

Lean4

/-- The tangent space at the identity of a Lie group is a Lie algebra, for the bracket
given by the Lie bracket of invariant vector fields. -/
noncomputable instance instLieAlgebraGroupLieAlgebra : LieAlgebra 𝕜 (GroupLieAlgebra I G) where
  lie_smul c v
    w := by
    simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_smul]
    rw [mlieBracket_const_smul_right]
    exact mdifferentiableAt_mulInvariantVectorField _

Похожие утверждения