Exterior powers of representations

This file equips each exterior power of a representation with the induced diagonal action. Intertwining maps and equivalences pass functorially to exterior powers, and the zeroth and first exterior powers recover the trivial and original representations.

Main definitions

• Representation.exteriorPower is the induced action on ⋀[R]^d M.
• IntertwiningMap.exteriorPower is the induced map between exterior-power representations.
• Representation.Equiv.exteriorPower is the induced equivalence.

References

• Classical groups roadmap, Layer 1, “Symmetric and exterior power representations”.

The functorial exterior-power API transported here — exteriorPower.map, its identity and composition laws, and the equivalences exteriorPower.zeroEquiv and exteriorPower.oneEquiv — is Mathlib's Mathlib.LinearAlgebra.ExteriorPower.Basic, by Sophie Morel and Joël Riou.

noncomputable def Representation.exteriorPower {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) (d : ℕ) : Representation R G ↥(⋀[R]^d M)

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

Equations

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

@[simp]

theorem Representation.exteriorPower_apply {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) (d : ℕ) (g : G) : (ρ.exteriorPower d) g = exteriorPower.map d (ρ g)

The action on an exterior power is induced by the action on the original representation.

theorem Representation.exteriorPower_apply_ιMulti {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) (d : ℕ) (g : G) (m : Fin d → M) : ((ρ.exteriorPower d) g) ((exteriorPower.ιMulti R d) m) = (exteriorPower.ιMulti R d) (⇑(ρ g) ∘ m)

The exterior-power action applies the original action to every factor of a pure wedge.

This is intentionally not a simp lemma: exteriorPower_apply followed by Mathlib's exteriorPower.map_apply_ιMulti already performs this simplification.

noncomputable def Representation.exteriorPowerZeroEquiv {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) : (ρ.exteriorPower 0).Equiv (trivial R G R)

The zeroth exterior power is equivalent to the trivial representation on the scalars.

Equations

• ρ.exteriorPowerZeroEquiv = Representation.Equiv.mk (exteriorPower.zeroEquiv R M) ⋯

@[simp]

theorem Representation.exteriorPowerZeroEquiv_toLinearEquiv {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) : ρ.exteriorPowerZeroEquiv.toLinearEquiv = exteriorPower.zeroEquiv R M

The underlying linear equivalence is Mathlib's identification of the zeroth exterior power with the scalars.

noncomputable def Representation.exteriorPowerOneEquiv {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) : (ρ.exteriorPower 1).Equiv ρ

The first exterior power is equivalent to the original representation.

Equations

• ρ.exteriorPowerOneEquiv = Representation.Equiv.mk (exteriorPower.oneEquiv R M) ⋯

@[simp]

theorem Representation.exteriorPowerOneEquiv_toLinearEquiv {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] (ρ : Representation R G M) : ρ.exteriorPowerOneEquiv.toLinearEquiv = exteriorPower.oneEquiv R M

The underlying linear equivalence is Mathlib's identification of the first exterior power with the module itself.

noncomputable def Representation.IntertwiningMap.exteriorPower {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (f : ρ.IntertwiningMap σ) (d : ℕ) : (ρ.exteriorPower d).IntertwiningMap (σ.exteriorPower d)

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

Equations

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

@[simp]

theorem Representation.IntertwiningMap.exteriorPower_toLinearMap {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (f : ρ.IntertwiningMap σ) (d : ℕ) : (f.exteriorPower d).toLinearMap = exteriorPower.map d f.toLinearMap

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

@[simp]

theorem Representation.IntertwiningMap.exteriorPower_apply_ιMulti {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (f : ρ.IntertwiningMap σ) (d : ℕ) (m : Fin d → M) : (f.exteriorPower d) ((exteriorPower.ιMulti R d) m) = (exteriorPower.ιMulti R d) (⇑f ∘ m)

The induced map sends a pure wedge to the wedge of the images of its factors.

@[simp]

theorem Representation.IntertwiningMap.exteriorPower_id {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] {ρ : Representation R G M} (d : ℕ) : (id ρ).exteriorPower d = id (ρ.exteriorPower d)

Exterior powers preserve identity intertwining maps.

@[simp]

theorem Representation.IntertwiningMap.exteriorPower_comp {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} {P : Type u_1} [AddCommGroup P] [Module R P] {τ : Representation R G P} (f : ρ.IntertwiningMap σ) (g : σ.IntertwiningMap τ) (d : ℕ) : (g.comp f).exteriorPower d = (g.exteriorPower d).comp (f.exteriorPower d)

Exterior powers preserve composition of intertwining maps.

noncomputable def Representation.Equiv.exteriorPower {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) : (ρ.exteriorPower d).Equiv (σ.exteriorPower d)

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

Equations

• e.exteriorPower d = Representation.Equiv.mk (Representation.Equiv.exteriorPowerLinearEquiv✝ e d) ⋯

@[simp]

theorem Representation.Equiv.exteriorPower_toLinearMap {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) : (↑(e.exteriorPower d)).toLinearMap = exteriorPower.map d (↑e).toLinearMap

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

@[simp]

theorem Representation.Equiv.exteriorPower_apply_ιMulti {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) (m : Fin d → M) : (e.exteriorPower d) ((exteriorPower.ιMulti R d) m) = (exteriorPower.ιMulti R d) (⇑e ∘ m)

The induced equivalence sends a pure wedge to the wedge of the images of its factors.

@[simp]

theorem Representation.Equiv.exteriorPower_refl {R : Type u} {G : Type v} {M : Type w} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] {ρ : Representation R G M} (d : ℕ) : (refl ρ).exteriorPower d = refl (ρ.exteriorPower d)

Exterior powers preserve identity equivalences.

@[simp]

theorem Representation.Equiv.exteriorPower_symm {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} (e : ρ.Equiv σ) (d : ℕ) : e.symm.exteriorPower d = (e.exteriorPower d).symm

Exterior powers preserve inverses of equivalences.

@[simp]

theorem Representation.Equiv.exteriorPower_trans {R : Type u} {G : Type v} {M : Type w} {N : Type w'} [CommRing R] [Monoid G] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] {ρ : Representation R G M} {σ : Representation R G N} {P : Type u_1} [AddCommGroup P] [Module R P] {τ : Representation R G P} (e : ρ.Equiv σ) (f : σ.Equiv τ) (d : ℕ) : (e.trans f).exteriorPower d = (e.exteriorPower d).trans (f.exteriorPower d)

Exterior powers preserve composition of equivalences.