English
The tangent space at the identity of a Lie group, namely GroupLieAlgebra I G, carries a Lie algebra structure over 𝕜, with the bracket defined by the Lie bracket of invariant vector fields.
Русский
Тангенс-пространство в точке идентичности Ли-группы, а именно GroupLieAlgebra I G, имеет структуру Ли-алгебры над 𝕜, скобка определяется через скобку Ли инвариантных векторных полей.
LaTeX
$$$LieRing (GroupLieAlgebra I G)$$$
Lean4
/-- The invariant vector field associated to the value at the identity of the Lie bracket of
two invariant vector fields, is everywhere the Lie bracket of the invariant vector fields. -/
@[to_additive /-- The invariant vector field associated to the value at zero of the Lie
bracket of two invariant vector fields, is everywhere the Lie bracket of the invariant vector
fields. -/
]
theorem mulInvariantVector_mlieBracket (v w : GroupLieAlgebra I G) :
mulInvariantVectorField (mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) 1) =
mlieBracket I (mulInvariantVectorField v) (mulInvariantVectorField w) :=
by
ext g
rw [mulInvariantVectorField_eq_mpullback, mpullback_mlieBracket (n := minSmoothness 𝕜 3),
mpullback_mulInvariantVectorField, mpullback_mulInvariantVectorField]
· exact mdifferentiableAt_mulInvariantVectorField _
· exact mdifferentiableAt_mulInvariantVectorField _
· exact contMDiffAt_mul_left
· exact minSmoothness_monotone (by norm_cast)
