instLieRingModuleSubtypeMemLieSubmodule

English

There is a canonical Lie-module equivalence between genWeightSpace and shiftedGenWeightSpace, forgetting the L-action.

Русский

Существует каноническое эквивалентное отображение между genWeightSpace и shiftedGenWeightSpace с забыванием действия L.

LaTeX

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

Lean4

instance : LieRingModule L (shiftedGenWeightSpace R L M χ)
    where
  bracket x m := ⁅x, m⁆ - χ x • m
  add_lie x y
    m := by
    nontriviality shiftedGenWeightSpace R L M χ
    simp only [add_lie, LinearWeights.map_add χ (aux R L M χ), add_smul]
    abel
  lie_add x m
    n := by
    nontriviality shiftedGenWeightSpace R L M χ
    simp only [lie_add, smul_add]
    abel
  leibniz_lie x y
    m := by
    nontriviality shiftedGenWeightSpace R L M χ
    simp only [lie_sub, lie_smul, lie_lie, LinearWeights.map_lie χ (aux R L M χ), zero_smul, sub_zero, smul_sub,
      smul_comm (χ x)]
    abel

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