English
There exists a join operation on Lie submodules: for N,N' LieSubmodules, N ⊔ N' is the smallest Lie submodule containing both, with underlying Submodule equal to their sum and closed under the Lie action.
Русский
Существует операция объединения (поглощения) подподмодулей: для N,N' — минимальный Ли-подмодуль, содержащий оба, основанный на сумме их подмодулей и замыкающий под скобкой Ли-операции.
LaTeX
$$$(N \sqcup N')^{\mathrm{toSubmodule}} = N^{\mathrm{toSubmodule}} \;\sqcup\; N'^{\mathrm{toSubmodule}}$$$
Lean4
instance : Max (LieSubmodule R L M) where
max N
N' :=
{ toSubmodule := (N : Submodule R M) ⊔ (N' : Submodule R M)
lie_mem := by
rintro x m (hm : m ∈ (N : Submodule R M) ⊔ (N' : Submodule R M))
change ⁅x, m⁆ ∈ (N : Submodule R M) ⊔ (N' : Submodule R M)
rw [Submodule.mem_sup] at hm ⊢
obtain ⟨y, hy, z, hz, rfl⟩ := hm
exact ⟨⁅x, y⁆, N.lie_mem hy, ⁅x, z⁆, N'.lie_mem hz, (lie_add _ _ _).symm⟩ }
