- -

Library mathcomp.character.integral_char

- -

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

- -

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