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
• instIsNilpotentNilradical : LieModule.IsNilpotent (↥(nilradical 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 (↥(nilradical 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 (↥(nilradical 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 = { toSMul := instModuleAdoSpace._aux_1✝, 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 = { toBracket := instLieRingModuleAdoSpace._aux_1✝, 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 instIsNilpotentSubtypeMemLieIdealNilradicalAdoSpace {K : Type u} {𝔤 : Type u_1} [Field K] [LieRing 𝔤] [LieAlgebra K 𝔤] [ia : LieAlgebra.IsAdo K 𝔤] : LieModule.IsNilpotent (↥(LieAlgebra.nilradical 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 𝔤)

theorem LieEquiv.isAdo {K : Type u} {𝔤₁ : Type u_2} {𝔤₂ : Type u_3} [Field K] [LieRing 𝔤₁] [LieAlgebra K 𝔤₁] [LieRing 𝔤₂] [LieAlgebra K 𝔤₂] (e : 𝔤₁ ≃ₗ⁅K⁆ 𝔤₂) [LieAlgebra.IsAdo K 𝔤₁] : LieAlgebra.IsAdo K 𝔤₂

theorem LieEquiv.isAdo_iff {K : Type u} {𝔤₁ : Type u_2} {𝔤₂ : Type u_3} [Field K] [LieRing 𝔤₁] [LieAlgebra K 𝔤₁] [LieRing 𝔤₂] [LieAlgebra K 𝔤₂] (e : 𝔤₁ ≃ₗ⁅K⁆ 𝔤₂) : LieAlgebra.IsAdo K 𝔤₁ ↔ LieAlgebra.IsAdo K 𝔤₂