iSupIndep_genWeightSpace — Mathlib

English

The family χ ↦ genWeightSpace M χ is independent in the sense of iSupIndep.

Русский

Семейство χ ↦ genWeightSpace M χ независимо в смысле iSupIndep.

LaTeX

$$iSupIndep (fun χ => genWeightSpace M χ)$$

Lean4

/-- Lie module weight spaces are independent.

See also `LieModule.iSupIndep_genWeightSpace'`. -/
theorem iSupIndep_genWeightSpace [NoZeroSMulDivisors R M] : iSupIndep fun χ : L → R ↦ genWeightSpace M χ :=
  by
  simp only [← LieSubmodule.iSupIndep_toSubmodule, genWeightSpace, LieSubmodule.iInf_toSubmodule]
  exact
    Module.End.independent_iInf_maxGenEigenspace_of_forall_mapsTo (toEnd R L M)
      (fun x y φ z ↦ (genWeightSpaceOf M φ y).lie_mem)

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