maxTrivSubmodule_eq_bot_of_center_eq_bot

English

If the center is trivial, then the maximal triv-submodule of the adjoint action is the zero submodule.

Русский

Если центр тривиален, то максимальное тривиальное подмодульное пространство равно нулю.

LaTeX

$$maxTrivSubmodule = ⊥ when center = ⊥$$

Lean4

theorem maxTrivSubmodule_eq_bot_of_center_eq_bot (h : LieAlgebra.center R L = ⊥) :
    LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥ :=
  by
  refine (LieSubmodule.eq_bot_iff _).mpr fun D hD ↦ ext fun x ↦ ?_
  have : ad R L (D x) = 0 := by
    rw [LieModule.mem_maxTrivSubmodule] at hD
    simp [ad_apply_lieDerivation, hD]
  rw [← LieHom.mem_ker, ad_ker_eq_center, h, LieSubmodule.mem_bot] at this
  simp [this]

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