Ado's theorem

TheoremAdo's theorem#✓fully proved

Every finite-dimensional Lie algebra \(L\) over a field \(K\) of characteristic zero has a faithful finite-dimensional representation: there are a natural number \(n\) and an injective homomorphism of Lie algebras over \(K\) from \(L\) into the Lie algebra of \(K\)-linear endomorphisms of \(K^n\) with the commutator bracket.

Proof: Following Tao's 2011 route, the nilpotent and solvable cases are proved by induction using finite-dimensional quotients of universal enveloping algebras. The general case uses the Levi decomposition and combines the resulting radical representation with the adjoint representation.

public theorem ado
    {K L : Type*} [Field K] [CharZero K] [LieRing L] [LieAlgebra K L]
    [Module.Finite K L] :
    ∃ (n : ℕ) (ρ : L →ₗ⁅K⁆ Module.End K (Fin n → K)),
      Function.Injective ρ

Sources

• I. D. Ado, Bull. Soc. Phys.-Math. Kazan 7 (1935) and 1947 char-zero theorem; Bourbaki, Lie Groups and Lie Algebras; Lean states char-zero finite-dimensional version while modern theorem extends to arbitrary fields.

Uses 1

Proof usesLevi decomposition

TheoremAdo–Iwasawa theorem#●ready to prove

Let \(K\) be a field and let \(L\) be a finite-dimensional Lie algebra over \(K\). Then \(L\) has a faithful finite-dimensional representation: there are a finite-dimensional vector space \(V\) over \(K\) and an injective homomorphism of Lie algebras over \(K\) from \(L\) to the Lie algebra of \(K\)-linear endomorphisms of \(V\) with the commutator bracket.

public theorem_wanted adoIwasawa [FiniteDimensional K L] :
    ∃ (V : Type u) (_ : AddCommGroup V) (_ : Module K V) (_ : FiniteDimensional K V)
      (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ρ

Sources

• 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. Problem adoIwasawa of the lean-eval benchmark.

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.