English
Let p be a submodule of M. Then p is the underlying submodule of some Lie submodule of M if and only if for every x in L and every m in M, m ∈ p implies [x, m] ∈ p.
Русский
Пусть p ⊆ M является подпространством. Тогда существует Lie-подпространство N ⊆ M с такими же элементами, как p, тогда как для каждого x ∈ L и каждого m ∈ M верно: если m ∈ p, то ⁅x, m⁆ ∈ p. Иными словами, p является подмодулем Ли-структуры L-области M, если и только если она замкнута относительно действия bracket.
LaTeX
$$$ (\exists N\,:\sLieSubmodule\ R\ L\ M,\ (N : Submodule R M) = p) \iff \forall x : L, \forall m : M, m \in p \rightarrow ⁅x, m⁆ \in p $$$
Lean4
theorem exists_lieSubmodule_coe_eq_iff (p : Submodule R M) :
(∃ N : LieSubmodule R L M, ↑N = p) ↔ ∀ (x : L) (m : M), m ∈ p → ⁅x, m⁆ ∈ p :=
by
constructor
· rintro ⟨N, rfl⟩ _ _; exact N.lie_mem
· intro h; use { p with lie_mem := @h }
