LeanPool.LowDimSolvClassification.QuotientSolvable

theorem LieIdeal.comap_incl_eq_bot_of_le {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {I J : LieIdeal R L} (h : J ≤ I) : comap I.incl J = ⊥ ↔ J = ⊥

A reformulation of LieIdeal.comap_incl_eq_bot under the additional hypothesis J ≤ I.

def LieAlgebra.Quotient.mk' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : L →ₗ⁅R⁆ L ⧸ I

TODO.

Equations

• LieAlgebra.Quotient.mk' I = { toFun := LieSubmodule.Quotient.mk, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }

theorem LieAlgebra.surjective_mk' {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) : Function.Surjective ⇑(Quotient.mk' I)

theorem LieAlgebra.solvable_of_ideal_and_quot_solvable {R : Type u_1} {L : Type u_2} [CommRing R] [LieRing L] [LieAlgebra R L] {I : LieIdeal R L} (quotsol : IsSolvable (L ⧸ I)) (Isol : IsSolvable ↥I) : IsSolvable L