Cofinite kernels of Lie algebra maps into finite associative algebras

A Lie algebra map f : L →ₗ⁅R⁆ A into an associative algebra extends along the universal property to an algebra homomorphism UniversalEnvelopingAlgebra.lift R f. The motivating case is a representation ρ : L →ₗ⁅K⁆ Module.End K V over a field, but nothing below uses the endomorphism structure, so the results are stated for an arbitrary associative target. When A is a Noetherian R-module (for instance, finite-dimensional over a field), the kernel of this extension is cofinite: its quotient embeds linearly in A, so it is a finite R-module. 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 ι R 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

• TauCeti.UniversalEnvelopingAlgebra.finite_quotient_ker_lift: the quotient of the enveloping algebra by the kernel of lift R f is a finite R-module when A is a Noetherian R-module.
• TauCeti.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 TauCeti.UniversalEnvelopingAlgebra.finite_quotient_ker_lift (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type w} [Ring A] [Algebra R A] [IsNoetherian R A] (f : L →ₗ⁅R⁆ A) : Module.Finite 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 an associative algebra that is Noetherian as an R-module is a finite R-module.

theorem TauCeti.UniversalEnvelopingAlgebra.pow_ι_mem_ker_lift_iff (R : Type u) {L : Type v} [CommRing R] [LieRing L] [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 TauCeti.UniversalEnvelopingAlgebra.isNilpotent_iff_exists_pow_ι_mem_ker_lift (R : Type u) {L : Type v} [CommRing R] [LieRing L] [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.