coe_lie_shiftedGenWeightSpace_apply

English

The simplicial equivalence for shifted weight spaces is identity, showing no loss of information under shift.

Русский

Симпликативное отображение для сдвинутых весовых пространств — это идентичность, т.е.shift не теряет информации.

LaTeX

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

Lean4

@[simp]
theorem coe_lie_shiftedGenWeightSpace_apply (x : L) (m : shiftedGenWeightSpace R L M χ) :
    letI : Bracket L (shiftedGenWeightSpace R L M χ) := LieRingModule.toBracket
    ⁅x, m⁆ = ⁅x, (m : M)⁆ - χ x • m :=
  rfl

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