lie_eq_self_of_isAtom_of_nonabelian

English

In the same setting as above, for a Lie ideal I and an atom N in a Lie module, if N is nonabelian in the bracket sense with I and [I,N] ≠ ⊥, then [I,N] = N.

Русский

В той же постановке: если N атомарен и [I,N] не равен нулю, то [I,N] = N, когда [I,N] не абелевация.

LaTeX

$$$\text{If } N \text{ is an atom and } [I,N] \neq \{0\}, \; [I,N] = N$$$

Lean4

theorem lie_eq_self_of_isAtom_of_nonabelian {R L : Type*} [CommRing R] [LieRing L] [LieAlgebra R L] (I : LieIdeal R L)
    (hI : IsAtom I) (h : ¬IsLieAbelian I) : ⁅I, I⁆ = I :=
  lie_eq_self_of_isAtom_of_ne_bot hI <| not_imp_not.mpr (lie_abelian_iff_lie_self_eq_bot I).mpr h

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