instSubtypeMemLieSubmodule — Mathlib

English

The shifted action on the weight space respects the Lie bracket: [x, m] in shifted equals [x, m] in M minus χ(x) m.

Русский

Сдвиннутое действие на весовом пространство удовлетворяет тождеству: \$ [x,m]_{shifted} = [x,m] - χ(x) m.\$

LaTeX

$$$\\text{coe\\_lie\\_shiftedGenWeightSpace\_apply}(x,m): [x,m] = [x,m]-χ(x)\\,m.$$$

Lean4

instance : LieModule R L (shiftedGenWeightSpace R L M χ)
    where
  smul_lie t x
    m := by
    nontriviality shiftedGenWeightSpace R L M χ
    apply Subtype.ext
    rw [coe_lie_shiftedGenWeightSpace_apply]
    simp only [smul_lie, LinearWeights.map_smul χ (aux R L M χ), smul_assoc t, SetLike.val_smul]
    rw [← smul_sub]
    congr
  lie_smul t x
    m := by
    nontriviality shiftedGenWeightSpace R L M χ
    apply Subtype.ext
    rw [coe_lie_shiftedGenWeightSpace_apply]
    simp only [SetLike.val_smul, lie_smul]
    rw [smul_comm (χ x), ← smul_sub]
    congr

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