English
Let K ≤ K' be Lie subalgebras of a Lie algebra L over a commutative ring R. Then there exists a LieIdeal I inside K' whose underlying LieSubalgebra coincides with the image of K under the inclusion, if and only if for every x in K' and y in K, the bracket [x,y] lies in K.
Русский
Пусть K ⊆ K' являются модулями Ли подалгебрами L над кольцом R. Существует LieIdeal I внутри K', чья лежащая подалгебра равна изображению K через инклюзию, если и только если для всех x ∈ K' и y ∈ K выполняется [x,y] ∈ K.
LaTeX
$$$ (\\exists I : \\mathrm{LieIdeal}(R,K'))\\ ↑I = \\mathrm{ofLe}(h) \\quad \\iff \\quad \\forall x,y:\\,L,\\; x \\in K',\\; y \\in K \\;\\rightarrow \\; [x,y] \\in K $$$
Lean4
theorem exists_nested_lieIdeal_coe_eq_iff {K' : LieSubalgebra R L} (h : K ≤ K') :
(∃ I : LieIdeal R K', ↑I = ofLe h) ↔ ∀ x y : L, x ∈ K' → y ∈ K → ⁅x, y⁆ ∈ K :=
by
simp only [exists_lieIdeal_coe_eq_iff, coe_bracket, mem_ofLe]
constructor
· intro h' x y hx hy; exact h' ⟨x, hx⟩ ⟨y, h hy⟩ hy
· rintro h' ⟨x, hx⟩ ⟨y, hy⟩ hy'; exact h' x y hx hy'
