English
A submodule p is the underlying submodule of some LieSubalgebra K if and only if p is closed under the Lie bracket: for all x,y ∈ p, [x,y] ∈ p.
Русский
Подмодуль p равен носителю некоторой подалгебры K тогда и только тогда, когда p замкнут относительно бракета: для всех x,y ∈ p, [x,y] ∈ p.
LaTeX
$$$$\forall {R} {L} [\text{CommRing } R] [\text{LieRing } L] [\text{LieAlgebra } R L]\ (p : \text{Submodule } R L),\ (\exists K : \text{LieSubalgebra } R L, \uparrow K = p) \iff \forall x y : L, x \in p \Rightarrow y \in p \Rightarrow [x,y] \in p.$$$$
Lean4
theorem exists_lieSubalgebra_coe_eq_iff (p : Submodule R L) :
(∃ K : LieSubalgebra R L, ↑K = p) ↔ ∀ x y : L, x ∈ p → y ∈ p → ⁅x, y⁆ ∈ p :=
by
constructor
· rintro ⟨K, rfl⟩ _ _
exact K.lie_mem'
· intro h
use { p with lie_mem' := h _ _ }
