Ado's theorem in characteristic zero

Every finite-dimensional Lie algebra L over a field of characteristic zero has a faithful finite-dimensional representation, and one can be chosen in which every element of the nilradical N acts nilpotently. Hochschild's strengthening follows: the same representation sends every ad-nilpotent element of L to a nilpotent endomorphism.

The argument

Following Fulton–Harris, a representation that is faithful on the centre Z of L is grown along a chain of Lie subalgebras

Z = S₀ ⊂ S₁ ⊂ ⋯ ⊂ N ⊂ ⋯ ⊂ R ⊂ L,

where R is the solvable radical. Each step S ⊂ S' exhibits S' as a split extension of S by a complementary subalgebra H whose adjoint action on S takes values in N, and TauCeti.exists_semiDirectSum_rep_of_forall_mem extends the representation across it, without losing any direction of S that was detected and keeping the elements of N nilpotent.

• From Z to N the steps have codimension one. A proper subspace of the nilpotent ideal N is normalized by a further element of N (LieIdeal.exists_mem_notMem_lie_mem_of_lt), and every element of N is ad-nilpotent, so the extended representation stays nilpotent on the whole of the larger algebra.
• From N to R the steps again have codimension one: ⁅L, R⁆ ≤ N (TauCeti.LieAlgebra.lie_radical_le_nilradical) makes every subspace between N and R an ideal of L.
• From R to L the complement is a Levi subalgebra (TauCeti.exists_leviComplement), whose adjoint action on R again lands in N.

The resulting representation ρ₀ of L is faithful on Z, and the adjoint representation has kernel exactly Z, so ρ₀ ⊕ ad is faithful.

Nilpotence on the nilradical upgrades to nilpotence on every ad-nilpotent element by Hochschild's argument (LieSubalgebra.isNilpotent_apply_of_isNilpotent_ad_of_isCompl_radical), which needs nothing of the representation beyond its nilpotence on N and uses a Levi complement only in its proof.

Main results

• TauCeti.exists_faithful_nilrepresentation_charZero: a faithful finite-dimensional representation in which every element of the nilradical acts nilpotently.
• TauCeti.exists_faithful_preserving_ad_nilpotence_charZero: Hochschild's strengthening in characteristic zero, a faithful finite-dimensional representation in which every ad-nilpotent element acts nilpotently.
• TauCeti.adoCharZero: Ado's theorem in characteristic zero.

References

• W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E, §E.2.
• S. Asgarli, Ado's Theorem.
• N. Jacobson, Lie Algebras, Interscience (1962), Chapter VI.
• G. Hochschild, An Addition to Ado's Theorem, Proc. Amer. Math. Soc. 17 (1966), 531–533.

theorem TauCeti.exists_faithful_nilrepresentation_charZero (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] : ∃ (V : Type (max u v)) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ ∧ ∀ x_3 ∈ LieAlgebra.nilradical K L, IsNilpotent (ρ x_3)

Ado's theorem in characteristic zero, with nilpotence on the nilradical. A finite-dimensional Lie algebra over a field of characteristic zero has a faithful finite-dimensional representation in which every element of the nilradical acts nilpotently.

theorem TauCeti.exists_faithful_preserving_ad_nilpotence_charZero (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] : ∃ (V : Type (max u v)) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ ∧ ∀ (x_3 : L), IsNilpotent ((LieAlgebra.ad K L) x_3) → IsNilpotent (ρ x_3)

Hochschild's strengthening of Ado's theorem in characteristic zero. A finite-dimensional Lie algebra over a field of characteristic zero has a faithful finite-dimensional representation that preserves nilpotence of the adjoint action: every ad-nilpotent element acts nilpotently.

For semisimple L the nilradical is zero, so the nilpotence clause of TauCeti.exists_faithful_nilrepresentation_charZero is empty there, while this one still constrains every ad-nilpotent element.

theorem TauCeti.adoCharZero (K : Type u) (L : Type v) [Field K] [LieRing L] [LieAlgebra K L] [FiniteDimensional K L] [CharZero K] : ∃ (V : Type (max u v)) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ

Ado's theorem in characteristic zero. Every finite-dimensional Lie algebra over a field of characteristic zero admits a faithful finite-dimensional representation.