Tensor powers of the standard representation

This file specializes the diagonal tensor-power construction to the standard representation of the general linear group. It supplies the tensor powers that underpin the Weyl construction for polynomial representations, together with the description of their monoid-algebra image over an infinite field.

Main results

• TauCeti.tensorPowerRep is the d-fold tensor power of stdRep.
• TauCeti.tensorPowerFDRep is its bundled finite-dimensional form.
• TauCeti.commute_permTensorAction_tensorPowerRep proves that the general-linear and symmetric-group actions commute, and TauCeti.commute_permTensorActionAlgHom_tensorPowerRep extends that to the whole group algebra k[S_d].
• TauCeti.permTensorPowerRep combines the two commuting actions into one representation of S_d × GL n k, and TauCeti.range_asAlgebraHom_permTensorAction_le_comap says that the image of any element of k[S_d], such as a Young symmetrizer, is a GL n k-subrepresentation.
• TauCeti.trace_permTensorAction_conj_mul_tensorPowerRep: for any g ∈ GL n k, the trace of a permutation of the tensor factors composed with g^{⊗d} is a class function of the permutation.
• TauCeti.tensorPowerPermIntertwiningMap packages g^{⊗d} as an intertwining map of the symmetric-group action, and TauCeti.tensorPowerIntertwiningRep is the resulting action of GL n k on the S_d-intertwining maps into the tensor power, by composition.
• TauCeti.toSubmodule_range_tensorPowerRep_asAlgebraHom_eq_span_range_map_const identifies the image of k[GLₙ] with the span of all diagonal tensor operators over an infinite field.

@[reducible, inline]

noncomputable abbrev TauCeti.tensorPowerRep (k : Type u) (n d : ℕ) [CommRing k] : Representation k (GL (Fin n) k) (TensorPower k d (Fin n → k))

The diagonal action of GL n k on the d-fold tensor power of its standard representation.

@[reducible, inline]

noncomputable abbrev TauCeti.tensorPowerFDRep (k : Type u) (n d : ℕ) [CommRing k] : FDRep k (GL (Fin n) k)

The tensor power of the standard representation, bundled as an object of FDRep.

theorem TauCeti.commute_permTensorAction_tensorPowerRep (k : Type u) (n d : ℕ) [CommRing k] (σ : Equiv.Perm (Fin d)) (g : GL (Fin n) k) : Commute ((permTensorAction k n d) σ) ((tensorPowerRep k n d) g)

The actions of GL n k and the symmetric group on the tensor power commute.

This is the commuting-actions half of Schur--Weyl duality; it makes no double-centralizer claim.

theorem TauCeti.trace_permTensorAction_conj_mul_tensorPowerRep {k : Type u} {n d : ℕ} [CommRing k] (σ τ : Equiv.Perm (Fin d)) (g : GL (Fin n) k) : (LinearMap.trace k (PiTensorProduct k fun (x : Fin d) => Fin n → k)) ((permTensorAction k n d) (τ * σ * τ⁻¹) * (tensorPowerRep k n d) g) = (LinearMap.trace k (PiTensorProduct k fun (x : Fin d) => Fin n → k)) ((permTensorAction k n d) σ * (tensorPowerRep k n d) g)

The trace of a permutation of the tensor factors composed with g^{⊗d} is a class function of the permutation, because the two actions commute.

theorem TauCeti.commute_permTensorActionAlgHom_tensorPowerRep (k : Type u) (n d : ℕ) [CommRing k] (a : MonoidAlgebra k (Equiv.Perm (Fin d))) (g : GL (Fin n) k) : Commute ((permTensorActionAlgHom k n d) a) ((tensorPowerRep k n d) g)

The whole group algebra k[S_d] commutes with the general-linear action on the tensor power, so a Young symmetrizer cuts out a GL n k-subrepresentation.

theorem TauCeti.range_asAlgebraHom_permTensorAction_le_comap (k : Type u) (n d : ℕ) [CommRing k] (a : MonoidAlgebra k (Equiv.Perm (Fin d))) (g : GL (Fin n) k) : LinearMap.range ((permTensorAction k n d).asAlgebraHom a) ≤ Submodule.comap ((tensorPowerRep k n d) g) (LinearMap.range ((permTensorAction k n d).asAlgebraHom a))

The image of an element of k[S_d] in (kⁿ)^{⊗d} is stable under GL n k, because the two actions commute. In particular a Young symmetrizer cuts out a subrepresentation.

noncomputable def TauCeti.permTensorPowerRep (k : Type u) (n d : ℕ) [CommRing k] : Representation k (Equiv.Perm (Fin d) × GL (Fin n) k) (TensorPower k d (Fin n → k))

