shiftedGenWeightSpace — Mathlib

English

The shifted weight space is the same as the original weight space when forgetting the L-action; they are equivalent as Lie modules.

Русский

Сдвинутое весовое пространство эквивалентно исходному векторному пространству весов, когда забывается действие L; они эквивалентны как модули Ли.

LaTeX

$$$\\mathrm{shiftedGenWeightSpace}(R,L,M,χ) \\simeq\\mathrm{genWeightSpace}(M,χ).$$$

Lean4

/-- A type synonym for the `χ`-weight space but with the action of `x : L`
on `m : genWeightSpace M χ`, shifted to act as `⁅x, m⁆ - χ x • m`. -/
def shiftedGenWeightSpace :=
  genWeightSpace M χ

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