English
For a nilpotent module, the intersection of the first term of the lower central series with the maximal trivial submodule being trivial implies the module is trivial, and conversely.
Русский
Для нильпотентного модуля пересечение первого члена нижней центральной серии с максимальным тривиальным подмодулем тривиально тогда и только тогда, когда модуль тривиален.
LaTeX
$$$\\operatorname{Disjoint}\\bigl(\\lowerCentralSeries R L M 1, \\maxTrivSubmodule R L M\\bigr) \\iff \\operatorname{IsTrivial}_L(M).$$$
Lean4
/-- For a nilpotent Lie module `M` of a Lie algebra `L`, the first term in the lower central series
of `M` contains a non-zero element on which `L` acts trivially unless the entire action is trivial.
Taking `M = L`, this provides a useful characterisation of Abelian-ness for nilpotent Lie
algebras. -/
theorem disjoint_lowerCentralSeries_maxTrivSubmodule_iff [IsNilpotent L M] :
Disjoint (lowerCentralSeries R L M 1) (maxTrivSubmodule R L M) ↔ IsTrivial L M :=
by
refine ⟨fun h ↦ ?_, fun h ↦ by simp⟩
nontriviality M
by_contra contra
have : lowerCentralSeriesLast R L M ≤ lowerCentralSeries R L M 1 ⊓ maxTrivSubmodule R L M :=
le_inf_iff.mpr ⟨lowerCentralSeriesLast_le_of_not_isTrivial R L M contra, lowerCentralSeriesLast_le_max_triv R L M⟩
suffices ¬Nontrivial (lowerCentralSeriesLast R L M) by exact this (nontrivial_lowerCentralSeriesLast R L M)
rw [h.eq_bot, le_bot_iff] at this
exact this ▸ not_nontrivial _
