Finite associative targets for Lie representations

An injective Lie map from L to a finite-dimensional associative algebra A gives a faithful finite-dimensional representation: let L act on A by left multiplication. Conversely, a faithful finite-dimensional representation extends uniquely to an algebra homomorphism from the universal enveloping algebra whose restriction to L remains injective.

Thus existence of a faithful finite-dimensional representation is equivalent to existence of a finite-dimensional associative target of the universal enveloping algebra that separates the canonical copy of L. This interface lets constructions of finite quotients of U(L) produce representations without repeating the left-regular argument.

Main results

• TauCeti.ado_of_finiteAssociativeEmbedding: an associative embedding gives a faithful finite-dimensional representation.
• TauCeti.ado_of_finiteEnvelopingTarget: a finite target of the enveloping algebra gives such a representation.
• TauCeti.faithfulRepresentation_iff_finiteEnvelopingTarget: the finite-target equivalence.

theorem TauCeti.ado_of_finiteAssociativeEmbedding (K : Type u) [Field K] (L : Type u) [LieRing L] [LieAlgebra K L] {A : Type u} [Ring A] [Algebra K A] [FiniteDimensional K A] (f : L →ₗ⁅K⁆ A) (hf : Function.Injective ⇑f) : ∃ (V : Type u) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ

An injective Lie map into a finite-dimensional associative algebra yields a faithful finite-dimensional representation, obtained by letting the Lie algebra act by left multiplication.

theorem TauCeti.ado_of_finiteEnvelopingTarget (K : Type u) [Field K] (L : Type u) [LieRing L] [LieAlgebra K L] {A : Type u} [Ring A] [Algebra K A] [FiniteDimensional K A] (q : UniversalEnvelopingAlgebra K L →ₐ[K] A) (hq : Function.Injective fun (x : L) => q ((UniversalEnvelopingAlgebra.ι K) x)) : ∃ (V : Type u) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ

A finite-dimensional associative target of the universal enveloping algebra which separates the canonical copy of L yields a faithful finite-dimensional representation.

theorem TauCeti.faithfulRepresentation_iff_finiteEnvelopingTarget (K : Type u) [Field K] (L : Type u) [LieRing L] [LieAlgebra K L] : (∃ (V : Type u) (x : AddCommGroup V) (x_1 : Module K V) (_ : FiniteDimensional K V) (ρ : L →ₗ⁅K⁆ Module.End K V), Function.Injective ⇑ρ) ↔ ∃ (A : Type u) (x : Ring A) (x_1 : Algebra K A) (_ : FiniteDimensional K A) (q : UniversalEnvelopingAlgebra K L →ₐ[K] A), Function.Injective fun (x_3 : L) => q ((UniversalEnvelopingAlgebra.ι K) x_3)

A Lie algebra has a faithful finite-dimensional representation if and only if its universal enveloping algebra has a finite-dimensional associative target whose restriction to the canonical copy of the Lie algebra is injective.