Tensor powers of representations

This file equips the tensor power of a representation with its diagonal action. The action on a pure tensor applies the original action in every factor. This construction is used by the classical-groups roadmap to form tensor powers of the standard representation.

Main definitions

• Representation.tensorPower is the diagonal action on ⨂[R]^d M.

References

• Classical groups roadmap, Layer 1.

@[simp]

theorem TauCeti.TensorPower.map_fin_zero {R : Type u} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] (f : Fin 0 → M →ₗ[R] M) : PiTensorProduct.map f = LinearMap.id

A family of linear maps indexed by Fin 0 acts as the identity on the zero-fold tensor power.

theorem TauCeti.TensorPower.mulEquiv_conj_map {R : Type u} {M : Type w} [CommSemiring R] [AddCommMonoid M] [Module R M] {d e : ℕ} (f : Fin d → M →ₗ[R] M) (g : Fin e → M →ₗ[R] M) : TensorPower.mulEquiv.conj (TensorProduct.map (PiTensorProduct.map f) (PiTensorProduct.map g)) = PiTensorProduct.map (Fin.append f g)

Splitting a tensor power intertwines separate families of maps on the two factors with their appended family on the combined tensor power.

noncomputable def Representation.tensorPower {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) : Representation R G (TensorPower R d M)

The diagonal action of G on the d-fold tensor power of a representation.

Equations

• ρ.tensorPower d = PiTensorProduct.mapMonoidHom.comp (MonoidHom.pi fun (x : Fin d) => ρ)

@[simp]

theorem Representation.tensorPower_apply {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (g : G) : (ρ.tensorPower d) g = PiTensorProduct.map fun (x : Fin d) => ρ g

The tensor-power action applies the original action in every tensor factor.

theorem Representation.tensorPower_zero_apply {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (g : G) : (ρ.tensorPower 0) g = LinearMap.id

The action on the zero-fold tensor power is the identity.

This is intentionally not a simp lemma: tensorPower_apply followed by TauCeti.TensorPower.map_fin_zero already performs this simplification.

noncomputable def Representation.tensorPowerAddEquiv {R : Type u} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d e : ℕ) : ((ρ.tensorPower d).tprod (ρ.tensorPower e)).Equiv (ρ.tensorPower (d + e))

Splitting the factors gives an equivalence from the tensor product of two tensor-power representations to the tensor power indexed by their sum.

Equations

• ρ.tensorPowerAddEquiv d e = Representation.Equiv.mk TensorPower.mulEquiv ⋯

@[simp]

theorem Representation.char_tensorPower {R : Type u} {G : Type v} {M : Type w} [Field R] [Monoid G] [AddCommGroup M] [Module R M] [FiniteDimensional R M] (ρ : Representation R G M) (d : ℕ) (g : G) : (ρ.tensorPower d).character g = ρ.character g ^ d

The character of a tensor-power representation is the corresponding power of the character.