Basic results on universal enveloping algebras

This file records general results about universal enveloping algebras that do not depend on additional structures such as filtrations, bialgebras, or antipodes.

Main definitions and results

• Ado.UniversalEnvelopingAlgebra.adjoin_range_ι: a universal enveloping algebra is generated, as an algebra, by its canonical Lie generators.
• Ado.UniversalEnvelopingAlgebra.induction_ι: the induction principle on the canonical Lie generators that the previous statement supplies.
• Ado.UniversalEnvelopingAlgebra.instFiniteType: a universal enveloping algebra is an algebra of finite type over the base ring as soon as the Lie algebra is finite as a module.
• Ado.UniversalEnvelopingAlgebra.representation: the algebra homomorphism U(L) → End M attached to a Lie module M, in particular the adjoint action of U(L) on L at M = L.
• Ado.UniversalEnvelopingAlgebra.representation_lie_of_mem_center: a central element of U(L) acts on a Lie module by a map commuting with the Lie action.
• Ado.UniversalEnvelopingAlgebra.mem_center_iff_forall_lie_ι: centrality in U(L) is detected on the canonical Lie generators alone.
• Ado.UniversalEnvelopingAlgebra.ad_ι_pow_apply_ι: iterating the commutator with a Lie generator reproduces, on the Lie generators, the iterated adjoint action of L.
• Ado.UniversalEnvelopingAlgebra.lie_map_ι: an algebra representation maps the bracket of canonical Lie generators to the bracket of their images.
• Ado.UniversalEnvelopingAlgebra.lie_map_ι_eq_smul: a Lie-bracket eigenvector remains one under an algebra representation.
• Ado.UniversalEnvelopingAlgebra.mul_sub_mul_eq_map_ι_lie: the image of a Lie bracket under an algebra homomorphism is the ring commutator of the images.
• Ado.UniversalEnvelopingAlgebra.commute_of_lie_eq_zero: images of Lie-commuting elements commute.
• Ado.UniversalEnvelopingAlgebra.zsmul_mul_zsmul_eq_add_nsmul_of_zsmul_lie_eq: a scaled Lie-bracket relation gives the corresponding scaled ring-commutator relation.
• Ado.UniversalEnvelopingAlgebra.mul_eq_mul_add_zsmul_of_lie_eq: an integral Lie-bracket structure constant gives the corresponding ring-commutator relation.

theorem Ado.UniversalEnvelopingAlgebra.adjoin_range_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] : Algebra.adjoin R (Set.range ⇑(UniversalEnvelopingAlgebra.ι R)) = ⊤

The enveloping algebra is generated by the canonical Lie generators. This is the U(L) analogue of TensorAlgebra.adjoin_range_ι, obtained by pushing that statement along the surjective quotient map UniversalEnvelopingAlgebra.mkAlgHom R L.

theorem Ado.UniversalEnvelopingAlgebra.induction_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {p : UniversalEnvelopingAlgebra R L → Prop} (ι : ∀ (x : L), p ((UniversalEnvelopingAlgebra.ι R) x)) (algebraMap : ∀ (r : R), p ((algebraMap R (UniversalEnvelopingAlgebra R L)) r)) (add : ∀ (a b : UniversalEnvelopingAlgebra R L), p a → p b → p (a + b)) (mul : ∀ (a b : UniversalEnvelopingAlgebra R L), p a → p b → p (a * b)) (u : UniversalEnvelopingAlgebra R L) : p u

Induction on the canonical Lie generators. A property of elements of U(L) that holds for the canonical Lie generators and the scalars, and is stable under sums and products, holds everywhere, since those generate U(L) as an R-algebra.

instance Ado.UniversalEnvelopingAlgebra.instFiniteType {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] [Module.Finite R L] : Algebra.FiniteType R (UniversalEnvelopingAlgebra R L)

The enveloping algebra of a Lie algebra which is finite as a module is an R-algebra of finite type: a finite spanning set of L generates U(L) as an algebra, the canonical Lie generators of U(L) generating it (Ado.UniversalEnvelopingAlgebra.adjoin_range_ι).

