shift — Mathlib

English

The shifted weight space carries a Lie module structure over L, with bracket defined by the shifted action.

Русский

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

LaTeX

$$$\\text{shiftedGenWeightSpace} \\;\\text{is a LieModule } L\\;\\big(\\mathrm{shiftedGenWeightSpace}(R,L,M,χ)\\big).$$$

Lean4

/-- Forgetting the action of `L`,
the spaces `genWeightSpace M χ` and `shiftedGenWeightSpace R L M χ` are equivalent. -/
@[simps!]
def shift : genWeightSpace M χ ≃ₗ[R] shiftedGenWeightSpace R L M χ :=
  LinearEquiv.refl R _

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