Weight spaces of a product of Lie modules

For two modules M and N over a nilpotent Lie algebra, the generalized χ-weight space of M × N is the product of the generalized χ-weight spaces of the factors. Consequently a linear form is a weight of the product exactly when it is a weight of at least one factor, and a product of modules with linear weights again has linear weights.

Main results

• Ado.mem_genWeightSpace_prod_iff: membership in a generalized weight space is componentwise.
• Ado.genWeightSpace_prod_eq_bot_iff: a generalized weight space is trivial exactly when both corresponding spaces in the factors are trivial.
• Ado.instLinearWeightsProd: products of modules with linear weights have linear weights.
• Ado.finrank_genWeightSpace_prod: over a field, generalized weight-space dimensions add.

The first consumer is Ado.formalCharacter_prod, the product-additivity result supporting the "Formal characters" target in Layer 6 of the highest-weight representation-theory roadmap.

@[simp]

theorem Ado.mem_genWeightSpace_prod_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] {χ : L → R} {p : M × N} : p ∈ LieModule.genWeightSpace (M × N) χ ↔ p.1 ∈ LieModule.genWeightSpace M χ ∧ p.2 ∈ LieModule.genWeightSpace N χ

Membership in a generalized weight space of a product is componentwise. A vector lies in the generalized χ-weight space of a product exactly when each component lies in the corresponding generalized χ-weight space of its factor.

@[simp]

theorem Ado.genWeightSpace_prod_eq_bot_iff {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] {χ : L → R} : LieModule.genWeightSpace (M × N) χ = ⊥ ↔ LieModule.genWeightSpace M χ = ⊥ ∧ LieModule.genWeightSpace N χ = ⊥

A linear form is a weight of a product exactly when it is a weight of one factor.

instance Ado.instLinearWeightsProd {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [CommRing R] [LieRing L] [LieAlgebra R L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module R M] [LieRingModule L M] [LieModule R L M] [AddCommGroup N] [Module R N] [LieRingModule L N] [LieModule R L N] [LieModule.LinearWeights R L M] [LieModule.LinearWeights R L N] : LieModule.LinearWeights R L (M × N)

The weights of a product of Lie modules are linear as soon as those of both factors are, since a weight of the product is a weight of one of the factors.

@[simp]

theorem Ado.finrank_genWeightSpace_prod {K : Type u} {L : Type v} {M : Type w} {N : Type w₁} [Field K] [LieRing L] [LieAlgebra K L] [LieRing.IsNilpotent L] [AddCommGroup M] [Module K M] [LieRingModule L M] [LieModule K L M] [FiniteDimensional K M] [AddCommGroup N] [Module K N] [LieRingModule L N] [LieModule K L N] [FiniteDimensional K N] (χ : L → K) : Module.finrank K ↥(LieModule.genWeightSpace (M × N) χ) = Module.finrank K ↥(LieModule.genWeightSpace M χ) + Module.finrank K ↥(LieModule.genWeightSpace N χ)

Generalized weight-space dimensions of a product add.