noncomputable def Ado.UniversalEnvelopingAlgebra.representation (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] : UniversalEnvelopingAlgebra R L →ₐ[R] Module.End R M

The representation of a universal enveloping algebra on a Lie module: the algebra homomorphism obtained from LieModule.toEnd by the universal property of U(L). At M = L this is the adjoint action, since LieAlgebra.ad R L is LieModule.toEnd R L L.

Equations

• Ado.UniversalEnvelopingAlgebra.representation R L M = (UniversalEnvelopingAlgebra.lift R) (LieModule.toEnd R L M)

theorem Ado.UniversalEnvelopingAlgebra.representation_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : (representation R L M) ((UniversalEnvelopingAlgebra.ι R) x) = (LieModule.toEnd R L M) x

The representation acts on a canonical Lie generator by the Lie action.

theorem Ado.UniversalEnvelopingAlgebra.representation_ι_ad (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (x : L) : (representation R L L) ((UniversalEnvelopingAlgebra.ι R) x) = (LieAlgebra.ad R L) x

The representation on the Lie algebra itself acts on a canonical generator by the adjoint action.

@[simp]

theorem Ado.UniversalEnvelopingAlgebra.representation_ι' (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) : (representation R L M) ((UniversalEnvelopingAlgebra.mkAlgHom R L) ((TensorAlgebra.ι R) x)) = (LieModule.toEnd R L M) x

The simp-normal form of Ado.UniversalEnvelopingAlgebra.representation_ι, stated for the canonical generators as simp writes them.

theorem Ado.UniversalEnvelopingAlgebra.representation_ι_apply (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] (x : L) (m : M) : ((representation R L M) ((UniversalEnvelopingAlgebra.ι R) x)) m = ⁅x, m⁆

The pointwise form of Ado.UniversalEnvelopingAlgebra.representation_ι: a Lie generator acts by the Lie bracket.

theorem Ado.UniversalEnvelopingAlgebra.representation_lie_of_mem_center (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] (M : Type w) [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] {u : UniversalEnvelopingAlgebra R L} (hu : u ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L)) (x : L) (m : M) : ((representation R L M) u) ⁅x, m⁆ = ⁅x, ((representation R L M) u) m⁆

A central element of U(L) acts on a Lie module by a map commuting with the Lie action. Equivalently, Ado.UniversalEnvelopingAlgebra.representation R L M u is L-equivariant, that is, a homomorphism of Lie modules. Centrality is used only against the canonical Lie generators, which is what the Lie action is read off.

theorem Ado.UniversalEnvelopingAlgebra.lie_map_ι {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : Type w} [Ring B] [Algebra R B] (ρ : UniversalEnvelopingAlgebra R L →ₐ[R] B) (x y : L) : ⁅ρ ((UniversalEnvelopingAlgebra.ι R) x), ρ ((UniversalEnvelopingAlgebra.ι R) y)⁆ = ρ ((UniversalEnvelopingAlgebra.ι R) ⁅x, y⁆)

An algebra representation of the universal enveloping algebra maps the Lie bracket to the commutator in its target algebra.

theorem Ado.UniversalEnvelopingAlgebra.lie_map_ι_eq_smul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : Type w} [Ring B] [Algebra R B] (ρ : UniversalEnvelopingAlgebra R L →ₐ[R] B) {x y : L} {a : R} (hxy : ⁅x, y⁆ = a • y) : ⁅ρ ((UniversalEnvelopingAlgebra.ι R) x), ρ ((UniversalEnvelopingAlgebra.ι R) y)⁆ = a • ρ ((UniversalEnvelopingAlgebra.ι R) y)

A Lie-bracket eigenvector remains one under an algebra representation of the universal enveloping algebra.

theorem Ado.UniversalEnvelopingAlgebra.mul_sub_mul_eq_map_ι_lie {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : Type w} [Ring B] [Algebra R B] (ρ : UniversalEnvelopingAlgebra R L →ₐ[R] B) (a b : L) : ρ ((UniversalEnvelopingAlgebra.ι R) a) * ρ ((UniversalEnvelopingAlgebra.ι R) b) - ρ ((UniversalEnvelopingAlgebra.ι R) b) * ρ ((UniversalEnvelopingAlgebra.ι R) a) = ρ ((UniversalEnvelopingAlgebra.ι R) ⁅a, b⁆)

