冪零 Lie 代数に対する Ado の定理

def Submodule.toLieSubalgebraOfDimOne {K : Type u_1} {𝔫 : Type u_2} [Field K] [LieRing 𝔫] [LieAlgebra K 𝔫] [FiniteDimensional K 𝔫] (𝔥 : Submodule K 𝔫) (h𝔥 : Module.finrank K ↥𝔥 = 1) : LieSubalgebra K 𝔫

Equations

• 𝔥.toLieSubalgebraOfDimOne h𝔥 = { toSubmodule := 𝔥, lie_mem' := ⋯ }

@[simp]

theorem Submodule.toLieSubalgebraOfDimOne_toSubmodule {K : Type u_1} {𝔫 : Type u_2} [Field K] [LieRing 𝔫] [LieAlgebra K 𝔫] [FiniteDimensional K 𝔫] (𝔥 : Submodule K 𝔫) (h𝔥 : Module.finrank K ↥𝔥 = 1) : (𝔥.toLieSubalgebraOfDimOne h𝔥).toSubmodule = 𝔥

theorem LieAlgebra.IsAdo.of_isNilpotent_of_isFaithful_center {K : Type u_1} {𝔫 : Type u_2} [Field K] [LieRing 𝔫] [LieAlgebra K 𝔫] [FiniteDimensional K 𝔫] (V : Type u_3) [AddCommGroup V] [Module K V] [FiniteDimensional K V] [LieRingModule 𝔫 V] [LieModule K 𝔫 V] [LieModule.IsFaithful K (↥(center K 𝔫)) V] [LieModule.IsNilpotent (↥(nilradical K 𝔫)) V] : IsAdo K 𝔫

instance LieAlgebra.IsAdo.of_isNilpotent {K : Type u_1} {𝔫 : Type u_2} [Field K] [LieRing 𝔫] [LieAlgebra K 𝔫] [FiniteDimensional K 𝔫] [LieRing.IsNilpotent 𝔫] : IsAdo K 𝔫