The joint action of S_d × GL n k on (kⁿ)^{⊗d}: a pair (σ, g) acts by permuting the tensor factors by σ after applying g in every factor. It is a representation of the product group because the two actions commute.

@[simp]

theorem TauCeti.permTensorPowerRep_apply (k : Type u) (n d : ℕ) [CommRing k] (σ : Equiv.Perm (Fin d)) (g : GL (Fin n) k) : (permTensorPowerRep k n d) (σ, g) = (permTensorAction k n d) σ * (tensorPowerRep k n d) g

The pair (σ, g) acts on (kⁿ)^{⊗d} as σ ∘ g^{⊗d}.

noncomputable def TauCeti.tensorPowerPermIntertwiningMap (k : Type u) (n d : ℕ) [CommRing k] (g : GL (Fin n) k) : (permTensorAction k n d).IntertwiningMap (permTensorAction k n d)

The operator g^{⊗d} on (kⁿ)^{⊗d} as an intertwining map of the symmetric-group action: the diagonal action of GL n k commutes with permuting the tensor factors.

@[simp]

theorem TauCeti.tensorPowerPermIntertwiningMap_apply (k : Type u) (n d : ℕ) [CommRing k] (g : GL (Fin n) k) (x : TensorPower k d (Fin n → k)) : (tensorPowerPermIntertwiningMap k n d g) x = ((tensorPowerRep k n d) g) x

noncomputable def TauCeti.tensorPowerIntertwiningRep {k : Type u} {n d : ℕ} [CommRing k] {W : Type u_1} [AddCommGroup W] [Module k W] (ρ : Representation k (Equiv.Perm (Fin d)) W) : Representation k (GL (Fin n) k) (ρ.IntertwiningMap (permTensorAction k n d))

The representation of GL n k on the S_d-intertwining maps from ρ into (kⁿ)^{⊗d}, by composition with g^{⊗d}. In a split semisimple setting, when ρ is irreducible, this is the multiplicity space of ρ in the tensor power, with its residual action of the general linear group.

@[simp]

theorem TauCeti.tensorPowerIntertwiningRep_apply_apply {k : Type u} {n d : ℕ} [CommRing k] {W : Type u_1} [AddCommGroup W] [Module k W] (ρ : Representation k (Equiv.Perm (Fin d)) W) (g : GL (Fin n) k) (f : ρ.IntertwiningMap (permTensorAction k n d)) (w : W) : (((tensorPowerIntertwiningRep ρ) g) f) w = ((tensorPowerRep k n d) g) (f w)

theorem TauCeti.span_range_tensorPowerRep_eq_span_range_map_const (k : Type u) (n d : ℕ) [Field k] [Infinite k] : Submodule.span k (Set.range ⇑(tensorPowerRep k n d)) = Submodule.span k (Set.range fun (f : (Fin n → k) →ₗ[k] Fin n → k) => PiTensorProduct.map fun (x : Fin d) => f)

The general linear group spans the same operators on (kⁿ)^{⊗d} as the whole endomorphism algebra of kⁿ: the span of the diagonal operators g^{⊗d} for g invertible is the span of all the diagonal operators f^{⊗d}. This is the Zariski density of the invertible endomorphisms of kⁿ, and it needs the field to be infinite.

theorem TauCeti.toSubmodule_range_tensorPowerRep_asAlgebraHom_eq_span_range_map_const (k : Type u) (n d : ℕ) [Field k] [Infinite k] : Subalgebra.toSubmodule (tensorPowerRep k n d).asAlgebraHom.range = Submodule.span k (Set.range fun (f : (Fin n → k) →ₗ[k] Fin n → k) => PiTensorProduct.map fun (x : Fin d) => f)

The image of the monoid algebra k[GLₙ] in End ((kⁿ)^{⊗d}) is the span of all the diagonal operators f^{⊗d}, with f ranging over every endomorphism of kⁿ and not only the invertible ones.

theorem TauCeti.char_tensorPowerRep (k : Type u) (n d : ℕ) [Field k] (g : GL (Fin n) k) : (tensorPowerRep k n d).character g = (↑g).trace ^ d

The character of the tensor power is the corresponding power of the standard character.

This is intentionally not a simp lemma: Representation.char_tensorPower and char_stdRep already normalize its left-hand side, so registering this specialization would violate simpNF.

@[simp]

theorem TauCeti.char_tensorPowerFDRep (k : Type u) (n d : ℕ) [Field k] (g : GL (Fin n) k) : (tensorPowerFDRep k n d).character g = (↑g).trace ^ d

The character of the bundled tensor power is the corresponding power of the matrix trace.