English
For p a Submodule of L, the same equivalence as above holds with the same meaning.
Русский
Для p такой же эквивалентности, как выше, выполняется та же формула.
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_eq_span_of_forall_lie_eq_zero {s : Set L} (hs : ∀ᵉ (x ∈ s) (y ∈ s), ⁅x, y⁆ = 0) :
lieSpan R L s = span R s :=
by
suffices ∀ {x y}, x ∈ span R s → y ∈ span R s → ⁅x, y⁆ ∈ span R s
by
refine le_antisymm ?_ submodule_span_le_lieSpan
change _ ≤ ({ span R s with lie_mem' := this } : LieSubalgebra R L)
rw [lieSpan_le]
exact subset_span
intro x y hx hy
induction hx, hy using span_induction₂ with
| mem_mem x y hx hy => simp [hs x hx y hy]
| zero_left y hy => simp
| zero_right x hx => simp
| add_left x y z _ _ _ hx hy => simp [add_mem hx hy]
| add_right x y z _ _ _ hx hy => simp [add_mem hx hy]
| smul_left r x y _ _ h => simp [smul_mem _ r h]
| smul_right r x y _ _ h => simp [smul_mem _ r h]
