Weight spaces of a tensor product of Lie modules #
Let L be a nilpotent Lie algebra acting on two modules M and N. Then L acts on M ⊗ N, and
this file computes the generalized weight spaces of that action: the χ-weight space of M ⊗ N is
spanned by the pure tensors m ⊗ₜ n with m of weight μ, n of weight ν and μ + ν = χ.
Two facts meet. Mathlib's LieModule.weight_vector_multiplication already says that a pure tensor
of a generalized eigenvector of eigenvalue φ and one of eigenvalue ψ is a generalized
eigenvector of eigenvalue φ + ψ, so the inclusion Mμ ⊗ Nν ≤ (M ⊗ N)_{μ+ν} needs no hypothesis
beyond nilpotency of L, and the tensor product of two triangularizable modules is triangularizable
over any commutative ring. The reverse inclusion is not a computation but a counting argument: over
a field, in finite dimensions and with M and N triangularizable, the pure tensors of weight
vectors already span M ⊗ N, so the coarse family indexed by χ refines the independent family of
weight spaces of M ⊗ N and must agree with it termwise
(iSupIndep.le_iff_eq_of_iSup_eq_top).
Main results #
TauCeti.tmul_mem_maxGenEigenspace_add: generalized eigenvalues add on pure tensors, the elementwise form ofLieModule.weight_vector_multiplication.TauCeti.isTriangularizable_tensorProduct: a tensor product of triangularizable modules is triangularizable, over any commutative ring and with no finiteness assumption.TauCeti.tmul_mem_genWeightSpace_add: weights add on pure tensors. Ifmhas weightμandnhas weightν, thenm ⊗ₜ nhas weightμ + ν, andTauCeti.map₂_mk_genWeightSpace_leis the submodule form.TauCeti.iSup_map₂_mk_genWeightSpace_eq_top: the pure tensors of weight vectors spanM ⊗ N.TauCeti.genWeightSpace_tensorProduct_eq_iSup: the weight-space decomposition of a tensor product. Theχ-weight space ofM ⊗ Nis the supremum, over the pairs(μ, ν)withμ + ν = χ, of the submodules spanned byMμ ⊗ Nν.TauCeti.genWeightSpace_tensorProduct_ne_botandTauCeti.exists_weight_add_eq: the weights ofM ⊗ Nare exactly the sums of a weight ofMand a weight ofN.TauCeti.instLinearWeightsTensorProduct: tensor products inherit linear weights from their finite-dimensional triangularizable factors.
Implementation notes #
The submodule spanned by the pure tensors m ⊗ₜ n with m ∈ Mμ and n ∈ Nν is written as
Mathlib's Submodule.map₂ (TensorProduct.mk R M N), the submodule image of a bilinear map, rather
than through a new definition: the supremum and monotonicity API the proofs need
(Submodule.map₂_iSup_left, Submodule.map₂_le) is already stated for it.
The weight spaces are Mathlib's generalized weight spaces LieModule.genWeightSpace, so the
statements below are read in Submodule R (M ⊗[R] N) rather than in the lattice of Lie submodules;
LieSubmodule.toSubmodule mediates. Nothing here needs the weight spaces to be honest eigenspaces.
The multiplicity count dim (M ⊗ N)_χ = ∑_{μ + ν = χ} dim Mμ · dim Nν, which is what a formal
character consumes, needs in addition that the family indexed by pairs (μ, ν) is independent,
and is not proved here.
References #
- N. Bourbaki, Groupes et algèbres de Lie, Chapitre VII, §1.1, Proposition 2.
- J. E. Humphreys, Introduction to Lie Algebras and Representation Theory, GTM 9, §20.
- Highest-weight roadmap,
Layer 6, "The representation ring and the character algebra", which asks for the tensor product of
Lie modules as the preliminary to a formal character multiplicative on tensor products
(
formalCharacter_tensor); this file supplies its weight-theoretic half.
Generalized eigenvalues add on pure tensors #
Generalized eigenvalues add on pure tensors. A pure tensor of a generalized eigenvector of
x of eigenvalue φ in M and one of eigenvalue ψ in N is a generalized eigenvector of x of
eigenvalue φ + ψ in M ⊗ N.
This is the elementwise form of Mathlib's LieModule.weight_vector_multiplication, applied to the
identity map of M ⊗ N. Neither nilpotency of L nor any finiteness is involved.
A tensor product of triangularizable modules is triangularizable. If every element of L
acts on M and on N with its generalized eigenspaces spanning, then the same holds on M ⊗ N:
the pure tensors of generalized eigenvectors span M ⊗ N, and they are generalized eigenvectors by
TauCeti.tmul_mem_maxGenEigenspace_add.
Weights add on pure tensors #
Weights add on pure tensors. A pure tensor of a vector of generalized weight χ in M and
a vector of generalized weight ψ in N has generalized weight χ + ψ in M ⊗ N.
This is TauCeti.tmul_mem_maxGenEigenspace_add, applied one element x : L at a time. No
finiteness or triangularizability is involved.
The submodule of M ⊗ N spanned by the pure tensors of a χ-weight vector of M and a
ψ-weight vector of N lies in the (χ + ψ)-weight space of M ⊗ N. This is the submodule form
of TauCeti.tmul_mem_genWeightSpace_add.
The weights of a tensor product over a field #
A sum of weights is a weight of the tensor product. If the μ-weight space of M and the
ν-weight space of N are both nonzero, then so is the (μ + ν)-weight space of M ⊗ N: a pure
tensor of two nonzero vectors is nonzero over a field. This is the converse of
TauCeti.exists_weight_add_eq.
The pure tensors of weight vectors span the tensor product. The weight spaces of M and of
N exhaust them, and Submodule.map₂ distributes over suprema in both arguments.
The weight-space decomposition of a tensor product. The generalized χ-weight space of
M ⊗ N is the supremum, over the pairs of weights (μ, ν) with μ + ν = χ, of the submodules
spanned by the pure tensors m ⊗ₜ n with m of weight μ and n of weight ν.
One inclusion is TauCeti.map₂_mk_genWeightSpace_le. For the other, the family on the right has
supremum ⊤, and it lies inside the independent family of weight spaces of M ⊗ N, so
iSupIndep.le_iff_eq_of_iSup_eq_top makes the two families agree term by term.
Every weight of a tensor product is a sum of weights. If χ is a weight of M ⊗ N, then
χ = μ + ν for a weight μ of M and a weight ν of N. This is the converse of
TauCeti.genWeightSpace_tensorProduct_ne_bot.
If no such pair existed then every term of the decomposition
TauCeti.genWeightSpace_tensorProduct_eq_iSup of the χ-weight space would have a zero factor, so
that weight space would be zero.
A tensor product of finite-dimensional triangularizable modules with linear weights again has linear weights. Every weight of the tensor product is a sum of weights of the two factors.