Lie ideals in universal enveloping algebras

A Lie ideal I of L generates a two-sided ideal of the universal enveloping algebra U(L). Although Ideal.span (ι '' I) is initially only a left ideal, the commutator relation ι x * ι y = ι [x, y] + ι y * ι x and the Lie-ideal property show that it is also closed under multiplication on the right.

An intermediate result identifies the image of the ideal generated by I under an arbitrary ring homomorphism. The final results identify powers of the enveloping ideal with the lower-central action filtration and give a uniform power contained in a two-sided ideal J when the canonical images of the elements of I are nilpotent modulo J and U(L) / J is Noetherian over the base ring. For the Ado--Iwasawa construction, I is the nilradical of a solvable Lie algebra and J is the two-sided kernel of a finite-dimensional representation, whose quotient satisfies this Noetherian hypothesis.

These declarations live in the root LieIdeal namespace, extending Mathlib's API and supporting receiver notation on the Lie ideal.

Main definitions and results

• LieIdeal.envelopingIdeal: the ideal of U(L) generated by a Lie ideal I.
• LieIdeal.envelopingIdeal_le_iff: its universal property as a generated ideal.
• LieIdeal.envelopingIdeal_mono, LieIdeal.envelopingIdeal_bot, LieIdeal.envelopingIdeal_sup, LieIdeal.envelopingIdeal_top: monotonicity and the values on ⊥, ⊔, and ⊤.
• LieIdeal.isTwoSided_envelopingIdeal: the generated ideal is two-sided.
• LieIdeal.map_envelopingIdeal: its image under a ring homomorphism is generated by the images of the elements of I.
• LieIdeal.lieSubmoduleOrderIso_lcs_eq_envelopingIdeal_pow_smul_top: powers of the enveloping ideal act through the lower-central filtration for the restricted Lie action.
• LieIdeal.exists_envelopingIdeal_pow_le_of_forall_isNilpotent: nilpotence of the Lie generators modulo an ideal with Noetherian quotient gives a uniform power of the generated ideal contained in it.
• LieIdeal.exists_sup_envelopingIdeal_pow_le_of_forall_isNilpotent: the ideal generated by a Lie ideal is nilpotent modulo a two-sided ideal with Noetherian quotient when its Lie generators are nilpotent there.

References

The ideal construction and its use in the proof of Ado's theorem follow W. Fulton and J. Harris, Representation Theory: A First Course, Appendix E.

The uniform nilpotence argument uses Mathlib's Engel-theorem characterization LieModule.isNilpotent_iff_forall' from Mathlib.Algebra.Lie.Engel.

