English
Comment: Ideals of the bottom LieIdeal are not generally the same as ideals of the ambient Lie algebra restricted to the bottom.
Русский
Замечание: идеалы нижней Ли-идеалы не обязательно совпадают с идеалами всего исходного алгебраического пространства, ограниченными до нижнего.
LaTeX
$$Note: (LieIdeal R L) , (⊥ : LieIdeal R L) have distinct ideal lattices in general$$
Lean4
/-- Note that this is not a special case of `LieSubmodule.subsingleton_of_bot`. Indeed, given
`I : LieIdeal R L`, in general the two lattices `LieIdeal R I` and `LieSubmodule R L I` are
different (though the latter does naturally inject into the former).
In other words, in general, ideals of `I`, regarded as a Lie algebra in its own right, are not the
same as ideals of `L` contained in `I`. -/
instance subsingleton_of_bot : Subsingleton (LieIdeal R (⊥ : LieIdeal R L)) :=
by
apply subsingleton_of_bot_eq_top
subsingleton
