Exterior powers of the standard representation

This file specializes exterior powers of representations to the standard representation of the general linear group. The resulting action applies a matrix to every factor of a pure wedge.

In the top degree d = n the action collapses to a scalar: a matrix acts on ⋀[k]^n (Fin n → k) by its determinant, so that exterior power is the determinant representation.

Main definitions

• TauCeti.extPowerRep is the exterior-power representation of GL n k.
• TauCeti.extPowerFDRep is its bundled finite-dimensional form.
• TauCeti.topExtPowerEquivDet identifies the top exterior power with the determinant representation, and TauCeti.extPowerFDRepDetIso is its bundled form.

Main results

• TauCeti.char_extPowerRep_diagonal identifies the character on diagonal matrices with an elementary symmetric polynomial.
• TauCeti.extPowerRep_self_apply and TauCeti.char_extPowerRep_self compute the top-degree action and character as the determinant.

Vanishing of ⋀[k]^d (Fin n → k), and hence extPowerRep k n d, once n < d is given by exteriorPower.eq_zero_of_finrank_lt in TauCeti.LinearAlgebra.ExteriorPower.Basic. The degree-zero and degree-one identifications of extPowerRep k n are the generic (stdRep k n).exteriorPowerZeroEquiv and (stdRep k n).exteriorPowerOneEquiv.

References

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

@[reducible, inline]

noncomputable abbrev TauCeti.extPowerRep (k : Type u) (n d : ℕ) [CommRing k] : Representation k (GL (Fin n) k) ↥(⋀[k]^d (Fin n → k))

The dth exterior power of the standard representation of GL n k.

Equations

• TauCeti.extPowerRep k n d = (TauCeti.stdRep k n).exteriorPower d

@[reducible, inline]

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

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

Equations

• TauCeti.extPowerFDRep k n d = FDRep.of (TauCeti.extPowerRep k n d)

theorem TauCeti.extPowerRep_self_apply (k : Type u) (n : ℕ) [CommRing k] (g : GL (Fin n) k) : (extPowerRep k n n) g = (↑g).det • LinearMap.id

In the top degree a matrix acts on the exterior power by multiplication by its determinant.

This is deliberately not a simp lemma: Representation.exteriorPower_apply and stdRep_apply already rewrite the left-hand side to exteriorPower.map n (Matrix.mulVecLin ↑g), so it is not in simp normal form and the rewrite could never fire. The simp-normal statement is Module.Basis.map_exteriorPower_top_eq_det_smul, applied here to Pi.basisFun k (Fin n).

noncomputable def TauCeti.topExtPowerEquivDet (k : Type u) (n : ℕ) [CommRing k] : (extPowerRep k n n).Equiv (detRep k n)

The top exterior power of the standard representation is the determinant representation. The identification sends a wedge of n vectors to the determinant of the matrix they form.

Equations

• TauCeti.topExtPowerEquivDet k n = Representation.Equiv.mk (Pi.basisFun k (Fin n)).exteriorPowerTopEquiv ⋯

@[simp]

theorem TauCeti.topExtPowerEquivDet_toLinearEquiv (k : Type u) (n : ℕ) [CommRing k] : (topExtPowerEquivDet k n).toLinearEquiv = (Pi.basisFun k (Fin n)).exteriorPowerTopEquiv

The underlying linear equivalence of TauCeti.topExtPowerEquivDet is the top-degree identification of the exterior power with the scalars.

@[simp]

theorem TauCeti.topExtPowerEquivDet_apply_ιMulti (k : Type u) (n : ℕ) [CommRing k] (v : Fin n → Fin n → k) : (topExtPowerEquivDet k n) ((exteriorPower.ιMulti k n) v) = (Matrix.of v).det

The identification sends a wedge of n vectors to the determinant of the matrix they form.

noncomputable def TauCeti.extPowerFDRepDetIso (k : Type u) (n : ℕ) [CommRing k] : extPowerFDRep k n n ≅ detFDRep k n

The identification of the top exterior power with the determinant representation, bundled as an isomorphism in FDRep.

Equations

• TauCeti.extPowerFDRepDetIso k n = Action.mkIso (TauCeti.topExtPowerEquivDet k n).toLinearEquiv.toFGModuleCatIso ⋯

@[simp]

theorem TauCeti.extPowerFDRepDetIso_hom_hom (k : Type u) (n : ℕ) [CommRing k] : (extPowerFDRepDetIso k n).hom.hom = CategoryTheory.ConcreteCategory.ofHom (↑(topExtPowerEquivDet k n)).toLinearMap

The forward map of the bundled identification is the underlying representation equivalence.

@[simp]

theorem TauCeti.extPowerFDRepDetIso_inv_hom (k : Type u) (n : ℕ) [CommRing k] : (extPowerFDRepDetIso k n).inv.hom = CategoryTheory.ConcreteCategory.ofHom (↑(topExtPowerEquivDet k n).symm).toLinearMap

The inverse map of the bundled identification is the inverse representation equivalence.

@[simp]

theorem TauCeti.char_extPowerRep_diagonal (k : Type u) (n d : ℕ) [Field k] (t : Fin n → kˣ) : (extPowerRep k n d).character (diagGL t) = (MvPolynomial.eval fun (i : Fin n) => ↑(t i)) (MvPolynomial.esymm (Fin n) k d)

The character of the dth exterior power on a diagonal matrix is the dth elementary symmetric polynomial in its diagonal entries.

theorem TauCeti.char_extPowerRep_self (k : Type u) (n : ℕ) [Field k] (g : GL (Fin n) k) : (extPowerRep k n n).character g = (↑g).det

The character of the top exterior power of the standard representation is the determinant.

This is deliberately not a simp lemma: on a diagonal matrix its left-hand side is also matched by TauCeti.char_extPowerRep_diagonal, whose elementary-symmetric right-hand side is a different normal form.