Library Combi.SymGroup.towerSn: The Tower of the Symmetric Groups
The Tower of the Symmetric Groups
- f \ox g = cfextprod g h == the external product of class function, defined by f \ox g (u, v) := f u * f v for (u, v) in G * H. It is of of type 'CF(setX G H) when g : 'CF(G) and h : 'CF(H).
- cfextprodr g h == cfextprod h g
- extprod_repr rG rH == the external product (tensor product) of matrix representation. Its character is the external product of the character of rG and rH.
- tinj == the tower injection morphism : 'S_m * 'S_n -> 'S_(m + n)
- f \o^ g == the image along tinj of the external product of f and g.
- 'z_p == zcoeff p == The cardinality of the centralizer of any permutation of cycle type p in algC, that is #|'S_k| / #|class p|.
- '1z_p = ncfuniCT p == the normalized cycle indicator class function for cycle type p == 'z_p *: '1_[p].
- Theorem cfuni_Res which expands the restriction to 'S_m * 'S_n
of the cycle indicator class function '1_[l]:
'Res[tinj @* ('dom tinj)] '1_[l] =
\sum_(pp | l == pp.1 +|+ pp.2) '1_[pp.1] \o^ '1_[pp.2].by Frobenius duality it implies: - Theorem ncfuniCT_Ind which expands the induction of two normalized
cycle indicator class functions:
'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]) = '1z_[p +|+ q].
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg fingroup morphism perm gproduct.
From mathcomp Require Import ssrnum matrix vector mxalgebra algC.
From mathcomp Require Import classfun character mxrepresentation.
Require Import tools ordcast partition sorted.
Require Import permcomp cycles cycletype permcent.
Notation "''SG_' n" := [set: 'S_n]
(at level 8, n at level 2, format "''SG_' n").
Import LeqGeqOrder.
Set Implicit Arguments.
Import GroupScope GRing.Theory.
#[local] Open Scope Combi_scope.
Section classGroup.
Variables gT aT: finGroupType.
Variable G H : {group gT}.
Lemma class_disj x y :
y \notin x ^: G -> x ^: G :&: y ^: G = set0.
Lemma prod_conjg (x y : gT * aT) : x ^ y = (x.1 ^ y.1, x.2 ^ y.2).
End classGroup.
From mathcomp Require Import all_ssreflect.
From mathcomp Require Import ssralg fingroup morphism perm gproduct.
From mathcomp Require Import ssrnum matrix vector mxalgebra algC.
From mathcomp Require Import classfun character mxrepresentation.
Require Import tools ordcast partition sorted.
Require Import permcomp cycles cycletype permcent.
Notation "''SG_' n" := [set: 'S_n]
(at level 8, n at level 2, format "''SG_' n").
Import LeqGeqOrder.
Set Implicit Arguments.
Import GroupScope GRing.Theory.
#[local] Open Scope Combi_scope.
Section classGroup.
Variables gT aT: finGroupType.
Variable G H : {group gT}.
Lemma class_disj x y :
y \notin x ^: G -> x ^: G :&: y ^: G = set0.
Lemma prod_conjg (x y : gT * aT) : x ^ y = (x.1 ^ y.1, x.2 ^ y.2).
End classGroup.
Section CFExtProdDefs.
Variables (gT aT : finGroupType).
Variables (G : {group gT}) (H : {group aT}).
#[local] Open Scope ring_scope.
Variables (gT aT : finGroupType).
Variables (G : {group gT}) (H : {group aT}).
#[local] Open Scope ring_scope.
One could use the following alternative definition
Definition cast_cf (G H : {set gT}) (eq_GH : G = H) (f : 'CF(G)) :=
let: erefl in _ = H := eq_GH return 'CF(H) in f.
Definition cfextprod (g : 'CF(G)) (h : 'CF(H)) : 'CF(setX G H) :=
(cfMorph (cast_cf (esym (@morphim_fstX _ _ G H)) g)) *
(cfMorph (cast_cf (esym (@morphim_sndX _ _ G H)) h)).
and prove the equivalence:
Lemma cfextprodE g h x y : (g \ox h) (x, y) = (g x) * (h y).
However, the more direct definition below leads to simpler proofs, at least
once we have proved that it is indeed a class function.
Definition cast_cf (G H : {set gT}) (eq_GH : G = H) (f : 'CF(G)) :=
let: erefl in _ = H := eq_GH return 'CF(H) in f.
Definition cfextprod (g : 'CF(G)) (h : 'CF(H)) : 'CF(setX G H) :=
(cfMorph (cast_cf (esym (@morphim_fstX _ _ G H)) g)) *
(cfMorph (cast_cf (esym (@morphim_sndX _ _ G H)) h)).
Lemma cfextprodE g h x y : (g \ox h) (x, y) = (g x) * (h y).
Fact cfextprod_subproof (g : 'CF(G)) (h : 'CF(H)) :
is_class_fun <<setX G H>> [ffun x => g x.1 * h x.2].
Definition cfextprod g h := Cfun 0 (cfextprod_subproof g h).
Definition cfextprodr_head k g h := let: tt := k in cfextprod h g.
End CFExtProdDefs.
Notation "f \ox g" := (cfextprod f g) (at level 40, left associativity).
Notation cfextprodr := (cfextprodr_head tt).
Section CFExtProdTheory.
Variables (gT aT : finGroupType).
Variables (G : {group gT}) (H : {group aT}).
Implicit Type (g : 'CF(G)) (h : 'CF(H)).
#[local] Open Scope ring_scope.
Lemma cfextprodrE h g : cfextprodr h g = g \ox h.
Fact cfextprod_is_linear g : linear (cfextprod g : 'CF(H) -> 'CF(setX G H)).
Lemma cfextprod0r g : g \ox (0 : 'CF(H)) = 0.
Lemma cfextprodNr g h : g \ox - h = - (g \ox h).
Lemma cfextprodDr g h1 h2 : g \ox (h1 + h2) = g \ox h1 + g \ox h2.
Lemma cfextprodBr g h1 h2 : g \ox (h1 - h2) = g \ox h1 - g \ox h2.
Lemma cfextprodMnr h g n : g \ox (h *+ n) = (g \ox h) *+ n.
Lemma cfextprod_sumr g I r (P : pred I) (phi : I -> 'CF(H)) :
g \ox (\sum_(i <- r | P i) phi i) = \sum_(i <- r | P i) g \ox phi i.
Lemma cfextprodZr g a h : g \ox (a *: h) = a *: (g \ox h).
Fact cfextprodr_is_linear h : linear (cfextprodr h : 'CF(G) -> 'CF(setX G H)).
Lemma cfextprod0l h : (0 : 'CF(G)) \ox h = 0.
Lemma cfextprodNl h g : - g \ox h = - g \ox h.
Lemma cfextprodDl h g1 g2 : (g1 + g2) \ox h = g1 \ox h + g2 \ox h.
Lemma cfextprodBl h g1 g2 : (g1 - g2) \ox h = g1 \ox h - g2 \ox h.
Lemma cfextprodMnl h g n : g *+ n \ox h = g \ox h *+ n.
Lemma cfextprod_suml h I r (P : pred I) (phi : I -> 'CF(G)) :
(\sum_(i <- r | P i) phi i) \ox h = \sum_(i <- r | P i) phi i \ox h.
Lemma cfextprodZl h a g : (a *: g) \ox h = a *: (g \ox h).
Section ReprExtProd.
Variables (n1 n2 : nat).
Variables (rG : mx_representation algC G n1)
(rH : mx_representation algC H n2).
Fact extprod_mx_repr_subproof :
mx_repr (setX G H) (fun x => tprod (rG x.1) (rH x.2)).
Definition extprod_mx_repr := MxRepresentation extprod_mx_repr_subproof.
Lemma cfRepr_extprod : cfRepr extprod_mx_repr = cfRepr rG \ox cfRepr rH.
End ReprExtProd.
Lemma cfextprod_char g h :
g \is a character -> h \is a character -> g \ox h \is a character.
End CFExtProdTheory.
is_class_fun <<setX G H>> [ffun x => g x.1 * h x.2].
Definition cfextprod g h := Cfun 0 (cfextprod_subproof g h).
Definition cfextprodr_head k g h := let: tt := k in cfextprod h g.
End CFExtProdDefs.
Notation "f \ox g" := (cfextprod f g) (at level 40, left associativity).
Notation cfextprodr := (cfextprodr_head tt).
Section CFExtProdTheory.
Variables (gT aT : finGroupType).
Variables (G : {group gT}) (H : {group aT}).
Implicit Type (g : 'CF(G)) (h : 'CF(H)).
#[local] Open Scope ring_scope.
Lemma cfextprodrE h g : cfextprodr h g = g \ox h.
Fact cfextprod_is_linear g : linear (cfextprod g : 'CF(H) -> 'CF(setX G H)).
Lemma cfextprod0r g : g \ox (0 : 'CF(H)) = 0.
Lemma cfextprodNr g h : g \ox - h = - (g \ox h).
Lemma cfextprodDr g h1 h2 : g \ox (h1 + h2) = g \ox h1 + g \ox h2.
Lemma cfextprodBr g h1 h2 : g \ox (h1 - h2) = g \ox h1 - g \ox h2.
Lemma cfextprodMnr h g n : g \ox (h *+ n) = (g \ox h) *+ n.
Lemma cfextprod_sumr g I r (P : pred I) (phi : I -> 'CF(H)) :
g \ox (\sum_(i <- r | P i) phi i) = \sum_(i <- r | P i) g \ox phi i.
Lemma cfextprodZr g a h : g \ox (a *: h) = a *: (g \ox h).
Fact cfextprodr_is_linear h : linear (cfextprodr h : 'CF(G) -> 'CF(setX G H)).
Lemma cfextprod0l h : (0 : 'CF(G)) \ox h = 0.
Lemma cfextprodNl h g : - g \ox h = - g \ox h.
Lemma cfextprodDl h g1 g2 : (g1 + g2) \ox h = g1 \ox h + g2 \ox h.
Lemma cfextprodBl h g1 g2 : (g1 - g2) \ox h = g1 \ox h - g2 \ox h.
Lemma cfextprodMnl h g n : g *+ n \ox h = g \ox h *+ n.
Lemma cfextprod_suml h I r (P : pred I) (phi : I -> 'CF(G)) :
(\sum_(i <- r | P i) phi i) \ox h = \sum_(i <- r | P i) phi i \ox h.
Lemma cfextprodZl h a g : (a *: g) \ox h = a *: (g \ox h).
Section ReprExtProd.
Variables (n1 n2 : nat).
Variables (rG : mx_representation algC G n1)
(rH : mx_representation algC H n2).
Fact extprod_mx_repr_subproof :
mx_repr (setX G H) (fun x => tprod (rG x.1) (rH x.2)).
Definition extprod_mx_repr := MxRepresentation extprod_mx_repr_subproof.
Lemma cfRepr_extprod : cfRepr extprod_mx_repr = cfRepr rG \ox cfRepr rH.
End ReprExtProd.
Lemma cfextprod_char g h :
g \is a character -> h \is a character -> g \ox h \is a character.
End CFExtProdTheory.
Section TowerMorphism.
Variables m n : nat.
#[local] Notation ct := cycle_typeSn.
#[local] Notation SnXm := (setX 'SG_m 'SG_n).
Definition tinjval (s : 'S_m * 'S_n) :=
fun (x : 'I_(m + n)) => match split x with
| inl a => unsplit (inl (s.1 a))
| inr a => unsplit (inr (s.2 a))
end.
Fact tinjval_inj s : injective (tinjval s).
Definition tinj s : 'S_(m + n) := perm (@tinjval_inj s).
Fact tinj_morphM : {morph tinj : x y / x * y >-> x * y}.
Canonical morph_of_tinj := Morphism (D := SnXm) (in2W tinj_morphM).
Lemma isom_tinj : isom SnXm (tinj @* ('dom tinj)) tinj.
Lemma expg_tinj_lshift s a i :
(tinj s ^+ i) (lshift n a) = lshift n ((s.1 ^+ i) a).
Lemma expg_tinj_rshift s a i :
(tinj s ^+ i) (rshift m a) = rshift m ((s.2 ^+ i) a).
Lemma porbit_tinj_lshift s a :
porbit (tinj s) (lshift n a) = [set @lshift m n x | x in porbit s.1 a].
Lemma porbit_tinj_rshift s a :
porbit (tinj s) (rshift m a) = [set @rshift m n x | x in porbit s.2 a].
Lemma porbits_tinj s :
porbits (tinj s) =
[set (@lshift m n) @: x | x : {set 'I_m} in porbits s.1]
:|:
[set (@rshift m n) @: x | x : {set 'I_n} in porbits s.2].
Lemma cycle_type_tinj s : ct (tinj s) = ct s.1 +|+ ct s.2.
End TowerMorphism.
Arguments tinj {m n} s.
Variables m n : nat.
#[local] Notation ct := cycle_typeSn.
#[local] Notation SnXm := (setX 'SG_m 'SG_n).
Definition tinjval (s : 'S_m * 'S_n) :=
fun (x : 'I_(m + n)) => match split x with
| inl a => unsplit (inl (s.1 a))
| inr a => unsplit (inr (s.2 a))
end.
Fact tinjval_inj s : injective (tinjval s).
Definition tinj s : 'S_(m + n) := perm (@tinjval_inj s).
Fact tinj_morphM : {morph tinj : x y / x * y >-> x * y}.
Canonical morph_of_tinj := Morphism (D := SnXm) (in2W tinj_morphM).
Lemma isom_tinj : isom SnXm (tinj @* ('dom tinj)) tinj.
Lemma expg_tinj_lshift s a i :
(tinj s ^+ i) (lshift n a) = lshift n ((s.1 ^+ i) a).
Lemma expg_tinj_rshift s a i :
(tinj s ^+ i) (rshift m a) = rshift m ((s.2 ^+ i) a).
Lemma porbit_tinj_lshift s a :
porbit (tinj s) (lshift n a) = [set @lshift m n x | x in porbit s.1 a].
Lemma porbit_tinj_rshift s a :
porbit (tinj s) (rshift m a) = [set @rshift m n x | x in porbit s.2 a].
Lemma porbits_tinj s :
porbits (tinj s) =
[set (@lshift m n) @: x | x : {set 'I_m} in porbits s.1]
:|:
[set (@rshift m n) @: x | x : {set 'I_n} in porbits s.2].
Lemma cycle_type_tinj s : ct (tinj s) = ct s.1 +|+ ct s.2.
End TowerMorphism.
Arguments tinj {m n} s.
Section Assoc.
Variables m n p : nat.
Lemma cast_rshift j : cast_ord (esym (add0n n)) j = rshift 0 j.
Lemma cast_lshift j : cast_ord (esym (addn0 n)) j = lshift 0 j.
Lemma tinj1E (t : 'S_n) : tinj (1%g, t) = cast_perm (esym (add0n n)) t.
Lemma tinjE1 (t : 'S_n) : tinj (t, 1%g) = cast_perm (esym (addn0 n)) t.
Lemma tinjA (s : 'S_m) (t : 'S_n) (u : 'S_p) :
tinj (tinj(s, t), u) = cast_perm (addnA m n p) (tinj (s, tinj (t, u))).
Lemma cycle_type_tinjC (s : 'S_m) (t : 'S_n) :
cycle_typeSn (tinj (s, t)) =
cycle_typeSn (cast_perm (esym (addnC m n)) (tinj (t, s))).
End Assoc.
Notation "f \o^ g" := (cfIsom (isom_tinj _ _) (f \ox g)) (at level 40).
#[local] Open Scope ring_scope.
Variables m n p : nat.
Lemma cast_rshift j : cast_ord (esym (add0n n)) j = rshift 0 j.
Lemma cast_lshift j : cast_ord (esym (addn0 n)) j = lshift 0 j.
Lemma tinj1E (t : 'S_n) : tinj (1%g, t) = cast_perm (esym (add0n n)) t.
Lemma tinjE1 (t : 'S_n) : tinj (t, 1%g) = cast_perm (esym (addn0 n)) t.
Lemma tinjA (s : 'S_m) (t : 'S_n) (u : 'S_p) :
tinj (tinj(s, t), u) = cast_perm (addnA m n p) (tinj (s, tinj (t, u))).
Lemma cycle_type_tinjC (s : 'S_m) (t : 'S_n) :
cycle_typeSn (tinj (s, t)) =
cycle_typeSn (cast_perm (esym (addnC m n)) (tinj (t, s))).
End Assoc.
Notation "f \o^ g" := (cfIsom (isom_tinj _ _) (f \ox g)) (at level 40).
#[local] Open Scope ring_scope.
Section Restriction.
Variables m n : nat.
#[local] Notation ct := cycle_typeSn.
Lemma cfuni_tinj s (l : 'P_(m + n)) :
'1_[l] (tinj s) = (l == ct s.1 +|+ ct s.2)%:R.
Theorem cfuni_Res (l : 'P_(m + n)) :
'Res[tinj @* ('dom tinj)] '1_[l] =
\sum_(pp | l == pp.1 +|+ pp.2) '1_[pp.1] \o^ '1_[pp.2].
End Restriction.
Variables m n : nat.
#[local] Notation ct := cycle_typeSn.
Lemma cfuni_tinj s (l : 'P_(m + n)) :
'1_[l] (tinj s) = (l == ct s.1 +|+ ct s.2)%:R.
Theorem cfuni_Res (l : 'P_(m + n)) :
'Res[tinj @* ('dom tinj)] '1_[l] =
\sum_(pp | l == pp.1 +|+ pp.2) '1_[pp.1] \o^ '1_[pp.2].
End Restriction.
Section Induction.
Variables m n : nat.
Implicit Types (p : 'P_m) (q : 'P_n).
#[local] Notation ct := cycle_typeSn.
#[local] Notation SnXm := (setX 'SG_m 'SG_n).
#[local] Notation classX p q := ((permCT p, permCT q) ^: SnXm).
Import GroupScope GRing.Theory Num.Theory.
#[local] Open Scope ring_scope.
Lemma classXE p q : classX p q = setX (classCT p) (classCT q).
Lemma cfextprod_cfuni p q : '1_[p] \ox '1_[q] = '1_(classX p q).
Lemma cfdot_classfun_part p1 p2 :
'[ '1_[p1], '1_[p2] ] = #|'SG_m|%:R^-1 * #|classCT p1|%:R * (p1 == p2)%:R.
Lemma decomp_cf_triv : \sum_(p : 'P_n) '1_[p] = 1.
Lemma classXI p1 p2 q1 q2 :
(p2, q2) != (p1, q1) -> (classX p1 q1) :&: (classX p2 q2) = set0.
Variables m n : nat.
Implicit Types (p : 'P_m) (q : 'P_n).
#[local] Notation ct := cycle_typeSn.
#[local] Notation SnXm := (setX 'SG_m 'SG_n).
#[local] Notation classX p q := ((permCT p, permCT q) ^: SnXm).
Import GroupScope GRing.Theory Num.Theory.
#[local] Open Scope ring_scope.
Lemma classXE p q : classX p q = setX (classCT p) (classCT q).
Lemma cfextprod_cfuni p q : '1_[p] \ox '1_[q] = '1_(classX p q).
Lemma cfdot_classfun_part p1 p2 :
'[ '1_[p1], '1_[p2] ] = #|'SG_m|%:R^-1 * #|classCT p1|%:R * (p1 == p2)%:R.
Lemma decomp_cf_triv : \sum_(p : 'P_n) '1_[p] = 1.
Lemma classXI p1 p2 q1 q2 :
(p2, q2) != (p1, q1) -> (classX p1 q1) :&: (classX p2 q2) = set0.
The normalized cycle type indicator basis
Definition zcoeff (k : nat) (p : 'P_k) : algC :=
#|'SG_k|%:R / #|classCT p|%:R.
Notation "''z_' p" := (zcoeff p) (at level 2, format "''z_' p").
Lemma zcoeffE k (l : 'P_k) : zcoeff l = (zcard l)%:R.
Lemma neq0zcoeff (k : nat) (p : 'P_k) : 'z_p != 0.
Hint Resolve neq0zcoeff : core.
Definition ncfuniCT (k : nat) (p : 'P_k) := 'z_p *: '1_[p].
Notation "''1z_[' p ]" := (ncfuniCT p) (format "''1z_[' p ]").
Lemma ncfuniCT_gen k (f : 'CF('SG_k)) :
f = \sum_(p : 'P_k) f (permCT p) / 'z_p *: '1z_[p].
Lemma cfdotr_ncfuniCT k (f : 'CF('SG_k)) (s : 'S_k) : (f s) = '[f, '1z_[ct s]].
#|'SG_k|%:R / #|classCT p|%:R.
Notation "''z_' p" := (zcoeff p) (at level 2, format "''z_' p").
Lemma zcoeffE k (l : 'P_k) : zcoeff l = (zcard l)%:R.
Lemma neq0zcoeff (k : nat) (p : 'P_k) : 'z_p != 0.
Hint Resolve neq0zcoeff : core.
Definition ncfuniCT (k : nat) (p : 'P_k) := 'z_p *: '1_[p].
Notation "''1z_[' p ]" := (ncfuniCT p) (format "''1z_[' p ]").
Lemma ncfuniCT_gen k (f : 'CF('SG_k)) :
f = \sum_(p : 'P_k) f (permCT p) / 'z_p *: '1z_[p].
Lemma cfdotr_ncfuniCT k (f : 'CF('SG_k)) (s : 'S_k) : (f s) = '[f, '1z_[ct s]].
Application of Frobenius duality : cfdot_Res_r
Lemma cfdot_Ind_cfuniCT p q (l : 'P_(m + n)) :
'[ 'Ind['SG_(m + n)] ('1_[p] \o^ '1_[q]), '1_[l] ] =
(p +|+ q == l)%:R / 'z_p / 'z_q.
Lemma cfdot_Ind_ncfuniCT p q (l : 'P_(m + n)) :
'[ 'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]), '1z_[l] ] =
(p +|+ q == l)%:R * 'z_l.
Theorem ncfuniCT_Ind p q :
'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]) = '1z_[p +|+ q].
End Induction.
Notation "''z_' p" := (zcoeff p) (at level 2, format "''z_' p").
Notation "''1z_[' p ]" := (ncfuniCT p) (format "''1z_[' p ]").
#[export] Hint Resolve neq0zcoeff : core.
'[ 'Ind['SG_(m + n)] ('1_[p] \o^ '1_[q]), '1_[l] ] =
(p +|+ q == l)%:R / 'z_p / 'z_q.
Lemma cfdot_Ind_ncfuniCT p q (l : 'P_(m + n)) :
'[ 'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]), '1z_[l] ] =
(p +|+ q == l)%:R * 'z_l.
Theorem ncfuniCT_Ind p q :
'Ind['SG_(m + n)] ('1z_[p] \o^ '1z_[q]) = '1z_[p +|+ q].
End Induction.
Notation "''z_' p" := (zcoeff p) (at level 2, format "''z_' p").
Notation "''1z_[' p ]" := (ncfuniCT p) (format "''1z_[' p ]").
#[export] Hint Resolve neq0zcoeff : core.