Weights add on a tensor product

A diagonal matrix acts on a pure tensor of weight vectors by the product of the two scalars, so a tensor product of weight vectors is again a weight vector and its weight is the sum of the two weights (TauCeti.tmul_mem_weightSpace_tprod). This file promotes that one-line computation to a decomposition: once each factor is spanned by its weight spaces, so is the tensor product, and — once distinct weights give distinct characters of the torus — its weight-l space is exactly the sum of the products of the weight spaces of the factors over the pairs of weights adding up to l.

The two directions are of quite different natures. The inclusion of the sum of products into the weight space is the computation above and needs only a commutative ring, and so does the fact that the weight spaces of the tensor product span it — that one is the distributivity of Submodule.map₂ over suprema, applied to TensorProduct.map₂_mk_top_top_eq_top. The reverse inclusion is not a computation at all: it says that a weight vector of the tensor product has no component outside the pieces just constructed, and that is read off the independence of the weight spaces (TauCeti.iSupIndep_weightSpace) through iSupIndep.le_iff_eq_of_iSup_eq_top. So it inherits the standing hypothesis of the weight theory, that distinct weights give distinct characters of the torus, and with it the coefficients: over 𝔽₂ the torus is trivial and nothing is independent.

The determinant powers are the worked case, and they need neither ingredient above. Because det ^ m is the one-dimensional representation on which the torus acts by the character of the constant weight fun _ ↦ m, the identification W ⊗[k] k ≃ₗ[k] W carries the action of ρ ⊗ det ^ m to the action of ρ rescaled by that one character, which cancels off the eigen-relation. So tensoring with det ^ m translates the weights of an arbitrary representation by the constant sequence m (TauCeti.weightSpace_tprod_detPowerRep), over a commutative ring, with no separation of weights and no assumption that ρ is weight-decomposed. The same holds on the left, through k ⊗[k] W ≃ₗ[k] W (TauCeti.weightSpace_detPowerRep_tprod), and that is the orientation in which the rational representations of GL n are written — and so it does for the twist Representation.charTwist (det ^ m) ρ, which is that tensor product with the line already absorbed, where the translation becomes an equality of submodules of the one carrier (TauCeti.weightSpace_charTwist_detPow). What is proved here is exactly that translation of weight spaces; it is the step that the classification of the irreducible rational representations of GL n as det-twists of the polynomial ones runs on, but that classification needs the highest-weight theory and is not proved here.

Main results

• TauCeti.tmul_mem_weightSpace_tprod: a pure tensor of weight vectors has the sum of the two weights.
• TauCeti.iSup_weightSpace_tprod_eq_top: the weight spaces of a tensor product span it, as soon as the weight spaces of each factor span.
• TauCeti.weightSpace_tprod: weights add. The weight-l space of a tensor product is the sum, over the weights a of the first factor, of the products of the weight space of a with the weight space of l - a in the second, once the weight spaces of each factor span and distinct weights give distinct characters.
• TauCeti.isInternal_weightSpace_tprod: a tensor product of weight-decomposed representations is weight-decomposed, once distinct weights give distinct characters.
• TauCeti.weightSpace_tprod_detPowerRep and TauCeti.weightSpace_detPowerRep_tprod: tensoring with det ^ m translates weights by the constant sequence m, for an arbitrary representation, on either side, the translation being read through W ⊗[k] k ≃ₗ[k] W and k ⊗[k] W ≃ₗ[k] W.
• TauCeti.weightSpace_charTwist_detPow: the same translation for the twist Representation.charTwist (det ^ m) ρ, where it is an equality of submodules of the one carrier, no identification intervening.

Implementation notes

The sum defining the weight-l space is indexed by a single weight a, the weight of the first factor, with l - a the weight of the second; indexing instead by the pairs (a, b) with a + b = l would carry a subtype through every rewrite for no gain.

