English
The family of Lie submodules forms a SupSet, with the supremum of a set S defined by taking the supremum of their underlying submodules and closing under the Lie structure.
Русский
Семейство Ли-подмодулей образует SupSet, причем верхняя грань множества S задаётся взятием верхней грани подмодулей и замыканием по структуре Ли.
LaTeX
$$$\text{SupSet}(S)^{\text{toSubmodule}} = \mathrm{sSup}\{s : \text{Submodule } R M \mid s \in S\}$$$
Lean4
instance : SupSet (LieSubmodule R L M) where
sSup
S :=
{ toSubmodule := sSup ({(p : Submodule R M) | p ∈ S})
lie_mem := by
intro x m (hm : m ∈ sSup ({(p : Submodule R M) | p ∈ S}))
change ⁅x, m⁆ ∈ sSup ({(p : Submodule R M) | p ∈ S})
obtain ⟨s, hs, hsm⟩ := Submodule.mem_sSup_iff_exists_finset.mp hm
clear hm
classical
induction s using Finset.induction_on generalizing m with
| empty =>
replace hsm : m = 0 := by simpa using hsm
simp [hsm]
| insert q t hqt ih =>
rw [Finset.iSup_insert] at hsm
obtain ⟨m', hm', u, hu, rfl⟩ := Submodule.mem_sup.mp hsm
rw [lie_add]
refine add_mem ?_ (ih (Subset.trans (by simp) hs) hu)
obtain ⟨p, hp, rfl⟩ : ∃ p ∈ S, ↑p = q := hs (Finset.mem_insert_self q t)
suffices p ≤ sSup ({(p : Submodule R M) | p ∈ S}) by exact this (p.lie_mem hm')
exact le_sSup ⟨p, hp, rfl⟩ }
