rootSpaceWeightSpaceProductAux — Mathlib

English

A natural bilinear map composing the root space and weight space actions to land in a higher weight space, built from a lift of an appropriate Lie module action.

Русский

Естественное билинейное отображение, совмещающее действия корневого пространства и весового пространства и выдающее элемент в более высоком весовом пространстве, построенное через подъем соответствующего действия модуля Ли.

LaTeX

$$$\mathrm{rootSpaceWeightSpaceProduct} (χ_1,χ_2,χ_3) (hχ : χ_1+χ_2=χ_3) : \mathrm{rootSpace} H χ_1 ⊗ genWeightSpace M χ_2 → genWeightSpace M χ_3$$$

Lean4

/-- Auxiliary definition for `rootSpaceWeightSpaceProduct`,
which is close to the deterministic timeout limit.
-/
def rootSpaceWeightSpaceProductAux {χ₁ χ₂ χ₃ : H → R} (hχ : χ₁ + χ₂ = χ₃) :
    rootSpace H χ₁ →ₗ[R] genWeightSpace M χ₂ →ₗ[R] genWeightSpace M χ₃
    where
  toFun
    x :=
    { toFun := fun m => ⟨⁅(x : L), (m : M)⁆, hχ ▸ lie_mem_genWeightSpace_of_mem_genWeightSpace x.property m.property⟩
      map_add' := fun m n => by simp only [LieSubmodule.coe_add, lie_add, AddMemClass.mk_add_mk]
      map_smul' := fun t m => by simp }
  map_add' x
    y := by
    ext m
    simp only [LieSubmodule.coe_add, add_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.add_apply,
      AddMemClass.mk_add_mk]
  map_smul' t
    x := by
    simp only [RingHom.id_apply]
    ext m
    simp only [SetLike.val_smul, smul_lie, LinearMap.coe_mk, AddHom.coe_mk, LinearMap.smul_apply, SetLike.mk_smul_mk]

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