English
The image of the k-th lower central series under a Lie module homomorphism maps into the k-th lower central series of the target module.
Русский
Образ k-й нижней центральной серии под гомоморфизмом отображает в соответствующую серию цели.
LaTeX
$$(lowerCentralSeries R L M k : Submodule R M).map g ≤ lowerCentralSeries R L₂ M₂ k$$
Lean4
theorem lieModule_lcs_map_le (k : ℕ) :
(lowerCentralSeries R L M k : Submodule R M).map g ≤ lowerCentralSeries R L₂ M₂ k := by
induction k with
| zero => simp [Submodule.map_top]
| succ k
ih =>
rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span, Submodule.span_le]
rintro m₂ ⟨m, ⟨x, n, m_n, ⟨h₁, h₂⟩⟩, rfl⟩
simp only [lowerCentralSeries_succ, SetLike.mem_coe, LieSubmodule.mem_toSubmodule]
have : ∃ y : L₂, ∃ n : lowerCentralSeries R L₂ M₂ k, ⁅y, n⁆ = g m :=
by
use f x, ⟨g m_n, ih (Submodule.mem_map_of_mem h₁)⟩
simp [hfg x m_n, h₂]
obtain ⟨y, n, hn⟩ := this
rw [← hn]
apply LieSubmodule.lie_mem_lie
· simp
· exact SetLike.coe_mem n
