Symmetric powers of representations

This file equips each symmetric power of a representation with the induced diagonal action. Intertwining maps and equivalences pass functorially to symmetric powers.

Main definitions

• Representation.symmetricPower is the induced action on Sym[R]^d M.
• IntertwiningMap.symmetricPower is the induced map between symmetric-power representations.
• Representation.Equiv.symmetricPower is the induced equivalence.

References

• Classical groups roadmap, Layer 1, “Symmetric and exterior power representations”.
• The representation and equivariance constructions are adapted from the formal template in TauCeti.RepresentationTheory.ExteriorPower.

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

The action induced by a representation on its dth symmetric power.

Equations

• ρ.symmetricPower d = { toFun := fun (g : G) => SymmetricPower.map (ρ g), map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Representation.symmetricPower_apply {R : Type} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (g : G) : (ρ.symmetricPower d) g = SymmetricPower.map (ρ g)

The action on a symmetric power is induced by the action on the original representation.

theorem Representation.symmetricPower_apply_tprod {R : Type} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] (ρ : Representation R G M) (d : ℕ) (g : G) (m : Fin d → M) : ((ρ.symmetricPower d) g) (⨂ₛ[R] (i : Fin d), m i) = ⨂ₛ[R] (i : Fin d), (ρ g) (m i)

The symmetric-power action applies the original action to every factor of a pure tensor.

This is intentionally not a simp lemma: symmetricPower_apply followed by SymmetricPower.map_tprod already performs this simplification.

noncomputable def Representation.IntertwiningMap.symmetricPower {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (f : ρ.IntertwiningMap σ) (d : ℕ) : (ρ.symmetricPower d).IntertwiningMap (σ.symmetricPower d)

An intertwining map induces an intertwining map on every symmetric power.

Equations

• f.symmetricPower d = { toLinearMap := SymmetricPower.map f.toLinearMap, isIntertwining' := ⋯ }

@[simp]

theorem Representation.IntertwiningMap.symmetricPower_toLinearMap {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (f : ρ.IntertwiningMap σ) (d : ℕ) : (f.symmetricPower d).toLinearMap = SymmetricPower.map f.toLinearMap

The underlying linear map is the usual map induced on symmetric powers.

@[simp]

theorem Representation.IntertwiningMap.symmetricPower_apply_tprod {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (f : ρ.IntertwiningMap σ) (d : ℕ) (m : Fin d → M) : (f.symmetricPower d) (⨂ₛ[R] (i : Fin d), m i) = ⨂ₛ[R] (i : Fin d), f (m i)

The induced map sends a pure symmetric tensor to the tensor of the images.

@[simp]

theorem Representation.IntertwiningMap.symmetricPower_id {R : Type} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] {ρ : Representation R G M} (d : ℕ) : (id ρ).symmetricPower d = id (ρ.symmetricPower d)

Symmetric powers preserve identity intertwining maps.

@[simp]

theorem Representation.IntertwiningMap.symmetricPower_comp {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} {P : Type u_1} [AddCommMonoid P] [Module R P] {τ : Representation R G P} (f : ρ.IntertwiningMap σ) (g : σ.IntertwiningMap τ) (d : ℕ) : (g.comp f).symmetricPower d = (g.symmetricPower d).comp (f.symmetricPower d)

Symmetric powers preserve composition of intertwining maps.

noncomputable def Representation.Equiv.symmetricPower {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) : (ρ.symmetricPower d).Equiv (σ.symmetricPower d)

An equivalence of representations induces an equivalence of every symmetric power.

Equations

• e.symmetricPower d = Representation.Equiv.mk (Representation.Equiv.symmetricPowerLinearEquiv✝ e d) ⋯

@[simp]

theorem Representation.Equiv.symmetricPower_toLinearMap {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) : (↑(e.symmetricPower d)).toLinearMap = SymmetricPower.map (↑e).toLinearMap

The underlying linear map is the usual map induced on symmetric powers.

@[simp]

theorem Representation.Equiv.symmetricPower_apply_tprod {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) (m : Fin d → M) : (e.symmetricPower d) (⨂ₛ[R] (i : Fin d), m i) = ⨂ₛ[R] (i : Fin d), e (m i)

The induced equivalence sends a pure symmetric tensor to the tensor of the images.

@[simp]

theorem Representation.Equiv.symmetricPower_refl {R : Type} {G : Type v} {M : Type w} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] {ρ : Representation R G M} (d : ℕ) : (refl ρ).symmetricPower d = refl (ρ.symmetricPower d)

Symmetric powers preserve identity equivalences.

@[simp]

theorem Representation.Equiv.symmetricPower_symm {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) : e.symm.symmetricPower d = (e.symmetricPower d).symm

Symmetric powers preserve inverses of equivalences.

@[simp]

theorem Representation.Equiv.symmetricPower_trans {R : Type} {G : Type v} {M : Type w} {N : Type w'} [CommSemiring R] [Monoid G] [AddCommMonoid M] [Module R M] [AddCommMonoid N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} {P : Type u_1} [AddCommMonoid P] [Module R P] {τ : Representation R G P} (e : ρ.Equiv σ) (f : σ.Equiv τ) (d : ℕ) : (e.trans f).symmetricPower d = (e.symmetricPower d).trans (f.symmetricPower d)

Symmetric powers preserve composition of equivalences.