(Joint Center)Library MathComp.integral_char

(* (c) Copyright Microsoft Corporation and Inria.                       
 You may distribute this file under the terms of the CeCILL-B license *)

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg poly finset.
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
Require Import commutator cyclic center pgroup sylow gseries nilpotent abelian.
Require Import ssrnum ssrint polydiv rat matrix mxalgebra intdiv mxpoly.
Require Import vector falgebra fieldext separable galois algC cyclotomic algnum.
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 cadinal 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 QnalgC}
         & nuQn : argumentType (mem ('Gal({:Qn}%VS / 1%VS))),
              {nu : {rmorphism algCalgC} |
                 {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).

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

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 characterchi x \in Aint.

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

Local Notation R_G := (group_ring algCfield G).
Local Notation a := gring_classM_coef.

This is Isaacs (2.25).
This is Isaacs, Theorem (3.7).
A more usable reformulation that does not involve the class sums.
Corollary Aint_class_div_irr1 x :
  x \in G#|x ^: G|%:R × 'chi_i x / 'chi_i 1%g \in Aint.

This is Isaacs, Theorem (3.8).
Theorem coprime_degree_support_cfcenter g :
    coprime (truncC ('chi_i 1%g)) #|g ^: G|g \notin ('Z('chi_i))%CF
  'chi_i g = 0.

End GringIrrMode.

This is Isaacs, Theorem (3.9).
Theorem primes_class_simple_gt1 C :
  simple G~~ abelian GC \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)%Nsolvable 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 j1g2 \in enum_val j2g \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 Gchi \is a characterchi \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]_ip.-nat (truncC ('chi_i 1%g)) →
    p.-Sylow(G) Pabelian 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.