Ado's theorem in characteristic zero

adoCharZero

Submitter: Kim Morrison.

Notes: Every finite-dimensional Lie algebra L over a characteristic-zero 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. The arbitrary-characteristic `adoIwasawa` entry subsumes this statement; this separate entry records the characteristic-zero proof milestone.

Source: Classical Ado theorem; W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E. See also the Tau Ceti Ado–Iwasawa roadmap, https://github.com/TauCetiProject/TauCetiRoadmap/pull/102.

Informal solution: Construct a faithful nilrepresentation of the center and extend it through an ideal flag in the solvable radical using derivation-stable cofinite ideals of universal enveloping algebras. Extend across a Levi complement, retaining a representation whose kernel meets the center trivially. Finally take its direct sum with the adjoint representation, whose kernel is the center; the direct sum is faithful.

theorem declaration uses `sorry`adoCharZero [CharZero K] [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✝¹:CharZero Kinst✝: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