English
For every natural number k, the two monotone operators on Lie submodules N ↦ N.lcs(k) and N ↦ N.ucs(k) form a Galois connection, i.e. for all Lie submodules N and P, N.lcs(k) ≤ P iff N ≤ P.ucs(k).
Русский
Для любого натурального k два монотонных отображения на подмодулях Ли-объектов: N ↦ N.lcs(k) и N ↦ N.ucs(k) образуют галуа-соединение, то есть для любых подмодулей N и P выполняется N.lcs(k) ≤ P ⟺ N ≤ P.ucs(k).
LaTeX
$$$\forall N,P \\in \\mathrm{LieSubmodule}_R L M, \\ N.\\mathrm{lcs}(k) \\le P.\\mathrm{ucs}(k) \\iff \\ N \\le P.\\mathrm{ucs}(k).$$$
Lean4
theorem gc_lcs_ucs (k : ℕ) :
GaloisConnection (fun N : LieSubmodule R L M => N.lcs k) fun N : LieSubmodule R L M => N.ucs k := fun _ _ =>
lcs_le_iff k