The products of weight spaces are written with Submodule.map₂ (TensorProduct.mk k W W') rather than with a tensor product of submodules: Submodule.map₂ is the image of the pure tensors, which is what the statements need, and it comes with the distributivity over suprema that the spanning proof runs on.

The two tensor orientations of the determinant twist are instead stated as a Submodule.comap along W ⊗[k] k ≃ₗ[k] W and k ⊗[k] W ≃ₗ[k] W, in that one form only: Submodule.mem_comap then reads membership in the twisted weight space off membership in the untwisted one, and the image form is Submodule.map_comap_eq_of_surjective away. The twist Representation.charTwist (det ^ m) ρ carries no identification at all, its carrier being that of ρ, so there the translation is a bare equality of submodules of the one carrier. All three run on the same private lemma, which asks only that some equivalence carry the action of the twisted representation to the action of ρ rescaled by det ^ m — TensorProduct.rid, TensorProduct.lid and LinearEquiv.refl respectively; the three cases differ merely in that computation.

References

• W. Fulton and J. Harris, Representation Theory: A First Course (1991), Lecture 15.

Pure tensors of weight vectors

theorem TauCeti.tmul_mem_weightSpace_tprod {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {W' : Type w} [AddCommGroup W'] [Module k W'] {ρ : Representation k (GL (Fin n) k) W} {σ : Representation k (GL (Fin n) k) W'} {a b : Fin n → ℤ} {w : W} {w' : W'} (hw : w ∈ weightSpace ρ a) (hw' : w' ∈ weightSpace σ b) : w ⊗ₜ[k] w' ∈ weightSpace (ρ.tprod σ) (a + b)

A pure tensor of weight vectors is a weight vector of the sum of the two weights: a diagonal matrix scales the two factors by the two characters, hence the tensor by their product, and characters multiply when weights are added.

theorem TauCeti.map₂_weightSpace_le_weightSpace_tprod {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {W' : Type w} [AddCommGroup W'] [Module k W'] (ρ : Representation k (GL (Fin n) k) W) (σ : Representation k (GL (Fin n) k) W') (a b : Fin n → ℤ) : Submodule.map₂ (TensorProduct.mk k W W') (weightSpace ρ a) (weightSpace σ b) ≤ weightSpace (ρ.tprod σ) (a + b)

The product of the weight-a space of one representation with the weight-b space of another lies in the weight-(a + b) space of their tensor product.

theorem TauCeti.iSup_map₂_weightSpace_le_weightSpace_tprod {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {W' : Type w} [AddCommGroup W'] [Module k W'] (ρ : Representation k (GL (Fin n) k) W) (σ : Representation k (GL (Fin n) k) W') (l : Fin n → ℤ) : ⨆ (a : Fin n → ℤ), Submodule.map₂ (TensorProduct.mk k W W') (weightSpace ρ a) (weightSpace σ (l - a)) ≤ weightSpace (ρ.tprod σ) l

The sum, over the weights a of the first factor, of the products of the weight-a space with the weight-(l - a) space of the second factor lies in the weight-l space of the tensor product. This is the easy half of TauCeti.weightSpace_tprod.

Spanning

theorem TauCeti.iSup_weightSpace_tprod_eq_top {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {W' : Type w} [AddCommGroup W'] [Module k W'] {ρ : Representation k (GL (Fin n) k) W} {σ : Representation k (GL (Fin n) k) W'} (hρ : ⨆ (a : Fin n → ℤ), weightSpace ρ a = ⊤) (hσ : ⨆ (b : Fin n → ℤ), weightSpace σ b = ⊤) : ⨆ (l : Fin n → ℤ), weightSpace (ρ.tprod σ) l = ⊤

The weight spaces of a tensor product span it, as soon as the weight spaces of each factor span. No separation of weights is needed: this is the computation TauCeti.tmul_mem_weightSpace_tprod on pure tensors, spread over the whole tensor product.

The determinant twist

@[simp]

theorem TauCeti.weightSpace_tprod_detPowerRep {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (m : ℤ) (l : Fin n → ℤ) : weightSpace (ρ.tprod (detPowerRep k n m)) l = Submodule.comap (↑(TensorProduct.rid k W)) (weightSpace ρ (l - fun (x : Fin n) => m))

Tensoring with det ^ m on the right translates weights by the constant sequence m: read through W ⊗[k] k ≃ₗ[k] W, the weight-l space of ρ ⊗ det ^ m is the weight-(l - m) space of ρ. This holds for every representation ρ over every commutative ring, since det ^ m is the one-dimensional representation on which the torus acts by the character of the constant weight m. Nothing beyond this translation of weight spaces is claimed: it is the computation underlying the classification of the irreducible rational representations of GL n as det-twists of the polynomial ones, which is not proved here.

@[simp]

theorem TauCeti.weightSpace_detPowerRep_tprod {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (m : ℤ) (l : Fin n → ℤ) : weightSpace ((detPowerRep k n m).tprod ρ) l = Submodule.comap (↑(TensorProduct.lid k W)) (weightSpace ρ (l - fun (x : Fin n) => m))

Tensoring with det ^ m on the left translates weights by the constant sequence m: read through k ⊗[k] W ≃ₗ[k] W, the weight-l space of det ^ m ⊗ ρ is the weight-(l - m) space of ρ. This is the orientation in which the rational representations of GL n are written as det-twists of the polynomial ones; like its right-handed companion TauCeti.weightSpace_tprod_detPowerRep it holds for every ρ over every commutative ring.

@[simp]

theorem TauCeti.weightSpace_charTwist_detPow {k : Type u} [CommRing k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] (ρ : Representation k (GL (Fin n) k) W) (m : ℤ) (l : Fin n → ℤ) : weightSpace (Representation.charTwist (Matrix.GeneralLinearGroup.det ^ m) ρ) l = weightSpace ρ (l - fun (x : Fin n) => m)

Twisting by the linear character det ^ m translates weights by the constant sequence m: the twist Representation.charTwist (det ^ m) ρ has the same carrier as ρ, so no identification intervenes and the weight-l space of the twist is the weight-(l - m) space of ρ on the nose. This is the orientation in which a rational representation of GL n is realized on a polynomial one, TauCeti.weightSpace_detPowerRep_tprod being the same translation read through k ⊗[k] W ≃ₗ[k] W.

Weights add

Here the coefficients must separate weights, in the sense that l ↦ weightChar k l is injective; TauCeti.weightChar_injective supplies that over an infinite field.

theorem TauCeti.weightSpace_tprod {k : Type u} [Field k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {W' : Type w} [AddCommGroup W'] [Module k W'] {ρ : Representation k (GL (Fin n) k) W} {σ : Representation k (GL (Fin n) k) W'} (hchar : Function.Injective (weightChar k)) (hρ : ⨆ (a : Fin n → ℤ), weightSpace ρ a = ⊤) (hσ : ⨆ (b : Fin n → ℤ), weightSpace σ b = ⊤) (l : Fin n → ℤ) : weightSpace (ρ.tprod σ) l = ⨆ (a : Fin n → ℤ), Submodule.map₂ (TensorProduct.mk k W W') (weightSpace ρ a) (weightSpace σ (l - a))

Weights add. The weight-l space of a tensor product is the sum, over the weights a of the first factor, of the products of the weight-a space with the weight-(l - a) space of the second factor.

Only the inclusion ≥ is a computation; the inclusion ≤ says that a weight vector of the tensor product has no component outside those products, and comes from the independence of the weight spaces, whence the separation hypothesis.

theorem TauCeti.isInternal_weightSpace_tprod {k : Type u} [Field k] {n : ℕ} {W : Type v} [AddCommGroup W] [Module k W] {W' : Type w} [AddCommGroup W'] [Module k W'] {ρ : Representation k (GL (Fin n) k) W} {σ : Representation k (GL (Fin n) k) W'} (hchar : Function.Injective (weightChar k)) (hρ : ⨆ (a : Fin n → ℤ), weightSpace ρ a = ⊤) (hσ : ⨆ (b : Fin n → ℤ), weightSpace σ b = ⊤) : DirectSum.IsInternal fun (l : Fin n → ℤ) => weightSpace (ρ.tprod σ) l

A tensor product of weight-decomposed representations is weight-decomposed. Only the spanning half of the hypothesis on each factor is needed: once weights are separated, the independence of the weight spaces of the tensor product is automatic (TauCeti.isInternal_weightSpace_of_iSup_eq_top).