English
Assuming Noetherian and Artinian conditions on M, the infimum of the lower central series equals posFittingComp.
Русский
При условии, что M удовлетворяет условиям Ноetherian и Artinian, инфimum нижних центральных серий равен posFittingComp.
LaTeX
$$$[\text{IsNoetherian } R M] \, [\text{IsArtinian } R M] : \\ \bigwedge_{k} \operatorname{lowerCentralSeries}(R,L,M,k) = \operatorname{posFittingComp}(R,L,M)$$$
Lean4
/-- See also `LieModule.iSup_ucs_eq_genWeightSpace_zero`. -/
@[simp]
theorem iInf_lowerCentralSeries_eq_posFittingComp [IsNoetherian R M] [IsArtinian R M] :
⨅ k, lowerCentralSeries R L M k = posFittingComp R L M :=
by
refine le_antisymm ?_ (posFittingComp_le_iInf_lowerCentralSeries R L M)
apply iInf_lcs_le_of_isNilpotent_quot
rw [LieModule.isNilpotent_iff_forall' (R := R)]
intro x
obtain ⟨k, hk⟩ := Filter.eventually_atTop.mp (toEnd R L M x).eventually_iInf_range_pow_eq
use k
ext ⟨m⟩
set F := posFittingComp R L M
replace hk : (toEnd R L M x ^ k) m ∈ F :=
by
apply posFittingCompOf_le_posFittingComp R L M x
simp_rw [← LieSubmodule.mem_toSubmodule, posFittingCompOf, hk k (le_refl k)]
apply LinearMap.mem_range_self
suffices
(toEnd R L (M ⧸ F) x ^ k) (LieSubmodule.Quotient.mk (N := F) m) =
LieSubmodule.Quotient.mk (N := F) ((toEnd R L M x ^ k) m)
by simpa [Submodule.Quotient.quot_mk_eq_mk, this]
have := LinearMap.congr_fun (Module.End.commute_pow_left_of_commute (LieSubmodule.Quotient.toEnd_comp_mk' F x) k) m
simpa using this
