English
The idealizer of a Lie submodule N is the LieIdeal of L consisting of those x ∈ L such that ∀ m ∈ M, [x,m] ∈ N.
Русский
Идеалайзер Ли-подмодуля N — это Ли-идеал L, состоящий из таких x ∈ L, что для всех m ∈ M выполняется [x,m] ∈ N.
LaTeX
$$$ \\mathrm{idealizer}(N) = \\{ x \\in L \\mid \\forall m \\in M, [x,m] \\in N \\}$$$
Lean4
/-- The idealizer of a Lie submodule.
See also `LieSubmodule.normalizer`. -/
def idealizer : LieIdeal R L where
carrier := {x : L | ∀ m : M, ⁅x, m⁆ ∈ N}
add_mem' := fun {x} {y} hx hy m ↦ by rw [add_lie]; exact N.add_mem (hx m) (hy m)
zero_mem' := by simp
smul_mem' := fun t {x} hx m ↦ by rw [smul_lie]; exact N.smul_mem t (hx m)
lie_mem := fun {x} {y} hy m ↦ by rw [lie_lie]; exact sub_mem (N.lie_mem (hy m)) (hy ⁅x, m⁆)
