English
The posFittingCompOf is a Lie submodule containing all iterated ranges of powers of the endomorphism toEnd x, hence prescribing a decreasing system.
Русский
posFittingCompOf является подмодулем Ли, содержащим все диапазоны степеней эндоморфизма toEnd x, образуя убывающую систему.
LaTeX
$$posFittingCompOf R M x := { toSubmodule := ⨅ k, range (toEnd R L M x ^ k), ... }$$
Lean4
@[simp]
theorem posFittingCompOf_le_lowerCentralSeries (x : L) (k : ℕ) : posFittingCompOf R M x ≤ lowerCentralSeries R L M k :=
by
suffices ∀ m l, (toEnd R L M x ^ l) m ∈ lowerCentralSeries R L M l
by
intro m hm
obtain ⟨n, rfl⟩ := (mem_posFittingCompOf R x m).mp hm k
exact this n k
intro m l
induction l with
| zero => simp
| succ l ih =>
simp only [lowerCentralSeries_succ, pow_succ', Module.End.mul_apply]
exact LieSubmodule.lie_mem_lie (LieSubmodule.mem_top x) ih
