English
LieSpan establishes a Galois insertion with the inclusion from LieSubmodule to Set, i.e., lieSpan is the left adjoint to the inclusion.
Русский
LieSpan образует GI (Галоc-инсерцию) с включением LieSubmodule в множество; lieSpan является левым соседом включения.
LaTeX
$$lieSpan_{R,L} \\dashv \\iota: Set M \\to \\text{LieSubmodule}(R,L,M)$$
Lean4
/-- `lieSpan` forms a Galois insertion with the coercion from `LieSubmodule` to `Set`. -/
protected def gi : GaloisInsertion (lieSpan R L : Set M → LieSubmodule R L M) (↑)
where
choice s _ := lieSpan R L s
gc _ _ := lieSpan_le
le_l_u _ := subset_lieSpan
choice_eq _ _ := rfl
