isCompl_genWeightSpaceOf_zero_posFittingCompOf

English

Under Noetherian and Artinian hypotheses, genWeightSpace M 0 and posFittingComp R L M form a direct decomposition of M.

Русский

При условиях Noetherian и Artinian генWeightSpace(M,0) и posFittingComp(R,L,M) образуют прямое разложение модуля M.

LaTeX

$$IsCompl (genWeightSpace M 0) (posFittingComp R L M)$$

Lean4

theorem isCompl_genWeightSpaceOf_zero_posFittingCompOf (x : L) :
    IsCompl (genWeightSpaceOf M 0 x) (posFittingCompOf R M x) := by
  simpa only [isCompl_iff, codisjoint_iff, disjoint_iff, ← LieSubmodule.toSubmodule_inj, LieSubmodule.sup_toSubmodule,
    LieSubmodule.inf_toSubmodule, LieSubmodule.top_toSubmodule, LieSubmodule.bot_toSubmodule,
    coe_genWeightSpaceOf_zero] using (toEnd R L M x).isCompl_iSup_ker_pow_iInf_range_pow

Похожие утверждения