Library mathcomp.character.integral_char

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

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 action finalg zmodp.
From mathcomp Require Import commutator cyclic center pgroup sylow gseries.
From mathcomp Require Import nilpotent abelian ssrnum ssrint polydiv rat.
From mathcomp Require Import matrix mxalgebra intdiv mxpoly vector falgebra.
From mathcomp Require Import fieldext separable galois algC cyclotomic algnum.
From mathcomp Require Import mxrepresentation classfun character.

This file provides some standard results based on integrality properties of characters, such as theorem asserting that the degree of an irreducible character of G divides the order of G (Isaacs 3.11), or the famous p^a.q^b solvability theorem of Burnside. Defined here: 'K_k == the kth class sum in gring F G, where k : 'I#|classes G|, and F is inferred from the context. := gset_mx F G (enum_val k) (see mxrepresentation.v). --> The 'K_k form a basis of 'Z(group_ring F G)%%MS. gring_classM_coef i j k == the coordinate of 'K_i *m 'K_j on 'K_k; this is usually abbreviated as a i j k. gring_classM_coef_set A B z == the set of all (x, y) in setX A B such that x * y = z; if A and B are respectively the ith and jth conjugacy class of G, and z is in the kth conjugacy class, then gring_classM_coef i j k is exactly the cardinal of this set. 'omega_i#A# == the mode of 'chi#G##i on (A \in 'Z(group_ring algC G))%MS, i.e., the z such that gring_op 'Chi_i A = z%:M.

Set Implicit Arguments.

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

Lemma group_num_field_exists (gT : finGroupType) (G : {group gT}) :
  {Qn : splittingFieldType rat & galois 1 {:Qn} &
    {QnC : {rmorphism Qn algC}
         & nuQn : argumentType (mem ('Gal({:Qn}%VS / 1%VS))),
              {nu : {rmorphism algC algC} |
                 {morph QnC: a / nuQn a >-> nu a}}
         & {w : Qn & #|G|.-primitive_root w <<1; w>>%VS = fullv
              & (hT : finGroupType) (H : {group hT}) (phi : 'CF(H)),
                       phi \is a character
                        x, (#[x] %| #|G|)%N {a | QnC a = phi x}}}}.

Section GenericClassSums.

This is Isaacs, Theorem (2.4), generalized to an arbitrary field, and with the combinatorial definition of the coefficients exposed. This part could move to mxrepresentation.

Variable (gT : finGroupType) (G : {group gT}) (F : fieldType).

Definition gring_classM_coef_set (Ki Kj : {set gT}) g :=
  [set xy in [predX Ki & Kj] | let: (x, y) := xy in x × y == g]%g.

Definition gring_classM_coef (i j k : 'I_#|classes G|) :=
  #|gring_classM_coef_set (enum_val i) (enum_val j) (repr (enum_val k))|.

Definition gring_class_sum (i : 'I_#|classes G|) := gset_mx F G (enum_val i).


Lemma gring_class_sum_central i : ('K_i \in 'Z(group_ring F G))%MS.

Lemma set_gring_classM_coef (i j k : 'I_#|classes G|) g :
    g \in enum_val k
  a i j k = #|gring_classM_coef_set (enum_val i) (enum_val j) g|.

Theorem gring_classM_expansion i j : 'K_i ×m 'K_j = \sum_k (a i j k)%:R *: 'K_k.

Fact gring_irr_mode_key : unit.
Definition gring_irr_mode_def (i : Iirr G) := ('chi_i 1%g)^-1 *: 'chi_i.
Definition gring_irr_mode := locked_with gring_irr_mode_key gring_irr_mode_def.
Canonical gring_irr_mode_unlockable := [unlockable fun gring_irr_mode].

End GenericClassSums.

Arguments gring_irr_mode {gT G%G} i%R _%g : extra scopes.

Notation "''K_' i" := (gring_class_sum _ i)
  (at level 8, i at level 2, format "''K_' i") : ring_scope.

Notation "''omega_' i [ A ]" := (xcfun (gring_irr_mode i) A)
   (at level 8, i at level 2, format "''omega_' i [ A ]") : ring_scope.

Section IntegralChar.

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

This is Isaacs, Corollary (3.6).
This is Isaacs (2.25).
This is Isaacs, Theorem (3.7).
A more usable reformulation that does not involve the class sums.
This is Isaacs, Theorem (3.8).
This is Isaacs, Theorem (3.9).
This is Burnside's famous p^a.q^b theorem (Isaacs, Theorem (3.10)).
Theorem Burnside_p_a_q_b gT (G : {group gT}) :
  (size (primes #|G|) 2)%N solvable G.

This is Isaacs, Theorem (3.11).
Theorem dvd_irr1_cardG gT (G : {group gT}) i : ('chi[G]_i 1%g %| #|G|)%C.

This is Isaacs, Theorem (3.12).
This is Isaacs, Problem (3.7).
This is Isaacs, Problem (2.16).
This is Isaacs, Theorem (3.13).
This is Isaacs, Lemma (3.14). Note that the assumption that G be cyclic is unnecessary, as S will be empty if this is not the case.
Lemma sum_norm2_char_generators gT (G : {group gT}) (chi : 'CF(G)) :
    let S := [pred s | generator G s] in
    chi \is a character {in S, s, chi s != 0}
  \sum_(s in S) `|chi s| ^+ 2 #|S|%:R.

This is Burnside's vanishing theorem (Isaacs, Theorem (3.15)).