Killing quotients of supplements

A Lie subalgebra P supplementing an ideal I, so that I + P = L, has quotient P ⧸ (I ∩ P) isomorphic to L ⧸ I by the first isomorphism theorem. Consequently the Killing property of L ⧸ I transfers to this quotient of P.

Main results

• LieIdeal.isKilling_quotient_comap_incl: if I + P = L and L ⧸ I is Killing, so is P ⧸ (I ∩ P).

theorem LieIdeal.isKilling_quotient_comap_incl {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) {P : LieSubalgebra R L} [LieAlgebra.IsKilling R (L ⧸ I)] (hIP : Codisjoint (↑I) P.toSubmodule) : LieAlgebra.IsKilling R (↥P ⧸ comap P.incl I)

A Lie subalgebra P supplementing an ideal I with Killing quotient has Killing quotient by I ∩ P, since P ⧸ (I ∩ P) is isomorphic to L ⧸ I.