English
If M₁ and M₂ are nilpotent under L, then their supremum M₁ ⊔ M₂ is nilpotent as a Lie module.
Русский
Если M₁ и M₂ нильпотентны, то их сумма (объединение) тоже нильпотентна под действием L.
LaTeX
$$IsNilpotent L (M₁ ⊔ M₂)$$
Lean4
instance instIsNilpotentSup (M₁ M₂ : LieSubmodule R L M) [IsNilpotent L M₁] [IsNilpotent L M₂] :
IsNilpotent L (M₁ ⊔ M₂ : LieSubmodule R L M) :=
by
obtain ⟨k, hk⟩ := IsNilpotent.nilpotent R L M₁
obtain ⟨l, hl⟩ := IsNilpotent.nilpotent R L M₂
let lcs_eq_bot {m n} (N : LieSubmodule R L M) (le : m ≤ n) (hn : lowerCentralSeries R L N m = ⊥) :
lowerCentralSeries R L N n = ⊥ := by simpa [hn] using antitone_lowerCentralSeries R L N le
have h₁ : lowerCentralSeries R L M₁ (k ⊔ l) = ⊥ := lcs_eq_bot M₁ (Nat.le_max_left k l) hk
have h₂ : lowerCentralSeries R L M₂ (k ⊔ l) = ⊥ := lcs_eq_bot M₂ (Nat.le_max_right k l) hl
refine (isNilpotent_iff R L (M₁ + M₂)).mpr ⟨k ⊔ l, ?_⟩
simp [LieSubmodule.add_eq_sup, (M₁ ⊔ M₂).lowerCentralSeries_eq_lcs_comap, LieSubmodule.lcs_sup,
(M₁.lowerCentralSeries_eq_bot_iff_lcs_eq_bot (k ⊔ l)).1 h₁,
(M₂.lowerCentralSeries_eq_bot_iff_lcs_eq_bot (k ⊔ l)).1 h₂, LieSubmodule.comap_incl_eq_bot]
