English
For a commutative ring R, a Lie algebra L over R, and a subset s ⊆ L, the Lie span of s is abelian if and only if all brackets of elements of s vanish: ⁅x, y⁆ = 0 for all x, y ∈ s.
Русский
Для кольца R и алгебры Ли L над R множество s ⊆ L порождает абелеву подалгебру тогда и только тогда, когда для любых x, y ∈ s выполняется ⁅x, y⁆ = 0.
LaTeX
$$$\\operatorname{IsLieAbelian}(\\operatorname{lieSpan} R L s) \\iff \\forall x\\in s,\\forall y\\in s,\\,[x,y]=0.$$$
Lean4
@[simp]
theorem isLieAbelian_lieSpan_iff {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] {s : Set L} :
IsLieAbelian (lieSpan R L s) ↔ ∀ᵉ (x ∈ s) (y ∈ s), ⁅x, y⁆ = 0 :=
by
refine ⟨fun h x hx y hy ↦ ?_, fun h ↦ ⟨fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ ?_⟩⟩
· let x' : lieSpan R L s := ⟨x, subset_lieSpan hx⟩
let y' : lieSpan R L s := ⟨y, subset_lieSpan hy⟩
suffices ⁅x', y'⁆ = 0 by simpa [x', y', Subtype.ext_iff, -trivial_lie_zero] using this
simp
·
induction hx using lieSpan_induction with
| mem w hw =>
induction hy using lieSpan_induction with
| mem u hu => simpa [Subtype.ext_iff] using h w hw u hu
| zero => simp [Subtype.ext_iff]
| add u v _ _ hu
hv =>
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, lie_add] at hu hv ⊢
simp [hu, hv]
| smul t u _ hu =>
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
simp [Subtype.ext_iff, hu]
| lie u v _ _ hu
hv =>
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
rw [leibniz_lie]
simp [hu, hv]
| zero => simp [Subtype.ext_iff]
| add u v _ _ hu
hv =>
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero, add_lie] at hu hv ⊢
simp [hu, hv]
| smul t u _ hu =>
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu
simp [Subtype.ext_iff, hu]
| lie u v _ _ hu hv =>
simp only [Subtype.ext_iff, coe_bracket, ZeroMemClass.coe_zero] at hu hv ⊢
simp [hu, hv]
