Cofinite kernels of finite-dimensional Lie representations

A Lie algebra map f : L →ₗ⁅K⁆ A into an associative algebra extends along the universal property to an algebra homomorphism UniversalEnvelopingAlgebra.lift K f. The motivating case is a representation ρ : L →ₗ⁅K⁆ Module.End K V, but nothing below uses the endomorphism structure, so the results are stated for an arbitrary associative target. When A is finite-dimensional, the kernel of this extension is cofinite: its quotient embeds linearly in A. As a ring-homomorphism kernel it is automatically a two-sided ideal in Mathlib's ideal API.

The same kernel records nilpotence of the original map. For x : L, the element f x is nilpotent exactly when some power of the canonical generator ι x belongs to the kernel. This is the form needed when a finite-dimensional representation is replaced by a smaller ideal while preserving nilpotence of selected operators.

Main results

• Ado.UniversalEnvelopingAlgebra.finiteDimensional_quotient_ker_lift: its quotient is finite-dimensional.
• Ado.UniversalEnvelopingAlgebra.isNilpotent_iff_exists_pow_ι_mem_ker_lift: nilpotence of the image of an element is equivalent to membership of a power of its enveloping generator in the kernel.

theorem Ado.UniversalEnvelopingAlgebra.finiteDimensional_quotient_ker_lift (R : Type u) (L : Type v) [LieRing L] [Field R] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] [FiniteDimensional R A] (f : L →ₗ⁅R⁆ A) : FiniteDimensional R (UniversalEnvelopingAlgebra R L ⧸ RingHom.ker ((UniversalEnvelopingAlgebra.lift R) f))

The quotient by the kernel of the enveloping-algebra extension of a Lie algebra map into a finite-dimensional associative algebra is finite-dimensional.

theorem Ado.UniversalEnvelopingAlgebra.pow_ι_mem_ker_lift_iff (R : Type u) (L : Type v) [LieRing L] [CommRing R] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) (x : L) (n : ℕ) : (UniversalEnvelopingAlgebra.ι R) x ^ n ∈ RingHom.ker ((UniversalEnvelopingAlgebra.lift R) f) ↔ f x ^ n = 0

A power of the canonical enveloping generator belongs to the kernel of the extended map exactly when the corresponding power of the image vanishes.

theorem Ado.UniversalEnvelopingAlgebra.isNilpotent_iff_exists_pow_ι_mem_ker_lift (R : Type u) (L : Type v) [LieRing L] [CommRing R] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] (f : L →ₗ⁅R⁆ A) (x : L) : IsNilpotent (f x) ↔ ∃ (n : ℕ), (UniversalEnvelopingAlgebra.ι R) x ^ n ∈ RingHom.ker ((UniversalEnvelopingAlgebra.lift R) f)

The image of an element is nilpotent exactly when some power of its canonical enveloping-algebra generator belongs to the kernel of the extended map.