English
For a Submodule p of L, the Lie span of p considered as a subset equals p as a submodule if and only if p is the underlying Submodule of some LieSubalgebra of L.
Русский
Для подмодуля p Ли-порождение подмножества p равно p как подмодуль тогда и только тогда, когда p является базисной подмодулой некоторой подпалгебры Ли L.
LaTeX
$$$(\\operatorname{lieSpan}_R L(p) : \\text{Submodule}_R L) = p \\;\\iff\\; \\exists K : \\text{LieSubalgebra}_R L,\\; \\uparrow K = p$$$
Lean4
theorem coe_lieSpan_submodule_eq_iff {p : Submodule R L} :
(lieSpan R L (p : Set L) : Submodule R L) = p ↔ ∃ K : LieSubalgebra R L, ↑K = p :=
by
rw [p.exists_lieSubalgebra_coe_eq_iff]; constructor <;> intro h
· intro x m hm
rw [← h, mem_toSubmodule]
exact lie_mem _ (subset_lieSpan hm)
· rw [← toSubmodule_mk p @h, coe_toSubmodule, toSubmodule_inj, lieSpan_eq]
