span_weight_eq_top — Mathlib

English

The span of nonzero weights images equals the top submodule in the dual.

Русский

Образ ненулевых весов образует единичное подполье двойственного пространства.

LaTeX

$$$ span K (\\{ α \\mid α.IsNonZero \\}.image (Weight.toLinear K H L)) = \\top $$$

Lean4

/-- Given a splitting Cartan subalgebra `H` of a finite-dimensional Lie algebra with non-singular
Killing form, the corresponding roots span the dual space of `H`. -/
@[simp]
theorem span_weight_eq_top : span K (range (Weight.toLinear K H L)) = ⊤ :=
  by
  refine eq_top_iff.mpr (le_trans ?_ (LieModule.range_traceForm_le_span_weight K H L))
  rw [← traceForm_flip K H L, ← LinearMap.dualAnnihilator_ker_eq_range_flip, ker_traceForm_eq_bot_of_isCartanSubalgebra,
    Submodule.dualAnnihilator_bot]

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