Ado–Iwasawa theorem over an arbitrary field

adoIwasawa

Submitter: Kim Morrison.

Notes: Every finite-dimensional Lie algebra L over an arbitrary field K admits a faithful finite-dimensional representation. The representation is required to be given as an injective K-linear Lie homomorphism from L to the commutator Lie algebra of endomorphisms of a finite-dimensional K-vector space. This entry subsumes `adoCharZero`; both remain separate problem-list entries because the characteristic-zero proof is a distinct milestone.

Source: K. Iwasawa, On the representation of Lie algebras, Japanese Journal of Mathematics 19 (1948), 405–426. See also the Tau Ceti Ado–Iwasawa roadmap, https://github.com/TauCetiProject/TauCetiRoadmap/pull/102.

Informal solution: Split on the characteristic of K. In characteristic zero, apply Ado's theorem. In characteristic p, use PBW and central p-polynomials to make the universal enveloping algebra finite over a central commutative subalgebra. A generalized Krull intersection argument produces a finite-dimensional quotient that remains injective on L; its left-regular action is the required faithful representation.

theorem declaration uses `sorry`adoIwasawa [FiniteDimensional K L] :
    ∃ (V : Type u) (_ : AddCommGroup V) (_ : Module K V) (_ : FiniteDimensional K V)
      (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ρ := byK:Type uL:Type uinst✝³:Field Kinst✝²:LieRing Linst✝¹:LieAlgebra K Linst✝:FiniteDimensional K L⊢ ∃ V x x_1, ∃ (_ : FiniteDimensional K V), ∃ ρ, Function.Injective ⇑ρ
  sorryAll goals completed! 🐙

Solved by

• @Vilin97 with Opus-5 on Aug 5, 2026