normalizer_eq_top — Mathlib

English

Let I be a Lie ideal of a Lie algebra L over a commutative ring R. The normalizer of I, when viewed as a Lie subalgebra of L, is the whole algebra; equivalently every element of L normalizes I.

Русский

Пусть I — идеал Ли в ленгой алгебре L над кольцом R. Нормализатор I в L, рассматриваемый как подалгебра, равен всей алгебре; то есть каждый элемент L нормализует I.

LaTeX

$$$$\{ x \in L \mid [x,I]\subseteq I \} = L.$$$$

Lean4

@[simp]
theorem normalizer_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L) :
    (I : LieSubalgebra R L).normalizer = ⊤ := by
  ext x
  simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true] using fun y hy => I.lie_mem hy

Похожие утверждения