Library mathcomp.character.vcharacter

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

From HB Require Import structures.
From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path.
From mathcomp Require Import div choice fintype tuple finfun bigop prime order.
From mathcomp Require Import ssralg poly finset fingroup morphism perm.
From mathcomp Require Import automorphism quotient finalg action gproduct.
From mathcomp Require Import zmodp commutator cyclic center pgroup sylow.
From mathcomp Require Import frobenius vector ssrnum ssrint archimedean intdiv.
From mathcomp Require Import algC algnum classfun character integral_char.

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.

Set Implicit Arguments.

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

Section Basics.

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

Definition Zchar : {pred 'CF(B)} :=
[pred phi in 'CF(B, A) | dec_Cint_span (in_tuple S) phi].

Lemma cfun0_zchar : 0 \in Zchar.

Fact Zchar_zmod : zmod_closed Zchar.

Lemma scale_zchar a phi : a \in Num.int 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.
A pure seq version with the extra hypothesis of S's unicity.
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 Num.nat.

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.

Lemma cnorm_dconstt (phi : 'CF(G)) :
phi \in 'Z[irr G]
'[phi] = \sum_(i in dirr_constt phi) '[phi, dchi i] ^+ 2.

Lemma dirr_small_norm (phi : 'CF(G)) n :
phi \in 'Z[irr G] '[phi] = n%:R (n < 4)%N
[/\ #|dirr_constt phi| = n, dirr_constt phi :&: dirr_constt (- phi) = set0 &
phi = \sum_(i in dirr_constt phi) dchi i].

Lemma cfdot_sum_dchi (phi1 phi2 : 'CF(G)) :
'[\sum_(i in dirr_constt phi1) dchi i,
\sum_(i in dirr_constt phi2) dchi i] =
#|dirr_constt phi1 :&: dirr_constt phi2|%:R -
#|dirr_constt phi1 :&: dirr_constt (- phi2)|%:R.

Lemma cfdot_dirr_eq1 :
{in dirr G &, phi psi, ('[phi, psi] == 1) = (phi == psi)}.