English
For a nilpotent action and Noetherian/Artinian base, genWeightSpace with weight 0 is complementary to posFittingComp.
Русский
При нильпотентном действии и базе, удовлетворяющей Noetherian/Artinian, генWeightSpace при весе 0 дополняет posFittingComp.
LaTeX
$$IsCompl (genWeightSpace M 0) (posFittingComp R L M)$$
Lean4
/-- This is the Fitting decomposition of the Lie module `M`. -/
theorem isCompl_genWeightSpace_zero_posFittingComp : IsCompl (genWeightSpace M 0) (posFittingComp R L M) :=
by
let P : LieSubmodule R L M → Prop := fun N ↦ IsCompl (genWeightSpace N 0) (posFittingComp R L N)
suffices P ⊤ by
let e := LieModuleEquiv.ofTop R L M
rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e]
exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mp this
refine (LieSubmodule.wellFoundedLT_of_isArtinian R L M).induction (C := P) _ fun N hN ↦ ?_
refine isCompl_genWeightSpace_zero_posFittingComp_aux R L N fun N' hN' ↦ ?_
suffices IsCompl (genWeightSpace (N'.map N.incl) 0) (posFittingComp R L (N'.map N.incl))
by
let e := LieSubmodule.equivMapOfInjective N' N.injective_incl
rw [← map_genWeightSpace_eq e, ← map_posFittingComp_eq e] at this
exact (LieSubmodule.orderIsoMapComap e).isCompl_iff.mpr this
exact hN _ (LieSubmodule.map_incl_lt_iff_lt_top.mpr hN')
