English
The additive variant of the previous construction yields a Lie algebra structure on GroupLieAlgebra I G (additive case) with Lie bracket defined via invariant vector fields.
Русский
Аддитивный вариант конструкции задаёт Ли-алгебру на GroupLieAlgebra I G (аддитивный случай) с скобкой Ли, заданной через инвариантные векторные поля.
LaTeX
$$$\text{instLieAlgebraAddGroupLieAlgebra} :\ LieAlgebra 𝕜 (AddGroupLieAlgebra I G)$$$
Lean4
/-- The tangent space at the identity of a Lie group is a Lie ring, for the bracket
given by the Lie bracket of invariant vector fields. -/
@[to_additive /-- The tangent space at the identity of an additive Lie group is a Lie ring, for the
bracket given by the Lie bracket of invariant vector fields. -/
]
noncomputable instance : LieRing (GroupLieAlgebra I G)
where
add_lie u v
w := by
simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]
rw [mlieBracket_add_left]
· exact mdifferentiableAt_mulInvariantVectorField _
· exact mdifferentiableAt_mulInvariantVectorField _
lie_add u v
w := by
simp only [GroupLieAlgebra.bracket_def, mulInvariantVectorField_add]
rw [mlieBracket_add_right]
· exact mdifferentiableAt_mulInvariantVectorField _
· exact mdifferentiableAt_mulInvariantVectorField _
lie_self v := by simp [GroupLieAlgebra.bracket_def]
leibniz_lie u v
w := by
simp only [GroupLieAlgebra.bracket_def, mulInvariantVector_mlieBracket]
apply leibniz_identity_mlieBracket_apply <;>
exact
contMDiff_mulInvariantVectorField _
_
/- `to_additive` fails on the next instance, as it tries to additivize `smul` while it shouldn't.
Therefore, we state and prove by hand the additive version. -/
