English
The normalizer of a Lie submodule N is the largest Lie submodule of M consisting of those m ∈ M for which [x,m] ∈ N for all x ∈ L.
Русский
Нормализатор подпространства Ли N — это наибольшее подмодуля M, состоящее из элементов m, для которых [x,m] ∈ N для всех x ∈ L.
LaTeX
$$$\\mathrm{normalizer}(N) = \\{\,m \\in M \\mid \\forall x \\in L,\\ [x,m] \\in N\\,\}$$$
Lean4
/-- The normalizer of a Lie submodule.
See also `LieSubmodule.idealizer`. -/
def normalizer : LieSubmodule R L M where
carrier := {m | ∀ x : L, ⁅x, m⁆ ∈ N}
add_mem' hm₁ hm₂ x := by rw [lie_add]; exact N.add_mem' (hm₁ x) (hm₂ x)
zero_mem' x := by simp
smul_mem' t m hm x := by rw [lie_smul]; exact N.smul_mem' t (hm x)
lie_mem {x m} hm y := by rw [leibniz_lie]; exact N.add_mem' (hm ⁅y, x⁆) (N.lie_mem (hm y))