def LieIdeal.envelopingIdeal {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Ideal (UniversalEnvelopingAlgebra R L)

The ideal generated by a Lie ideal in the universal enveloping algebra. The ideal of U(L) generated by the canonical images of the elements of I; it is two-sided by LieIdeal.isTwoSided_envelopingIdeal.

Equations

• I.envelopingIdeal = Ideal.span (⇑(UniversalEnvelopingAlgebra.ι R) '' ↑I)

@[simp]

theorem LieIdeal.envelopingIdeal_le_iff {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} {J : Ideal (UniversalEnvelopingAlgebra R L)} : I.envelopingIdeal ≤ J ↔ ∀ x ∈ I, (UniversalEnvelopingAlgebra.ι R) x ∈ J

The universal property of the enveloping ideal. It is contained in an ideal J exactly when J contains the canonical image of every element of the Lie ideal.

theorem LieIdeal.ι_mem_envelopingIdeal {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {x : L} (hx : x ∈ I) : (UniversalEnvelopingAlgebra.ι R) x ∈ I.envelopingIdeal

A member of a Lie ideal maps into the ideal it generates in the enveloping algebra.

theorem LieIdeal.envelopingIdeal_mono {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : I ≤ J) : I.envelopingIdeal ≤ J.envelopingIdeal

The enveloping ideal construction is monotone.

@[simp]

theorem LieIdeal.envelopingIdeal_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ⊥.envelopingIdeal = ⊥

The zero Lie ideal generates the zero ideal of the universal enveloping algebra.

@[simp]

theorem LieIdeal.envelopingIdeal_sup {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I J : LieIdeal R L) : (I ⊔ J).envelopingIdeal = I.envelopingIdeal ⊔ J.envelopingIdeal

The enveloping ideal construction preserves binary suprema.

@[simp]

theorem LieIdeal.envelopingIdeal_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : ⊤.envelopingIdeal = Ideal.span (Set.range ⇑(UniversalEnvelopingAlgebra.ι R))

The top Lie ideal generates the ideal spanned by all canonical Lie generators.

instance LieIdeal.isTwoSided_envelopingIdeal {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : I.envelopingIdeal.IsTwoSided

The ideal generated by a Lie ideal is two-sided. I.envelopingIdeal is a two-sided ideal of U(L).

theorem LieIdeal.map_envelopingIdeal {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : Type u_1} [Semiring A] (I : LieIdeal R L) (f : UniversalEnvelopingAlgebra R L →+* A) : Ideal.map f I.envelopingIdeal = Ideal.span ((fun (x : L) => f ((UniversalEnvelopingAlgebra.ι R) x)) '' ↑I)

The image under a ring homomorphism of the enveloping ideal generated by I is the ideal spanned by the images of the elements of I. This is Ideal.map_span with the generating set rewritten to exhibit the composite map.

theorem LieIdeal.lieSubmoduleOrderIso_lie_eq_envelopingIdeal_smul {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_1} [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (N : LieSubmodule R L M) (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) : (Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso hcompat) ⁅I, N⁆ = I.envelopingIdeal • (Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso hcompat) N

The enveloping ideal generated by I acting on a Lie submodule N gives the Lie submodule generated by the action of I on N.

This is the bridge between ideal powers in U(L) and the lower-central filtration of a Lie module. The compatibility hypothesis says that the given U(L)-module structure extends the given L-module structure.

theorem LieIdeal.lieSubmoduleOrderIso_lcs_eq_envelopingIdeal_pow_smul_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_1} [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) (n : ℕ) : (Ado.UniversalEnvelopingAlgebra.lieSubmoduleOrderIso hcompat) (I.lcs M n) = I.envelopingIdeal ^ n • ⊤

Powers of an enveloping ideal are the lower-central action filtration. Under the enveloping-algebra dictionary, the n-fold action of a Lie ideal I on a module is exactly the submodule generated by the action of I.envelopingIdeal ^ n.

Consequently, nilpotence of the restricted I-action is equivalent to the vanishing of some power of the generated ideal on the module.

theorem LieIdeal.isNilpotent_iff_exists_envelopingIdeal_pow_smul_top_eq_bot {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {M : Type u_1} [AddCommGroup M] [Module R M] [Module (UniversalEnvelopingAlgebra R L) M] [IsScalarTower R (UniversalEnvelopingAlgebra R L) M] [LieRingModule L M] [LieModule R L M] (I : LieIdeal R L) (hcompat : ∀ (x : L) (m : M), (UniversalEnvelopingAlgebra.ι R) x • m = ⁅x, m⁆) : LieModule.IsNilpotent (↥I) M ↔ ∃ (n : ℕ), I.envelopingIdeal ^ n • ⊤ = ⊥

A Lie ideal acts nilpotently on a module exactly when a power of its enveloping ideal annihilates the module.

theorem LieIdeal.exists_envelopingIdeal_pow_le_of_forall_isNilpotent {K : Type u} {L' : Type v} [CommRing K] [LieRing L'] [LieAlgebra K L'] (I : LieIdeal K L') (J : Ideal (UniversalEnvelopingAlgebra K L')) [J.IsTwoSided] [IsNoetherian K (UniversalEnvelopingAlgebra K L' ⧸ J)] (hI : ∀ x ∈ I, IsNilpotent ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι K) x))) : ∃ (n : ℕ), I.envelopingIdeal ^ n ≤ J

A uniform power bound for an enveloping ideal modulo a two-sided ideal. If every canonical generator belonging to I is nilpotent modulo J, then a single power of I.envelopingIdeal is contained in J, provided U(L') / J is Noetherian over the base ring. In the Ado--Iwasawa construction, I is the nilradical.

theorem LieIdeal.exists_sup_envelopingIdeal_pow_le_of_forall_isNilpotent {K : Type u} {L' : Type v} [CommRing K] [LieRing L'] [LieAlgebra K L'] (I : LieIdeal K L') (J : Ideal (UniversalEnvelopingAlgebra K L')) [J.IsTwoSided] [IsNoetherian K (UniversalEnvelopingAlgebra K L' ⧸ J)] (hI : ∀ x ∈ I, IsNilpotent ((Ideal.Quotient.mk J) ((UniversalEnvelopingAlgebra.ι K) x))) : ∃ (n : ℕ), (J ⊔ I.envelopingIdeal) ^ n ≤ J

Nilpotence of the ideal generated by nilpotent Lie generators modulo an ideal with Noetherian quotient. Let J be a two-sided ideal of U(L') whose quotient is Noetherian over the base ring. If every canonical generator belonging to I is nilpotent modulo J, then the preimage J ⊔ I.envelopingIdeal of the ideal they generate in the quotient is nilpotent modulo J.

For the Ado--Iwasawa construction, take I to be the nilradical.