English
The tangent space at the identity of a Lie group carries a natural Lie algebra structure, with the bracket given by the Lie bracket of invariant vector fields.
Русский
Тangent-пространство в точке единицы группы Ли имеет естественную структуру Lie-алгебры, скобка задаётся скобкой Ли инвариантных векторных полей.
LaTeX
$$$\text{LieAlgebra } 𝕜 (GroupLieAlgebra I G) \text{ exists with bracket } [v,w] =
\text{LieBracket}(v,w) \text{ given by invariant vector fields}$$$
Lean4
/-- The tangent space at the identity of an additive Lie group is a Lie algebra, for the bracket
given by the Lie bracket of invariant vector fields. -/
noncomputable instance instLieAlgebraAddGroupLieAlgebra {G : Type*} [TopologicalSpace G] [ChartedSpace H G] [AddGroup G]
[LieAddGroup I (minSmoothness 𝕜 3) G] : LieAlgebra 𝕜 (AddGroupLieAlgebra I G) where
lie_smul c v
w := by
simp only [AddGroupLieAlgebra.bracket_def, addInvariantVectorField_smul]
rw [mlieBracket_const_smul_right]
exact mdifferentiableAt_addInvariantVectorField _
