English
In characteristic zero, the exponential of a nilpotent derivation is a Lie algebra automorphism; many properties reduce to equalities of linear maps.
Русский
В характеристике ноль экспонента для нильпотентной деривации образует автоморфизм Ли-алгебры; многие свойства сводятся к равенствам линейных отображений.
LaTeX
$$exp D h = IsNilpotent.exp D.toLinearMap$$
Lean4
/-- In characteristic zero, the exponential of a nilpotent derivation is a Lie algebra
automorphism. -/
noncomputable def exp (h : IsNilpotent D.toLinearMap) : L ≃ₗ⁅R⁆ L :=
{ toLinearMap := IsNilpotent.exp D.toLinearMap
map_lie' := by
let _i := LieRing.toNonUnitalNonAssocRing L
have : SMulCommClass R L L := LieAlgebra.smulCommClass R L
have : IsScalarTower R L L := LieAlgebra.isScalarTower R L
exact Module.End.exp_mul_of_derivation R L D.toLinearMap D.apply_lie_eq_add h
invFun x := IsNilpotent.exp (-D.toLinearMap) x
left_inv
x := by
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ← LinearMap.comp_apply, ← Module.End.mul_eq_comp,
h.exp_neg_mul_exp_self, Module.End.one_apply]
right_inv
x := by
simp only [AddHom.toFun_eq_coe, LinearMap.coe_toAddHom, ← LinearMap.comp_apply, ← Module.End.mul_eq_comp,
h.exp_mul_exp_neg_self, Module.End.one_apply] }
