Ado の定理の主張

structure LieAlgebra.BundledAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] : Type (max (u + 1) u_1)

• mk' :: (
• V : Type u
• instAddCommGroup : AddCommGroup self.V
• instModule : Module K self.V
• instFiniteDimentional : FiniteDimensional K self.V
• instLieRingModule : LieRingModule 𝔤 self.V
• instLieModule : LieModule K 𝔤 self.V
• instIsFaithful : LieModule.IsFaithful K 𝔤 self.V
• instIsNilpotentMaxNilpotentIdeal : LieModule.IsNilpotent (↥(maxNilpotentIdeal K 𝔤)) self.V
• )

noncomputable def LieAlgebra.BundledAdoSpace.mk {K : Type u} {𝔤 : Type u_1} [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] (V : Type u_2) [AddCommGroup V] [Module K V] [FiniteDimensional K V] [LieRingModule 𝔤 V] [LieModule K 𝔤 V] [LieModule.IsFaithful K 𝔤 V] [LieModule.IsNilpotent (↥(maxNilpotentIdeal K 𝔤)) V] : BundledAdoSpace K 𝔤

Equations

• One or more equations did not get rendered due to their size.

class LieAlgebra.IsAdo (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] : Prop

• nonempty_bundledAdoSpace : Nonempty (BundledAdoSpace K 𝔤)

theorem LieAlgebra.IsAdo.intro {K : Type u_1} {𝔤 : Type u_2} [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] (V : Type u_3) [AddCommGroup V] [Module K V] [FiniteDimensional K V] [LieRingModule 𝔤 V] [LieModule K 𝔤 V] [LieModule.IsFaithful K 𝔤 V] [LieModule.IsNilpotent (↥(maxNilpotentIdeal K 𝔤)) V] : IsAdo K 𝔤

def AdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : Type u

Equations

• AdoSpace K 𝔤 = ⋯.some.V

@[instance_reducible]

noncomputable instance instAddCommGroupAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : AddCommGroup (AdoSpace K 𝔤)

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

noncomputable instance instModuleAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : Module K (AdoSpace K 𝔤)

Equations

• instModuleAdoSpace K 𝔤 = { toSMul := instModuleAdoSpace._aux_1✝ K 𝔤, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

instance instFiniteDimensionalAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : FiniteDimensional K (AdoSpace K 𝔤)

@[instance_reducible]

noncomputable instance instLieRingModuleAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : LieRingModule 𝔤 (AdoSpace K 𝔤)

Equations

• instLieRingModuleAdoSpace K 𝔤 = { toBracket := instLieRingModuleAdoSpace._aux_1✝ K 𝔤, add_lie := ⋯, lie_add := ⋯, leibniz_lie := ⋯ }

instance instLieModuleAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : LieModule K 𝔤 (AdoSpace K 𝔤)

instance instIsFaithfulAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : LieModule.IsFaithful K 𝔤 (AdoSpace K 𝔤)

instance instIsNilpotentSubtypeMemLieSubmoduleMaxNilpotentIdealAdoSpace (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : LieModule.IsNilpotent (↥(LieAlgebra.maxNilpotentIdeal K 𝔤)) (AdoSpace K 𝔤)

instance instIsNilpotentAdoSpaceOfIsNilpotent (K : Type u) (𝔤 : Type u_1) [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] [LieRing.IsNilpotent 𝔤] : LieModule.IsNilpotent 𝔤 (AdoSpace K 𝔤)