lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left

English

Under nilpotent H and Cartan hypotheses, the trace of the endomorphism toEnd restricted to genWeightSpaceChain associated with coroots is zero.

Русский

При нильпотентности H и предположениях Картанова типа след эндоморфизма toEnd, ограниченного на genWeightSpaceChain, связанного с коротом, равен нулю.

LaTeX

$$$\operatorname{trace}R\_\_ (toEnd(R,H,\text{genWeightSpaceChain}(M, α, χ, p, q))) = 0$$$

Lean4

theorem lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_left [LieRing.IsNilpotent H]
    (hp : genWeightSpace M (p • α + χ) = ⊥) {x : L} (hx : x ∈ rootSpace H (-α)) {y : M}
    (hy : y ∈ genWeightSpaceChain M α χ p q) : ⁅x, y⁆ ∈ genWeightSpaceChain M α χ p q :=
  by
  replace hp : genWeightSpace M ((-p) • (-α) + χ) = ⊥ := by rwa [smul_neg, neg_smul, neg_neg]
  rw [← genWeightSpaceChain_neg] at hy ⊢
  exact lie_mem_genWeightSpaceChain_of_genWeightSpace_eq_bot_right M (-α) χ (-q) (-p) hp hx hy

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