Library mathcomp.character.integral_char

(* (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 action countalg finalg zmodp.
From mathcomp Require Import commutator cyclic center pgroup sylow gseries.
From mathcomp Require Import nilpotent abelian ssrnum ssrint archimedean polydiv.
From mathcomp Require Import rat 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 [in 'Gal({:Qn} / 1)],
              {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).

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.

End GenericClassSums.

Canonical gring_irr_mode_unlockable := Unlockable gring_irr_mode.unlock.
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).
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.

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

This is Isaacs (2.25).
Lemma mx_irr_gring_op_center_scalar n (rG : mx_representation algCfield G n) A :
  mx_irreducible rG → (A \in 'Z(R_G))%MS → is_scalar_mx (gring_op rG A).

Section GringIrrMode.

Variable i : Iirr G.

Let n := irr_degree (socle_of_Iirr i).
Let mxZn_inj: injective (@scalar_mx algCfield n).

Lemma cfRepr_gring_center n1 (rG : mx_representation algCfield G n1) A :
  cfRepr rG = 'chi_i → (A \in 'Z(R_G))%MS → gring_op rG A = 'omega_i[A]%:M.

Lemma irr_gring_center A :
  (A \in 'Z(R_G))%MS → gring_op 'Chi_i A = 'omega_i[A]%:M.

Lemma gring_irr_modeM A B :
    (A \in 'Z(R_G))%MS → (B \in 'Z(R_G))%MS →
  'omega_i[A ×m B] = 'omega_i[A] × 'omega_i[B].

Lemma gring_mode_class_sum_eq (k : 'I_#|classes G|) g :
  g \in enum_val k → 'omega_i['K_k] = #|g ^: G|%:R × 'chi_i g / 'chi_i 1%g.

This is Isaacs, Theorem (3.7).
Lemma Aint_gring_mode_class_sum k : 'omega_i['K_k] \in Aint.

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 (Num.trunc ('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 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 (Num.trunc ('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.