Theorems · Theorem · nonassociative algebras

LieModule.weight_vector_multiplication

∀ {R : Type u_2} {L : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M₁ : Type u_5)
  (M₂ : Type u_6) (M₃ : Type u_7) [inst_3 : AddCommGroup M₁] [inst_4 : Module R M₁] [inst_5 : LieRingModule L M₁]
  [inst_6 : LieModule R L M₁] [inst_7 : AddCommGroup M₂] [inst_8 : Module R M₂] [inst_9 : LieRingModule L M₂]
  [inst_10 : LieModule R L M₂] [inst_11 : AddCommGroup M₃] [inst_12 : Module R M₃] [inst_13 : LieRingModule L M₃]
  [inst_14 : LieModule R L M₃] (g : TensorProduct R M₁ M₂ →ₗ⁅R,L⁆ M₃) (χ₁ χ₂ : R) (x : L),
  (↑g ∘ₗ
        TensorProduct.mapIncl (((LieModule.toEnd R L M₁) x).maxGenEigenspace χ₁)
          (((LieModule.toEnd R L M₂) x).maxGenEigenspace χ₂)).range ≤
    ((LieModule.toEnd R L M₃) x).maxGenEigenspace (χ₁ + χ₂)

See also bourbaki1975b Chapter VII §1.1, Proposition 2 (ii).

Defined in

Mathlib.Algebra.Lie.Weights.Basic

Cited by

1 results in Mathlib

Foundations

Depth 75 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRingLieRingLieAlgebraAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModuleAddCommGroupModuleLieRingModuleLieModule