Library mathcomp.character.integral_char

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

Require Import mathcomp.ssreflect.ssreflect.

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 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 coeficients 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.

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).
Lemma Aint_char (chi : 'CF(G)) x : chi \is a character chi x \in Aint.

Lemma Aint_irr i x : 'chi[G]_i x \in Aint.

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).
Theorem primes_class_simple_gt1 C :
  simple G ~~ abelian G C \in (classes G)^# (size (primes #|C|) > 1)%N.

End IntegralChar.

Section MoreIntegralChar.

Implicit Type gT : finGroupType.

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).
Theorem dvd_irr1_index_center gT (G : {group gT}) i :
  ('chi[G]_i 1%g %| #|G : 'Z('chi_i)%CF|)%C.

This is Isaacs, Problem (3.7).
Lemma gring_classM_coef_sum_eq gT (G : {group gT}) j1 j2 k g1 g2 g :
   let a := @gring_classM_coef gT G j1 j2 in let a_k := a k in
   g1 \in enum_val j1 g2 \in enum_val j2 g \in enum_val k
   let sum12g := \sum_i 'chi[G]_i g1 × 'chi_i g2 × ('chi_i g)^* / 'chi_i 1%g in
  a_k%:R = (#|enum_val j1| × #|enum_val j2|)%:R / #|G|%:R × sum12g.

This is Isaacs, Problem (2.16).
Lemma index_support_dvd_degree gT (G H : {group gT}) chi :
    H \subset G chi \is a character chi \in 'CF(G, H)
    (H :==: 1%g) || abelian G
  (#|G : H| %| chi 1%g)%C.

This is Isaacs, Theorem (3.13).
Theorem faithful_degree_p_part gT (p : nat) (G P : {group gT}) i :
    cfaithful 'chi[G]_i p.-nat (truncC ('chi_i 1%g))
    p.-Sylow(G) P abelian P
  'chi_i 1%g = (#|G : 'Z(G)|`_p)%:R.

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)).
Theorem nonlinear_irr_vanish gT (G : {group gT}) i :
  'chi[G]_i 1%g > 1 exists2 x, x \in G & 'chi_i x = 0.

End MoreIntegralChar.