+ +

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). +
+
+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 (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 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.
+
+