Enveloping algebras of Lie subalgebras and PBW degree

Over any field an injective Lie homomorphism induces an injective map of universal enveloping algebras, and that map preserves and reflects the PBW filtration. Thus the enveloping algebra of a Lie subalgebra identifies with the subalgebra generated by its canonical Lie generators, with the filtration inherited from the ambient enveloping algebra.

References

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

theorem TauCeti.UniversalEnvelopingAlgebra.mapAssociatedGraded_injective (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) : Function.Injective ⇑(mapAssociatedGraded K f)

An injective Lie map induces an injective map of PBW associated gradeds.

theorem TauCeti.UniversalEnvelopingAlgebra.mapGradedPiece_injective (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) (n : ℕ) : Function.Injective ⇑(mapGradedPiece K f n)

An injective Lie map induces an injective map on every PBW graded piece.

theorem TauCeti.UniversalEnvelopingAlgebra.mem_pbwFiltrationPrevious_of_map_mem (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) {n : ℕ} {x : UniversalEnvelopingAlgebra K L} (hx : x ∈ pbwFiltration K L n) (hfx : (map K f) x ∈ pbwFiltrationPrevious K M n) : x ∈ pbwFiltrationPrevious K L n

For an injective Lie map, a filtered element whose image drops in degree already drops in degree in the source.

@[simp]

theorem UniversalEnvelopingAlgebra.map_mem_pbwFiltration_iff (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) (n : ℕ) (x : UniversalEnvelopingAlgebra K L) : (TauCeti.UniversalEnvelopingAlgebra.map K f) x ∈ TauCeti.UniversalEnvelopingAlgebra.pbwFiltration K M n ↔ x ∈ TauCeti.UniversalEnvelopingAlgebra.pbwFiltration K L n

An injective Lie map reflects membership in each PBW filtration step.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.comap_pbwFiltration (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) (n : ℕ) : Submodule.comap (map K f).toLinearMap (pbwFiltration K M n) = pbwFiltration K L n

The preimage of an ambient PBW filtration step along an injective Lie map is exactly the source filtration step.

theorem TauCeti.UniversalEnvelopingAlgebra.map_pbwFiltration_eq_inf_range_of_injective (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) (n : ℕ) : Submodule.map (map K f).toLinearMap (pbwFiltration K L n) = pbwFiltration K M n ⊓ (map K f).toLinearMap.range

For an injective Lie map, the image of a PBW filtration step is the corresponding ambient step intersected with the range of the enveloping-algebra map.

theorem TauCeti.UniversalEnvelopingAlgebra.map_injective (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) : Function.Injective ⇑(map K f)

An injective Lie homomorphism over a field induces an injective enveloping-algebra map.

theorem TauCeti.UniversalEnvelopingAlgebra.mapFiltration_injective (K : Type u) [Field K] {L : Type v} {M : Type w} [LieRing L] [LieAlgebra K L] [LieRing M] [LieAlgebra K M] (f : L →ₗ⁅K⁆ M) (hf : Function.Injective ⇑f) (n : ℕ) : Function.Injective ⇑(mapFiltration K f n)

An injective Lie map induces an injective map on every PBW filtration step.

noncomputable def LieSubalgebra.universalEnvelopingEquiv {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] (A : LieSubalgebra K L) : UniversalEnvelopingAlgebra K ↥A ≃ₐ[K] ↥(TauCeti.UniversalEnvelopingAlgebra.envelopingSubalgebra K A)

The enveloping algebra of a Lie subalgebra is the subalgebra of the ambient enveloping algebra generated by its canonical Lie generators.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem LieSubalgebra.coe_universalEnvelopingEquiv_apply {K : Type u} [Field K] {L : Type v} [LieRing L] [LieAlgebra K L] (A : LieSubalgebra K L) (x : UniversalEnvelopingAlgebra K ↥A) : ↑(A.universalEnvelopingEquiv x) = (TauCeti.UniversalEnvelopingAlgebra.map K A.incl) x

The enveloping-subalgebra equivalence is the canonical map induced by inclusion.