isNilpotent_of_le — Mathlib

English

Under surjectivity and compatibility assumptions, the map equality for lower central series holds for L,M and L₂,M₂.

Русский

При условии сюръективности и совместимости выполняется равенство отображения для нижней центральной серии.

LaTeX

$$theorem lieModule_lcs_map_eq (k : ℕ) : (lowerCentralSeries R L M k : Submodule R M).map g = lowerCentralSeries R L₂ M₂ k$$

Lean4

theorem isNilpotent_of_le (M₁ M₂ : LieSubmodule R L M) (h₁ : M₁ ≤ M₂) [IsNilpotent L M₂] : IsNilpotent L M₁ :=
  by
  let f : L →ₗ⁅R⁆ L := LieHom.id
  let g : M₁ →ₗ[R] M₂ := Submodule.inclusion h₁
  have hfg : ∀ x m, ⁅f x, g m⁆ = g ⁅x, m⁆ := by aesop
  exact (Submodule.inclusion_injective h₁).lieModuleIsNilpotent hfg

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