The image of a Lie bracket under an algebra homomorphism from a universal enveloping algebra is the ring commutator of the images.

theorem Ado.UniversalEnvelopingAlgebra.commute_of_lie_eq_zero {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : Type w} [Ring B] [Algebra R B] (ρ : UniversalEnvelopingAlgebra R L →ₐ[R] B) {a b : L} (hab : ⁅a, b⁆ = 0) : Commute (ρ ((UniversalEnvelopingAlgebra.ι R) a)) (ρ ((UniversalEnvelopingAlgebra.ι R) b))

Images of Lie-commuting elements commute under every algebra homomorphism from the universal enveloping algebra.

theorem Ado.UniversalEnvelopingAlgebra.zsmul_mul_zsmul_eq_add_nsmul_of_zsmul_lie_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : Type w} [Ring B] [Algebra R B] (ρ : UniversalEnvelopingAlgebra R L →ₐ[R] B) {a b b' : L} {p q r : ℤ} {n : ℕ} (hab : (p * q) • ⁅a, b⁆ = (↑n * r) • b') : p • ρ ((UniversalEnvelopingAlgebra.ι R) a) * q • ρ ((UniversalEnvelopingAlgebra.ι R) b) = q • ρ ((UniversalEnvelopingAlgebra.ι R) b) * p • ρ ((UniversalEnvelopingAlgebra.ι R) a) + n • r • ρ ((UniversalEnvelopingAlgebra.ι R) b')

A scaled Lie-bracket relation becomes the corresponding scaled ring-commutator relation under every algebra homomorphism from the universal enveloping algebra.

theorem Ado.UniversalEnvelopingAlgebra.mul_eq_mul_add_zsmul_of_lie_eq {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {B : Type w} [Ring B] [Algebra R B] (ρ : UniversalEnvelopingAlgebra R L →ₐ[R] B) {a b b' : L} {c : ℤ} (hab : ⁅a, b⁆ = c • b') : ρ ((UniversalEnvelopingAlgebra.ι R) a) * ρ ((UniversalEnvelopingAlgebra.ι R) b) = ρ ((UniversalEnvelopingAlgebra.ι R) b) * ρ ((UniversalEnvelopingAlgebra.ι R) a) + c • ρ ((UniversalEnvelopingAlgebra.ι R) b')

A bracket relation with an integral structure constant becomes the corresponding commutator relation under every algebra homomorphism from the universal enveloping algebra.

theorem Ado.UniversalEnvelopingAlgebra.mem_center_iff_forall_lie_ι (R : Type u) (L : Type v) [CommRing R] [LieRing L] [LieAlgebra R L] {u : UniversalEnvelopingAlgebra R L} : u ∈ Subalgebra.center R (UniversalEnvelopingAlgebra R L) ↔ ∀ (x : L), ⁅u, (UniversalEnvelopingAlgebra.ι R) x⁆ = 0

Centrality in U(L) is detected on the canonical Lie generators. An element of U(L) is central exactly when it brackets to zero against every canonical Lie generator, because those generators generate U(L) as an algebra and the elements commuting with a fixed element form a subalgebra.

theorem Ado.UniversalEnvelopingAlgebra.ad_ι_pow_apply_ι {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (x y : L) (n : ℕ) : ((LieAlgebra.ad R (UniversalEnvelopingAlgebra R L)) ((UniversalEnvelopingAlgebra.ι R) x) ^ n) ((UniversalEnvelopingAlgebra.ι R) y) = (UniversalEnvelopingAlgebra.ι R) (((LieAlgebra.ad R L) x ^ n) y)

The iterated commutator with a Lie generator, read on the Lie generators. Bracketing n times with ι x inside U(L) sends ι y to the image of the n-fold adjoint action of x on y; that is, ι intertwines LieAlgebra.ad R L x with the inner derivation of U(L) attached to ι x.