Theorems · Theorem · nonassociative algebras

LieModule.exists_nontrivial_weightSpace_of_isSolvable

∀ (k : Type u_1) [inst : Field k] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra k L] (V : Type u_3)
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : LieRingModule L V] [inst_6 : LieModule k L V] [CharZero k]
  [Module.Finite k V] [Nontrivial V] [LieAlgebra.IsSolvable L] [LieModule.IsTriangularizable k L V],
  ∃ χ, Nontrivial ↥(LieModule.weightSpace V ⇑χ)

Lie's theorem: Lie modules of solvable Lie algebras over fields of characteristic 0 have a common eigenvector for the action of all elements of the Lie algebra. See LieModule.exists_nontrivial_weightSpace_of_isNilpotent for the variant that assumes that L is nilpotent and drops the condition that k is of characteristic zero.

Defined in

Mathlib.Algebra.Lie.LieTheorem

Cited by

1 results in Mathlib

Foundations

Depth 129 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FieldLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleCharZeroModule.FiniteNontrivialLieAlgebra.IsSolvableLieModule.IsTriangularizable