lieAlgebra_isNilpotent — Mathlib

English

Let L, L' be Lie algebras over a commutative ring R, and f: L → L' be injective. If L' is nilpotent, then L is nilpotent.

Русский

Пусть L, L' — алгебры Ли над коммутативным кольцом R, и f: L → L' — инъективное отображение. Если L' нильпотентна, то и L нильпотентна.

LaTeX

$$$(\text{Injective } f) \land (\text{IsNilpotent } L') \Rightarrow \text{IsNilpotent } L$$$

Lean4

theorem lieAlgebra_isNilpotent [h₁ : IsNilpotent L'] {f : L →ₗ⁅R⁆ L'} (h₂ : Function.Injective f) : IsNilpotent L :=
  by
  rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢
  peel h₁ with k hk
  apply LieIdeal.bot_of_map_eq_bot h₂; rw [eq_bot_iff, ← hk]
  apply LieIdeal.map_lowerCentralSeries_le

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