lieAlgebra_isNilpotent — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem lieAlgebra_isNilpotent [h₁ : IsNilpotent L] {f : L →ₗ⁅R⁆ L'} (h₂ : Function.Surjective f) : IsNilpotent L' :=
  by
  rw [LieRing.IsNilpotent, LieModule.isNilpotent_iff R] at h₁ ⊢
  peel h₁ with k hk
  rw [← LieIdeal.lowerCentralSeries_map_eq k h₂, hk]
  simp only [LieIdeal.map_eq_bot_iff, bot_le]

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