(Joint Center)Library PFsection6

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg poly finset center.
Require Import fingroup morphism perm automorphism quotient action zmodp.
Require Import gfunctor gproduct cyclic pgroup commutator gseries nilpotent.
Require Import sylow abelian maximal hall frobenius.
Require Import matrix mxalgebra mxrepresentation vector ssrnum algC algnum.
Require Import classfun character inertia vcharacter integral_char.
Require Import PFsection1 PFsection2 PFsection3 PFsection4 PFsection5.

This file covers Peterfalvi, Section 6: Some Coherence Theorems Defined here: odd_Frobenius_quotient K L M <-> L has odd order, M <| L, K with K / M is nilpotent, and L / H1 is a Frobenius group with kernel K / H1, where H1 / M = (K / M)^(1). This is the statement of Peterfalvi, Hypothesis (6.4), except for the K <| L and subcoherence assumptions, to be required separately.

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.
Local Open Scope ring_scope.

The main section
Section Six.

Variables (gT : finGroupType) (G : {group gT}).
Implicit Types H K L M : {group gT}.

Grouping lemmas that assume Hypothesis (6.1).
Section GeneralCoherence.

Variables K L : {group gT}.
Local Notation S M := (seqIndD K L K M).
Local Notation calS := (S 1).

Variables (R : 'CF(L)seq 'CF(G)) (tau : {linear 'CF(L)'CF(G)}).

These may need to be grouped, in order to make the proofs of 6.8, 10.10, and 12.6 more manageable.
Hypotheses (nsKL : K <| L) (solK : solvable K).
Hypothesis Itau : {in 'Z[calS, L^#] &, isometry tau}.
Hypothesis scohS : subcoherent calS tau R.

Let sKL : K \subset L.
Let nKL : L \subset 'N(K).
Let orthS: pairwise_orthogonal calS.
Let sSS M : {subset S M calS}.
Let ccS M : conjC_closed (S M).
Let uniqS M : uniq (S M).
Let nrS : ~~ has cfReal calS.

Lemma exists_linInd M :
  M \proper KM <| Kexists2 phi, phi \in S M & phi 1%g = #|L : K|%:R.

This is Peterfalvi (6.2).
Lemma coherent_seqIndD_bound (A B C D : {group gT}) :
        [/\ A <| L, B <| L, C <| L & D <| L]
  (*a*) [/\ A \proper K, B \subset D, D \subset C, C \subset K
          & D / B \subset 'Z(C / B)]%g
  (*b1*) coherent (S A) L^# tau
  (*b2*) coherent (S B) L^# tau
   #|K : A|%:R - 1 2%:R × #|L : C|%:R × sqrtC #|C : D|%:R.

This is Peterfalvi, Theorem (6.3).
Theorem bounded_seqIndD_coherent M H H1 :
   [/\ M <| L, H <| L & H1 <| L]
   [/\ M \subset H1, H1 \subset H & H \subset K]
 (*a*) nilpotent (H / M)%g
 (*b*) coherent (S H1) L^# tau
 (*c*) (#|H : H1| > 4 × #|L : K| ^ 2 + 1)%N
 coherent (S M) L^# tau.

This is the statement of Peterfalvi, Hypothesis (6.4).
Definition odd_Frobenius_quotient M (H1 := K^`(1) <*> M) :=
  [/\ (*a*) odd #|L|,
      (*b*) [/\ M <| L, M \subset K & nilpotent (K / M)]
    & (*c*) [Frobenius L / H1 with kernel K / H1] ]%g.

This is Peterfalvi (6.5).
Lemma non_coherent_chief M (H1 := (K^`(1) <*> M)%G) :
   odd_Frobenius_quotient M
   coherent (S M) L^# tau
[/\ (*a*) chief_factor L H1 K (#|K : H1| 4 × #|L : K| ^ 2 + 1)%N
     & (*b*) exists2 p : nat, p.-group (K / M)%g ~~ abelian (K / M)%g
     & (*c*) ~~ (#|L : K| %| p - 1)].

This is Peterfalvi (6.6).
Lemma seqIndD_irr_coherence (Z : {group gT}) (calX := seqIndD K L Z 1) :
    odd_Frobenius_quotient 1%G
    [/\ Z <| L, Z :!=: 1 & Z \subset 'Z(K)]%g
    {subset calX irr L}
  calX =i [pred chi in irr L | ~~ (Z \subset cfker chi)]
   coherent calX L^#tau.

End GeneralCoherence.

This is Peterfalvi (6.7). In (6.8) we only know initially the P is Sylow in L; perhaps the lemma should be stated with this equivalent (but weaker) assumption.
Lemma constant_irr_mod_TI_Sylow (Z L P : {group gT}) p i :
     p.-Sylow(G) Podd #|L|normedTI P^# G L
     [/\ Z <| L, Z :!=: 1%g & Z \subset 'Z(P)]
     {in Z^# &, x y, #|'C_L[x]| = #|'C_L[y]| }
     let phi := 'chi[G]_i in
     {in Z^# &, x y, phi x = phi y}
   {in Z^#, x, phi x \in Cint (#|P| %| phi x - phi 1%g)%C}.

This is Peterfalvi, Theorem (6.8). We omit the semi-direct structure of L in assumption (a), since it is implied by our statement of assumption (c).
Theorem Sibley_coherence (L H W1 : {group gT}) :
  (*a*) [/\ odd #|L|, nilpotent H & normedTI H^# G L]
  (*b*) let calS := seqIndD H L H 1 in let tau := 'Ind[G, L] in
  (*c*) [\/ (*c1*) [Frobenius L = H ><| W1]
         | (*c2*) exists2 W2 : {group gT}, prime #|W2| W2 \subset H^`(1)%G
               & A0, W : {group gT}, defW : W1 \x W2 = W,
                 prime_Dade_hypothesis G L H H H^# A0 defW]
  coherent calS L^# tau.

End Six.