English
For a nilpotent Lie algebra L over a domain R and a finite free R-module M with an L-action, if the kernel of the trace form is {0}, then L is Abelian (i.e., [L,L] = {0}).
Русский
Для нильпотентной алгебры Ли L над областью R и конечномерного свободного модуля M с действием L, если ядро формы следа равно нулю, то L абелева (то есть [L,L] = {0}).
LaTeX
$$$\ker (traceForm R L M) = \{0\} \Rightarrow IsLieAbelian L$$$
Lean4
/-- A nilpotent Lie algebra with a representation whose trace form is non-singular is Abelian. -/
theorem isLieAbelian_of_ker_traceForm_eq_bot [Module.Free R M] [Module.Finite R M]
(h : LinearMap.ker (traceForm R L M) = ⊥) : IsLieAbelian L := by
simpa only [← disjoint_lowerCentralSeries_maxTrivSubmodule_iff R L L, disjoint_iff_inf_le,
LieIdeal.toLieSubalgebra_toSubmodule, LieSubmodule.toSubmodule_eq_bot, h] using
lowerCentralSeries_one_inf_center_le_ker_traceForm R L M
