Library Combi.SymGroup.reprSn: Basic representations of the Symmetric Groups

Basic representation of the Symmetric Groups

We define the two representations of dimension 1 together with the natural representation, and show that 'S_2 has only 2 representations. More precisely, for a fixed n and g : 'S_n:

triv_mx g == the 1x1 identity matrix.
sign_mx g == the 1x1 scalar matrix equal to the sign of g.
signed_mx R g == given a representation R the matrix sign g * R g
nat_mx g == the permutation matrix associated to g

These four matrices are actually representation matrices:

triv_repr == the trivial representation
sign_repr == the sign representation
signed_repr R == the representation R times the sign
nat_repr n == the natural representation of degree n

We show in Lemmas repr1 and repr_S2 that triv_repr and sign_repr exhausts all representations of 'S_n of degree 1 and all irreducible representations of of 'S_2.

From mathcomp Require Import all_ssreflect.
From mathcomp Require Import fingroup perm ssralg morphism perm action.
From mathcomp Require Import zmodp. From mathcomp Require Import vector matrix mxalgebra ssrnum algC.
From mathcomp Require Import mxrepresentation classfun character.

Require Import permcomp tools partition congr cycles cycletype presentSn.

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
#[local] Open Scope ring_scope.

#[local] Notation reprS n d := (mx_representation algC 'SG_n d).

Section TcastVal.
Variable (T : eqType).

Lemma tval_tcastE m n (eq_mn : m = n) (t : m.-tuple T) :
  tcast eq_mn t = t :> seq T.

End TcastVal.

Section LinRepr.

Variables (gT : finGroupType) (G : {group gT}).

Lemma cfRepr1_lin_char (rG : mx_representation algC G 1) :
  cfRepr rG \is a linear_char.

Lemma lin_char_reprP xi :
  reflect (exists rG : mx_representation algC G 1, xi = cfRepr rG)
          (xi \is a linear_char).

End LinRepr.

Lemma NirrSn n : Nirr 'SG_n = #|{:'P_n }|.

Section EltrConj.

Variable n : nat.

Lemma cycle_type_eltr i :
  (i < n)%N -> cycle_typeSn (eltr n i) = hookpartn n.+1 1.

Lemma eltr_conj i j :
  (i < n)%N -> (j < n)%N -> exists t , eltr n i = ((eltr n j) ^ t)%g.

End EltrConj.

Representation of dimension 1 and natural representation

Section DefTrivSign.

Context {n : nat} (d : nat).

Definition triv_mx (g : 'S_n) : 'M[algC]_1 := 1.
Definition sign_mx (g : 'S_n) : 'M[algC]_1 := (-1) ^+ (odd_perm g).
Definition signed_mx (rho : reprS n d) (g : 'S_n) : 'M[algC]_d :=
  (-1) ^+ (odd_perm g) *: rho g.

Definition nat_mx (g : 'S_n) : 'M[algC]_n := perm_mx g.

Lemma triv_mx_repr : mx_repr 'SG_n triv_mx.
Canonical triv_repr : reprS n 1 := MxRepresentation triv_mx_repr.

Lemma triv_irr : mx_irreducible triv_repr.

Lemma sign_mx_repr : mx_repr 'SG_n sign_mx.
Canonical sign_repr : reprS n 1 := MxRepresentation sign_mx_repr.

Lemma sign_irr : mx_irreducible sign_repr.

Lemma signed_mx_repr rho : mx_repr 'SG_n (signed_mx rho).
Canonical signed_repr rho : reprS n d := MxRepresentation (signed_mx_repr rho).

Lemma nat_mx_repr : mx_repr 'SG_n nat_mx.
Canonical nat_repr : reprS n n := MxRepresentation nat_mx_repr.

Lemma cfRepr_triv : cfRepr triv_repr = 1.

Lemma cfRepr_trivE : cfRepr triv_repr = 'chi_0.
Lemma triv_Chi : mx_rsim triv_repr 'Chi_0.

Lemma sign_char_subproof :
  is_class_fun <<'SG_n>> [ffun g => (-1) ^+ (odd_perm g)].
Definition sign_char := Cfun 0 sign_char_subproof.

Lemma cfRepr_sign : cfRepr sign_repr = sign_char.
Lemma sign_charP : sign_char \is a linear_char.

Lemma cfRepr_signed (rho : reprS n d) :
  cfRepr (signed_repr rho) = sign_char * cfRepr rho.

End DefTrivSign.

Representations of the symmetric Group for n = 0 and 1

Lemma row_free1 : row_free (1 : 'M[algC]_1).

Lemma charSG0 X : X \in irr 'SG_0 -> X = 1.

Lemma charSG1 X : X \in irr 'SG_1 -> X = 1.

Lemma repr1_S0 (rho : reprS 0 1) : mx_rsim rho triv_repr.

Lemma repr1_S1 (rho : reprS 1 1) : mx_rsim rho triv_repr.

Representations of dimension 1 the symmetric Group for n > 1

Lemma triv_sign_neq n : (n > 1)%N -> 1 != sign_char :> 'CF('SG_n).

Lemma triv_sign_not_sim n :
  (n > 1)%N -> ~ mx_rsim (G := [group of 'SG_n]) triv_repr sign_repr.

Lemma lin_char_Sn n (xi : 'CF('SG_n)) :
  xi \is a linear_char -> xi = 1 \/ xi = sign_char.

Lemma repr1 n (rho : reprS n 1) :
  mx_rsim rho triv_repr \/ mx_rsim rho sign_repr.

Representations of the symmetric Group for n=2

Lemma NirrS2 : Nirr 'SG_2 = 2.

Lemma cast_IirrS2 (i : Iirr 'SG_2) :
i != 0 -> i = cast_ord (esym NirrS2) 1.

Lemma sign_char2 : sign_char = 'chi_(cast_ord (esym NirrS2) 1).

Lemma cfRepr_sign2 : cfRepr sign_repr = 'chi_(cast_ord (esym NirrS2) 1).

Lemma sign_Chi2 : mx_rsim sign_repr 'Chi_(cast_ord (esym NirrS2) 1).

Lemma irr_S2 : irr 'SG_2 = tcast (esym NirrS2) [tuple 1; sign_char].

Lemma repr_S2 (rho : representation algC [group of 'SG_2]) :
mx_irreducible rho -> mx_rsim rho triv_repr \/ mx_rsim rho sign_repr.