The first decomposition of the standard representation

When 2 is invertible, the tensor square of a representation splits into its symmetric and exterior squares. This file establishes the representation equivalence and specializes it to the standard representation of the general linear group. Over any field, it also records the corresponding character identity, which remains valid even when the decomposition does not split.

Main definitions

• TauCeti.tensorSquareRepEquiv specializes it to the standard representation of GL n k.
• TauCeti.char_tensorSquare_stdRep is the tensor-square character identity.

References

• Classical groups roadmap, Layer 1, “The first decomposition”.
• W. Fulton and J. Harris, Representation Theory: A First Course, Lecture 6.

@[reducible, inline]

noncomputable abbrev TauCeti.tensorSquareRepEquiv (k : Type) (n : ℕ) [CommRing k] [Invertible 2] : (tensorPowerRep k n 2).Equiv ((symPowerRep k n 2).prod (extPowerRep k n 2))

The tensor square of the standard representation is equivalent to the product of its symmetric and exterior squares.

Equations

• TauCeti.tensorSquareRepEquiv k n = (TauCeti.stdRep k n).tensorSquareEquivSymmetricExterior

noncomputable def TauCeti.tensorSquareFDRepIso (k : Type) (n : ℕ) [CommRing k] [Invertible 2] : tensorPowerFDRep k n 2 ≅ FDRep.of ((symPowerRep k n 2).prod (extPowerRep k n 2))

The tensor-square decomposition bundled as an isomorphism in FDRep. The product representation is the direct sum of the symmetric and exterior squares.

Equations

• TauCeti.tensorSquareFDRepIso k n = Action.mkIso (TauCeti.tensorSquareRepEquiv k n).toLinearEquiv.toFGModuleCatIso ⋯

@[simp]

theorem TauCeti.tensorSquareFDRepIso_hom_hom (k : Type) (n : ℕ) [CommRing k] [Invertible 2] : (tensorSquareFDRepIso k n).hom.hom = CategoryTheory.ConcreteCategory.ofHom (↑(tensorSquareRepEquiv k n)).toLinearMap

The forward map of the bundled tensor-square decomposition is the natural representation equivalence.

@[simp]

theorem TauCeti.tensorSquareFDRepIso_inv_hom (k : Type) (n : ℕ) [CommRing k] [Invertible 2] : (tensorSquareFDRepIso k n).inv.hom = CategoryTheory.ConcreteCategory.ofHom (↑(tensorSquareRepEquiv k n).symm).toLinearMap

The inverse map of the bundled tensor-square decomposition is the inverse natural representation equivalence.

theorem TauCeti.char_tensorSquare_stdRep (k : Type) (n : ℕ) [Field k] (g : GL (Fin n) k) : (↑g).trace ^ 2 = (symPowerRep k n 2).character g + (extPowerRep k n 2).character g

Over any field, the square of the standard character is the sum of the symmetric-square and exterior-square characters.