English
For a Lie module M with Lie submodule N, the underlying sets of the k-th lower central series computed using the base ring R coincide with those computed using the integers Z: (lowerCentralSeries R L M k) as a subset of M equals (lowerCentralSeries ℤ L M k) as a subset of M.
Русский
Для модуля Ли M с подмодулом N множества k-й ниже центральной серии, взятые над кольцом R и над ℤ, совпадают как подмножества M.
LaTeX
$$$\\bigl(lowerCentralSeries R L M k\\bigr) = \\bigl(lowerCentralSeries \\mathbb{Z} L M k\\bigr), \\quad \\text{as subsets of } M$$$
Lean4
theorem coe_lowerCentralSeries_eq_int [LieModule R L M] (k : ℕ) :
(lowerCentralSeries R L M k : Set M) = (lowerCentralSeries ℤ L M k : Set M) :=
by
rw [← LieSubmodule.coe_toSubmodule, ← LieSubmodule.coe_toSubmodule]
induction k with
| zero => rfl
| succ k ih =>
rw [lowerCentralSeries_succ, lowerCentralSeries_succ]
rw [LieSubmodule.lieIdeal_oper_eq_linear_span', LieSubmodule.lieIdeal_oper_eq_linear_span']
rw [Set.ext_iff] at ih
simp only [SetLike.mem_coe, LieSubmodule.mem_toSubmodule] at ih
simp only [LieSubmodule.mem_top, ih, true_and]
apply le_antisymm
· exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
· simp only [← ih]
exact coe_lowerCentralSeries_eq_int_aux _ _ L M k
