PBW filtrations for Lie quotients

The quotient map of a Lie algebra by a Lie ideal induces a surjective map between corresponding PBW filtration steps. This file records the quotient specializations of the general surjectivity results in PBW.Functoriality.

Main results

• TauCeti.UniversalEnvelopingAlgebra.map_mkQ_pbwFiltration: specialization to a quotient by a Lie ideal.
• TauCeti.UniversalEnvelopingAlgebra.map_mkQ_pbwFiltrationPrevious: the same for the step immediately preceding a filtration degree.
• TauCeti.UniversalEnvelopingAlgebra.mapFiltration_mkQ_surjective: the induced linear map between quotient filtration steps is surjective.

References

• J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, Chapter V, §17.
• N. Bourbaki, Lie Groups and Lie Algebras, Chapter I, §2.7.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.map_mkQ_pbwFiltration (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : Submodule.map (map R I.mkQ).toLinearMap (pbwFiltration R L k) = pbwFiltration R (L ⧸ I) k

The enveloping-algebra map induced by a Lie quotient maps each PBW filtration step onto the corresponding filtration step of the quotient enveloping algebra.

@[simp]

theorem TauCeti.UniversalEnvelopingAlgebra.map_mkQ_pbwFiltrationPrevious (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : Submodule.map (map R I.mkQ).toLinearMap (pbwFiltrationPrevious R L k) = pbwFiltrationPrevious R (L ⧸ I) k

The enveloping-algebra map induced by a Lie quotient maps the step immediately preceding each PBW filtration degree onto the corresponding preceding step of the quotient enveloping algebra.

theorem TauCeti.UniversalEnvelopingAlgebra.mapFiltration_mkQ_surjective (R : Type u) [CommRing R] {L : Type v} [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) (k : ℕ) : Function.Surjective ⇑(mapFiltration R I.mkQ k)

The linear map on each PBW filtration step induced by a Lie quotient is surjective.