English
For every k, the k-th lower central series term being zero is equivalent to the k-th lcs being zero.
Русский
Для каждого k условие N.lcs k = ⊥ эквивалентно нижней центральной серии равной ⊥.
LaTeX
$$$lcs_k(N) = ⊥ \\iff lowerCentralSeries(R,L,N,k) = ⊥$$$
Lean4
theorem eventually_iInf_lowerCentralSeries_eq [IsArtinian R M] :
∀ᶠ l in Filter.atTop, ⨅ k, lowerCentralSeries R L M k = lowerCentralSeries R L M l :=
by
have h_wf : WellFoundedGT (LieSubmodule R L M)ᵒᵈ := LieSubmodule.wellFoundedLT_of_isArtinian R L M
obtain ⟨n, hn : ∀ m, n ≤ m → lowerCentralSeries R L M n = lowerCentralSeries R L M m⟩ :=
h_wf.monotone_chain_condition ⟨_, antitone_lowerCentralSeries R L M⟩
refine Filter.eventually_atTop.mpr ⟨n, fun l hl ↦ le_antisymm (iInf_le _ _) (le_iInf fun m ↦ ?_)⟩
rcases le_or_gt l m with h | h
· rw [← hn _ hl, ← hn _ (hl.trans h)]
· exact antitone_lowerCentralSeries R L M (le_of_lt h)
