English
If L₂,M₂ are nilpotent and compatible maps exist with surjectivity, then L,M are nilpotent in the appropriate sense.
Русский
Если L₂,M₂ нильпотентны и существуют совместимые отображения с сюръекттивностью, то L,M тоже нильпотентны.
LaTeX
$$Let f,g be maps with hfg compatibility and hg_inj, hf_surj, hg_surj; then LieModule.IsNilpotent L M$$
Lean4
theorem lieModule_lcs_map_eq (k : ℕ) :
(lowerCentralSeries R L M k : Submodule R M).map g = lowerCentralSeries R L₂ M₂ k :=
by
refine le_antisymm (lieModule_lcs_map_le hfg k) ?_
induction k with
| zero => simpa [LinearMap.range_eq_top]
| succ k
ih =>
suffices
{m | ∃ (x : L₂) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, g n⁆ = m} ⊆
g '' {m | ∃ (x : L) (n : _), n ∈ lowerCentralSeries R L M k ∧ ⁅x, n⁆ = m}
by
simp only [← LieSubmodule.mem_toSubmodule] at this
simp_rw [lowerCentralSeries_succ, LieSubmodule.lieIdeal_oper_eq_linear_span', Submodule.map_span,
LieSubmodule.mem_top, true_and, ← LieSubmodule.mem_toSubmodule]
refine Submodule.span_mono (Set.Subset.trans ?_ this)
rintro m₁ ⟨x, n, hn, rfl⟩
obtain ⟨n', hn', rfl⟩ := ih hn
exact ⟨x, n', hn', rfl⟩
rintro m₂ ⟨x, n, hn, rfl⟩
obtain ⟨y, rfl⟩ := hf_surj x
exact ⟨⁅y, n⁆, ⟨y, n, hn, rfl⟩, (hfg y n).symm⟩
