The subalgebra of an enveloping algebra generated by a Lie subalgebra

For a Lie subalgebra A of L, this file names the R-subalgebra TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra R A of U(L) generated by the canonical Lie generators of A, identifies it with the image of U(A) under the functorial map U(A) → U(L) of TauCeti/Algebra/Lie/UniversalEnveloping/Functoriality.lean, and proves the factorisation of U(L) that a splitting of a Lie subalgebra into two Lie subalgebras induces.

The factorisation

Let C be a Lie subalgebra of L whose underlying submodule is the sum of the underlying submodules of two Lie subalgebras A and B, so that C = A + B as modules — the sum is not assumed to be direct, and neither summand is assumed to be an ideal. Then

U(A) · U(B) = U(C)

as R-submodules of U(L), where U(A) · U(B) denotes the submodule spanned by the products. The proof is a straightening argument: a generator of B moves to the right across a word in the generators of A at the cost of a bracket, and that bracket is again a sum of an element of A and an element of B because C is closed under the bracket.

No Poincaré--Birkhoff--Witt input is used, and correspondingly the conclusion is a spanning statement about a product of submodules. It is strictly weaker than the assertion that U(C) is free as a left U(A)-module on a basis of U(B), which is the Poincaré--Birkhoff--Witt half and is not proved here.

Main definitions

• TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra: the subalgebra of U(L) generated by the canonical Lie generators of a Lie subalgebra of L.

Main results

• TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_le_iff: the elimination rule, saying that the enveloping subalgebra of A is the smallest subalgebra containing the canonical Lie generators of A.
• TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_eq_range_map: the enveloping subalgebra of A is the image of U(A) in U(L), which is what makes the name accurate, and TauCeti.UniversalEnvelopingAlgebra.mem_envelopingSubalgebra_iff, its membership form.
• envelopingSubalgebra_mul_envelopingSubalgebra_eq_envelopingSubalgebra: the factorisation U(A) · U(B) = U(C) for a Lie subalgebra C with C = A + B as modules, and TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_mul_envelopingSubalgebra_eq_top, its reading at C = L.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §17.2.

The subalgebra generated by a Lie subalgebra

def TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A : LieSubalgebra R L) : Subalgebra R (UniversalEnvelopingAlgebra R L)

The enveloping subalgebra of a Lie subalgebra A of L: the R-subalgebra of U(L) generated by the canonical Lie generators ι R x for x in A.

It is the image of U(A) in U(L), which is TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_eq_range_map, but it is defined here as a subalgebra of U(L) so that statements comparing several of them — the factorisation below first of all — are statements inside the single algebra U(L).

Equations

• TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra R A = Algebra.adjoin R (⇑(UniversalEnvelopingAlgebra.ι R) '' ↑A)

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_eq_adjoin (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A : LieSubalgebra R L) : envelopingSubalgebra R A = Algebra.adjoin R (⇑(UniversalEnvelopingAlgebra.ι R) '' ↑A)

The enveloping subalgebra of A is the subalgebra generated by the canonical Lie generators of A.

theorem TauCeti.UniversalEnvelopingAlgebra.ι_mem_envelopingSubalgebra (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : LieSubalgebra R L} {x : L} (hx : x ∈ A) : (UniversalEnvelopingAlgebra.ι R) x ∈ envelopingSubalgebra R A

The canonical Lie generator of an element of A lies in the enveloping subalgebra of A.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_le_iff (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : LieSubalgebra R L} {S : Subalgebra R (UniversalEnvelopingAlgebra R L)} : envelopingSubalgebra R A ≤ S ↔ ∀ x ∈ A, (UniversalEnvelopingAlgebra.ι R) x ∈ S

The elimination rule: the enveloping subalgebra of A is the smallest subalgebra of U(L) containing the canonical Lie generators of A.

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_mono (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A B : LieSubalgebra R L} (h : A ≤ B) : envelopingSubalgebra R A ≤ envelopingSubalgebra R B

Monotonicity: an inclusion h : A ≤ B of Lie subalgebras of L induces an inclusion of their enveloping subalgebras, the canonical Lie generators of A being among those of B.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_bot (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : envelopingSubalgebra R ⊥ = ⊥

The enveloping subalgebra generated by the zero Lie subalgebra consists only of scalars.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_sup (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A B : LieSubalgebra R L) : envelopingSubalgebra R (A ⊔ B) = envelopingSubalgebra R A ⊔ envelopingSubalgebra R B

The enveloping subalgebra generated by a supremum is the supremum of the enveloping subalgebras.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_top (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] : envelopingSubalgebra R ⊤ = ⊤

The enveloping subalgebra of L itself is all of U(L), the canonical Lie generators generating U(L).

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_eq_range_map (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (A : LieSubalgebra R L) : envelopingSubalgebra R A = (map R A.incl).range

The enveloping subalgebra of A is the image of U(A) in U(L). This identifies the subalgebra named here with the enveloping algebra of A, and is what licenses reading envelopingSubalgebra R A as U(A).

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.mem_envelopingSubalgebra_iff (R : Type u) {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A : LieSubalgebra R L} {u : UniversalEnvelopingAlgebra R L} : u ∈ envelopingSubalgebra R A ↔ ∃ (w : UniversalEnvelopingAlgebra R ↥A), (map R A.incl) w = u

Membership in the enveloping subalgebra of A: an element of U(L) lies in it exactly when it is the image of an element of U(A) under the functorial map. This is the membership form of TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_eq_range_map.

The factorisation induced by a splitting of a Lie subalgebra

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_mul_envelopingSubalgebra_eq_envelopingSubalgebra {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A B C : LieSubalgebra R L} (hC : C.toSubmodule = A.toSubmodule ⊔ B.toSubmodule) : Subalgebra.toSubmodule (envelopingSubalgebra R A) * Subalgebra.toSubmodule (envelopingSubalgebra R B) = Subalgebra.toSubmodule (envelopingSubalgebra R C)

The factorisation U(A) · U(B) = U(C) for Lie subalgebras A, B and C of L whose underlying submodules satisfy C = A + B.

The inclusion ⊇ is the substance: the product U(A) · U(B) absorbs left multiplication by every element of U(C) and contains 1. The converse inclusion holds because U(C) is a subalgebra containing U(A) and U(B).

This is a statement about spanning; it does not say that U(C) is free as a left U(A)-module, which is the Poincaré--Birkhoff--Witt half and needs a basis of L adapted to the splitting.

theorem TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra_mul_envelopingSubalgebra_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] {A B : LieSubalgebra R L} (hAB : A.toSubmodule ⊔ B.toSubmodule = ⊤) : Subalgebra.toSubmodule (envelopingSubalgebra R A) * Subalgebra.toSubmodule (envelopingSubalgebra R B) = ⊤

The factorisation U(A) · U(B) = U(L) for Lie subalgebras A and B of L whose underlying submodules span L.