Library mathcomp.character.vcharacter

(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.                  
 Distributed under the terms of CeCILL-B.                                  *)

Require Import mathcomp.ssreflect.ssreflect.

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

This file provides basic notions of virtual character theory: 'Z[S, A] == collective predicate for the phi that are Z-linear combinations of elements of S : seq 'CF(G) and have support in A : {set gT}. 'Z[S] == collective predicate for the Z-linear combinations of elements of S. 'Z[irr G] == the collective predicate for virtual characters. dirr G == the collective predicate for normal virtual characters, i.e., virtual characters of norm 1: mu \in dirr G <=> m \in 'Z[irr G] and ' [mu] = 1 <=> mu or - mu \in irr G. > othonormal subsets of 'Z[irr G] are contained in dirr G. dIirr G == an index type for normal virtual characters. dchi i == the normal virtual character of index i. of_irr i == the (unique) irreducible constituent of dchi i: dchi i = 'chi(of_irr i) or - 'chi(of_irr i). ndirr i == the index of - dchi i. dirr1 G == the normal virtual character index of 1 : 'CF(G), the principal character. dirr_dIirr j f == the index i (or dirr1 G if it does not exist) such that dchi i = f j. dirr_constt phi == the normal virtual character constituents of phi: i \in dirr_constt phi <=> [dchi i, phi] > 0. to_dirr phi i == the normal virtual character constituent of phi with an irreducible constituent i, when i \in irr_constt phi.

Section Basics.

