zeroRootSubalgebra_eq_of_is_cartan

English

If the zero root subalgebra equals H, then H is CartanSubalgebra.

Русский

Если нулевая корневая подсалалгебра равна H, тогда H является картановой подалгеброй.

LaTeX

$$$(\operatorname{zeroRootSubalgebra}(R,L,H) = H) \Rightarrow H.IsCartanSubalgebra$$$

Lean4

@[simp]
theorem zeroRootSubalgebra_eq_of_is_cartan (H : LieSubalgebra R L) [H.IsCartanSubalgebra] [IsNoetherian R L] :
    zeroRootSubalgebra R L H = H :=
  by
  refine le_antisymm ?_ (le_zeroRootSubalgebra R L H)
  suffices rootSpace H 0 ≤ H.toLieSubmodule by exact fun x hx => this hx
  obtain ⟨k, hk⟩ := (rootSpace H 0).isNilpotent_iff_exists_self_le_ucs.mp (by infer_instance)
  exact hk.trans (LieSubmodule.ucs_le_of_normalizer_eq_self (by simp) k)

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