isNilpotent_ad_of_isNilpotent_ad — Mathlib

English

If ad_R L x is nilpotent for some x in a Lie subalgebra K of L, then ad_R A x is nilpotent for A containing L (transfer of nilpotency from a subalgebra to ambient algebra).

Русский

Если для некоторого x ∈ K ⊆ L действует нильпотентно ад‑оператор в L, то ад‑оператор на A также нильпотентен для этого x.

LaTeX

$$IsNilpotent (ad R L x) → IsNilpotent (ad R A x)$$

Lean4

theorem _root_.LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad {L : Type v} [LieRing L] [LieAlgebra R L]
    (K : LieSubalgebra R L) {x : K} (h : IsNilpotent (LieAlgebra.ad R L ↑x)) : IsNilpotent (LieAlgebra.ad R K x) :=
  by
  obtain ⟨n, hn⟩ := h
  use n
  exact Module.End.submodule_pow_eq_zero_of_pow_eq_zero (K.ad_comp_incl_eq x) hn

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