Variables (gT : finGroupType) (B : {set gT}) (S : seq 'CF(B)) (A : {set gT}).

Definition Zchar : pred_class :=
  [pred phi in 'CF(B, A) | dec_Cint_span (in_tuple S) phi].
Fact Zchar_key : pred_key Zchar.
Canonical Zchar_keyed := KeyedPred Zchar_key.

Lemma cfun0_zchar : 0 \in Zchar.

Fact Zchar_zmod : zmod_closed Zchar.
Canonical Zchar_opprPred := OpprPred Zchar_zmod.
Canonical Zchar_addrPred := AddrPred Zchar_zmod.
Canonical Zchar_zmodPred := ZmodPred Zchar_zmod.

Lemma scale_zchar a phi : a \in Cint phi \in Zchar a *: phi \in Zchar.

End Basics.

Notation "''Z[' S , A ]" := (Zchar S A)
  (at level 8, format "''Z[' S , A ]") : group_scope.
Notation "''Z[' S ]" := 'Z[S, setT]
  (at level 8, format "''Z[' S ]") : group_scope.

Section Zchar.

Variables (gT : finGroupType) (G : {group gT}).
Implicit Types (A B : {set gT}) (S : seq 'CF(G)).

Lemma zchar_split S A phi :
  phi \in 'Z[S, A] = (phi \in 'Z[S]) && (phi \in 'CF(G, A)).

Lemma zcharD1E phi S : (phi \in 'Z[S, G^#]) = (phi \in 'Z[S]) && (phi 1%g == 0).

Lemma zcharD1 phi S A :
  (phi \in 'Z[S, A^#]) = (phi \in 'Z[S, A]) && (phi 1%g == 0).

Lemma zcharW S A : {subset 'Z[S, A] 'Z[S]}.

Lemma zchar_on S A : {subset 'Z[S, A] 'CF(G, A)}.

Lemma zchar_onS A B S : A \subset B {subset 'Z[S, A] 'Z[S, B]}.

Lemma zchar_onG S : 'Z[S, G] =i 'Z[S].

Lemma irr_vchar_on A : {subset 'Z[irr G, A] 'CF(G, A)}.

Lemma support_zchar S A phi : phi \in 'Z[S, A] support phi \subset A.

Lemma mem_zchar_on S A phi :
  phi \in 'CF(G, A) phi \in S phi \in 'Z[S, A].

A special lemma is needed because trivial fails to use the cfun_onT Hint.
Lemma mem_zchar S phi : phi \in S phi \in 'Z[S].

Lemma zchar_nth_expansion S A phi :
    phi \in 'Z[S, A]
  {z | i, z i \in Cint & phi = \sum_(i < size S) z i *: S`_i}.

Lemma zchar_tuple_expansion n (S : n.-tuple 'CF(G)) A phi :
    phi \in 'Z[S, A]
  {z | i, z i \in Cint & phi = \sum_(i < n) z i *: S`_i}.

A pure seq version with the extra hypothesis of S's unicity.
Lemma zchar_expansion S A phi : uniq S
    phi \in 'Z[S, A]
  {z | xi, z xi \in Cint & phi = \sum_(xi <- S) z xi *: xi}.

Lemma zchar_span S A : {subset 'Z[S, A] <<S>>%VS}.

Lemma zchar_trans S1 S2 A B :
  {subset S1 'Z[S2, B]} {subset 'Z[S1, A] 'Z[S2, A]}.

Lemma zchar_trans_on S1 S2 A :
  {subset S1 'Z[S2, A]} {subset 'Z[S1] 'Z[S2, A]}.

Lemma zchar_sub_irr S A :
  {subset S 'Z[irr G]} {subset 'Z[S, A] 'Z[irr G, A]}.

Lemma zchar_subset S1 S2 A :
  {subset S1 S2} {subset 'Z[S1, A] 'Z[S2, A]}.

Lemma zchar_subseq S1 S2 A :
  subseq S1 S2 {subset 'Z[S1, A] 'Z[S2, A]}.

Lemma zchar_filter S A (p : pred 'CF(G)) :
  {subset 'Z[filter p S, A] 'Z[S, A]}.

End Zchar.

Section VChar.

Variables (gT : finGroupType) (G : {group gT}).
Implicit Types (A B : {set gT}) (phi chi : 'CF(G)) (S : seq 'CF(G)).

Lemma char_vchar chi : chi \is a character chi \in 'Z[irr G].

Lemma irr_vchar i : 'chi[G]_i \in 'Z[irr G].

Lemma cfun1_vchar : 1 \in 'Z[irr G].

Lemma vcharP phi :
  reflect (exists2 chi1, chi1 \is a character
            & exists2 chi2, chi2 \is a character & phi = chi1 - chi2)
          (phi \in 'Z[irr G]).

Lemma Aint_vchar phi x : phi \in 'Z[irr G] phi x \in Aint.

Lemma Cint_vchar1 phi : phi \in 'Z[irr G] phi 1%g \in Cint.

Lemma Cint_cfdot_vchar_irr i phi : phi \in 'Z[irr G] '[phi, 'chi_i] \in Cint.

Lemma cfdot_vchar_r phi psi :
  psi \in 'Z[irr G] '[phi, psi] = \sum_i '[phi, 'chi_i] × '[psi, 'chi_i].

Lemma Cint_cfdot_vchar : {in 'Z[irr G] &, phi psi, '[phi, psi] \in Cint}.

Lemma Cnat_cfnorm_vchar : {in 'Z[irr G], phi, '[phi] \in Cnat}.

Fact vchar_mulr_closed : mulr_closed 'Z[irr G].
Canonical vchar_mulrPred := MulrPred vchar_mulr_closed.
Canonical vchar_smulrPred := SmulrPred vchar_mulr_closed.
Canonical vchar_semiringPred := SemiringPred vchar_mulr_closed.
Canonical vchar_subringPred := SubringPred vchar_mulr_closed.

Lemma mul_vchar A :
  {in 'Z[irr G, A] &, phi psi, phi × psi \in 'Z[irr G, A]}.

Section CfdotPairwiseOrthogonal.

Variables (M : {group gT}) (S : seq 'CF(G)) (nu : 'CF(G) 'CF(M)).
Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (oSS : pairwise_orthogonal S).

Let freeS := orthogonal_free oSS.
Let uniqS : uniq S := free_uniq freeS.
Let Z_S : {subset S 'Z[S]}.
Let notS0 : 0 \notin S.
Let dotSS := proj2 (pairwise_orthogonalP oSS).

Lemma map_pairwise_orthogonal : pairwise_orthogonal (map nu S).

Lemma cfproj_sum_orthogonal P z phi :
    phi \in S
  '[\sum_(xi <- S | P xi) z xi *: nu xi, nu phi]
    = if P phi then z phi × '[phi] else 0.

Lemma cfdot_sum_orthogonal z1 z2 :
  '[\sum_(xi <- S) z1 xi *: nu xi, \sum_(xi <- S) z2 xi *: nu xi]
    = \sum_(xi <- S) z1 xi × (z2 xi)^* × '[xi].

Lemma cfnorm_sum_orthogonal z :
  '[\sum_(xi <- S) z xi *: nu xi] = \sum_(xi <- S) `|z xi| ^+ 2 × '[xi].

Lemma cfnorm_orthogonal : '[\sum_(xi <- S) nu xi] = \sum_(xi <- S) '[xi].

End CfdotPairwiseOrthogonal.

Lemma orthogonal_span S phi :
    pairwise_orthogonal S phi \in <<S>>%VS
  {z | z = fun xi'[phi, xi] / '[xi] & phi = \sum_(xi <- S) z xi *: xi}.

Section CfDotOrthonormal.

Variables (M : {group gT}) (S : seq 'CF(G)) (nu : 'CF(G) 'CF(M)).
Hypotheses (Inu : {in 'Z[S] &, isometry nu}) (onS : orthonormal S).
Let oSS := orthonormal_orthogonal onS.
Let freeS := orthogonal_free oSS.
Let nS1 : {in S, phi, '[phi] = 1}.

Lemma map_orthonormal : orthonormal (map nu S).

Lemma cfproj_sum_orthonormal z phi :
  phi \in S '[\sum_(xi <- S) z xi *: nu xi, nu phi] = z phi.

Lemma cfdot_sum_orthonormal z1 z2 :
  '[\sum_(xi <- S) z1 xi *: xi, \sum_(xi <- S) z2 xi *: xi]
     = \sum_(xi <- S) z1 xi × (z2 xi)^*.

Lemma cfnorm_sum_orthonormal z :
  '[\sum_(xi <- S) z xi *: nu xi] = \sum_(xi <- S) `|z xi| ^+ 2.

Lemma cfnorm_map_orthonormal : '[\sum_(xi <- S) nu xi] = (size S)%:R.

Lemma orthonormal_span phi :
    phi \in <<S>>%VS
  {z | z = fun xi'[phi, xi] & phi = \sum_(xi <- S) z xi *: xi}.

End CfDotOrthonormal.

Lemma cfnorm_orthonormal S :
  orthonormal S '[\sum_(xi <- S) xi] = (size S)%:R.

Lemma vchar_orthonormalP S :
    {subset S 'Z[irr G]}
  reflect ( I : {set Iirr G}, b : Iirr G bool,
           perm_eq S [seq (-1) ^+ b i *: 'chi_i | i in I])
          (orthonormal S).

Lemma vchar_norm1P phi :
    phi \in 'Z[irr G] '[phi] = 1
   b : bool, i : Iirr G, phi = (-1) ^+ b *: 'chi_i.

Lemma zchar_small_norm phi n :
    phi \in 'Z[irr G] '[phi] = n%:R (n < 4)%N
  {S : n.-tuple 'CF(G) |
    [/\ orthonormal S, {subset S 'Z[irr G]} & phi = \sum_(xi <- S) xi]}.

Lemma vchar_norm2 phi :
    phi \in 'Z[irr G, G^#] '[phi] = 2%:R
   i, exists2 j, j != i & phi = 'chi_i - 'chi_j.

End VChar.

Section Isometries.

Variables (gT : finGroupType) (L G : {group gT}) (S : seq 'CF(L)).
Implicit Type nu : {additive 'CF(L) 'CF(G)}.

Lemma Zisometry_of_cfnorm (tauS : seq 'CF(G)) :
    pairwise_orthogonal S pairwise_orthogonal tauS
    map cfnorm tauS = map cfnorm S {subset tauS 'Z[irr G]}
  {tau : {linear 'CF(L) 'CF(G)} | map tau S = tauS
       & {in 'Z[S], isometry tau, to 'Z[irr G]}}.

Lemma Zisometry_of_iso f :
    free S {in S, isometry f, to 'Z[irr G]}
  {tau : {linear 'CF(L) 'CF(G)} | {in S, tau =1 f}
       & {in 'Z[S], isometry tau, to 'Z[irr G]}}.

Lemma Zisometry_inj A nu :
  {in 'Z[S, A] &, isometry nu} {in 'Z[S, A] &, injective nu}.

Lemma isometry_in_zchar nu : {in S &, isometry nu} {in 'Z[S] &, isometry nu}.

End Isometries.

Section AutVchar.

Variables (u : {rmorphism algC algC}) (gT : finGroupType) (G : {group gT}).
Implicit Type (S : seq 'CF(G)) (phi chi : 'CF(G)).

Lemma cfAut_zchar S A psi :
  cfAut_closed u S psi \in 'Z[S, A] psi^u \in 'Z[S, A].

Lemma cfAut_vchar A psi : psi \in 'Z[irr G, A] psi^u \in 'Z[irr G, A].

Lemma sub_aut_zchar S A psi :
   {subset S 'Z[irr G]} psi \in 'Z[S, A] psi^u \in 'Z[S, A]
  psi - psi^u \in 'Z[S, A^#].

Lemma conjC_vcharAut chi x : chi \in 'Z[irr G] (u (chi x))^* = u (chi x)^*.

Lemma cfdot_aut_vchar phi chi :
  chi \in 'Z[irr G] '[phi^u , chi^u] = u '[phi, chi].

Lemma vchar_aut A chi : (chi^u \in 'Z[irr G, A]) = (chi \in 'Z[irr G, A]).

End AutVchar.

Definition cfConjC_vchar := cfAut_vchar conjC.

Section MoreVchar.

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

Lemma cfRes_vchar phi : phi \in 'Z[irr G] 'Res[H] phi \in 'Z[irr H].

Lemma cfRes_vchar_on A phi :
  H \subset G phi \in 'Z[irr G, A] 'Res[H] phi \in 'Z[irr H, A].

Lemma cfInd_vchar phi : phi \in 'Z[irr H] 'Ind[G] phi \in 'Z[irr G].

Lemma sub_conjC_vchar A phi :
  phi \in 'Z[irr G, A] phi - (phi^*)%CF \in 'Z[irr G, A^#].

Lemma Frobenius_kernel_exists :
  [Frobenius G with complement H] {K : {group gT} | [Frobenius G = K ><| H]}.

End MoreVchar.

Definition dirr (gT : finGroupType) (B : {set gT}) : pred_class :=
  [pred f : 'CF(B) | (f \in irr B) || (- f \in irr B)].
Implicit Arguments dirr [[gT]].

Section Norm1vchar.

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

Fact dirr_key : pred_key (dirr G).
Canonical dirr_keyed := KeyedPred dirr_key.

Fact dirr_oppr_closed : oppr_closed (dirr G).
Canonical dirr_opprPred := OpprPred dirr_oppr_closed.

Lemma dirr_opp v : (- v \in dirr G) = (v \in dirr G).
Lemma dirr_sign n v : ((-1)^+ n *: v \in dirr G) = (v \in dirr G).

Lemma irr_dirr i : 'chi_i \in dirr G.

Lemma dirrP f :
  reflect ( b : bool, i, f = (-1) ^+ b *: 'chi_i) (f \in dirr G).

This should perhaps be the definition of dirr.
Lemma dirrE phi : phi \in dirr G = (phi \in 'Z[irr G]) && ('[phi] == 1).

Lemma cfdot_dirr f g : f \in dirr G g \in dirr G
  '[f, g] = (if f == - g then -1 else (f == g)%:R).

Lemma dirr_norm1 phi : phi \in 'Z[irr G] '[phi] = 1 phi \in dirr G.

Lemma dirr_aut u phi : (cfAut u phi \in dirr G) = (phi \in dirr G).

Definition dIirr (B : {set gT}) := (bool × (Iirr B))%type.

Definition dirr1 (B : {set gT}) : dIirr B := (false, 0).

Definition ndirr (B : {set gT}) (i : dIirr B) : dIirr B :=
  (~~ i.1, i.2).

Lemma ndirr_diff (i : dIirr G) : ndirr i != i.

Lemma ndirrK : involutive (@ndirr G).

Lemma ndirr_inj : injective (@ndirr G).

Definition dchi (B : {set gT}) (i : dIirr B) : 'CF(B) :=
  (-1)^+ i.1 *: 'chi_i.2.

Lemma dchi1 : dchi (dirr1 G) = 1.

Lemma dirr_dchi i : dchi i \in dirr G.

Lemma dIrrP phi : reflect ( i, phi = dchi i) (phi \in dirr G).

Lemma dchi_ndirrE (i : dIirr G) : dchi (ndirr i) = - dchi i.

Lemma cfdot_dchi (i j : dIirr G) :
  '[dchi i, dchi j] = (i == j)%:R - (i == ndirr j)%:R.

Lemma dchi_vchar i : dchi i \in 'Z[irr G].

Lemma cfnorm_dchi (i : dIirr G) : '[dchi i] = 1.

Lemma dirr_inj : injective (@dchi G).

Definition dirr_dIirr (B : {set gT}) J (f : J 'CF(B)) j : dIirr B :=
  odflt (dirr1 B) [pick i | dchi i == f j].

Lemma dirr_dIirrPE J (f : J 'CF(G)) (P : pred J) :
    ( j, P j f j \in dirr G)
   j, P j dchi (dirr_dIirr f j) = f j.

Lemma dirr_dIirrE J (f : J 'CF(G)) :
  ( j, f j \in dirr G) j, dchi (dirr_dIirr f j) = f j.

Definition dirr_constt (B : {set gT}) (phi: 'CF(B)) : {set (dIirr B)} :=
  [set i | 0 < '[phi, dchi i]].

Lemma dirr_consttE (phi : 'CF(G)) (i : dIirr G) :
  (i \in dirr_constt phi) = (0 < '[phi, dchi i]).

Lemma Cnat_dirr (phi : 'CF(G)) i :
  phi \in 'Z[irr G] i \in dirr_constt phi '[phi, dchi i] \in Cnat.

Lemma dirr_constt_oppr (i : dIirr G) (phi : 'CF(G)) :
  (i \in dirr_constt (-phi)) = (ndirr i \in dirr_constt phi).

Lemma dirr_constt_oppI (phi: 'CF(G)) :
   dirr_constt phi :&: dirr_constt (-phi) = set0.

Lemma dirr_constt_oppl (phi: 'CF(G)) i :
  i \in dirr_constt phi (ndirr i) \notin dirr_constt phi.

Definition to_dirr (B : {set gT}) (phi : 'CF(B)) (i : Iirr B) : dIirr B :=
  ('[phi, 'chi_i] < 0, i).

Definition of_irr (B : {set gT}) (i : dIirr B) : Iirr B := i.2.

Lemma irr_constt_to_dirr (phi: 'CF(G)) i : phi \in 'Z[irr G]
  (i \in irr_constt phi) = (to_dirr phi i \in dirr_constt phi).

Lemma to_dirrK (phi: 'CF(G)) : cancel (to_dirr phi) (@of_irr G).

Lemma of_irrK (phi: 'CF(G)) :
  {in dirr_constt phi, cancel (@of_irr G) (to_dirr phi)}.

Lemma cfdot_todirrE (phi: 'CF(G)) i (phi_i := dchi (to_dirr phi i)) :
  '[phi, phi_i] *: phi_i = '[phi, 'chi_i] *: 'chi_i.

Lemma cfun_sum_dconstt (phi : 'CF(G)) :
  phi \in 'Z[irr G]
  phi = \sum_(i in dirr_constt phi) '[phi, dchi i] *: dchi i.
GG -- rewrite pattern fails in trunk move=> PiZ; rewrite [X in X = _ ]cfun_sum_constt.