Library mathcomp.character.integral_char
(* (c) Copyright 2006-2015 Microsoft Corporation and Inria.
Distributed under the terms of CeCILL-B. *)
Require Import mathcomp.ssreflect.ssreflect.
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.
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.
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).
A more usable reformulation that does not involve the class sums.
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.
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.
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)).
This is Isaacs, Theorem (3.11).
This is Isaacs, Theorem (3.12).
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.
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.
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.
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.
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)).