(Joint Center)Library PFsection14

This file covers Peterfalvi, Section 14: Non_existence of G. It completes the proof of the Odd Order theorem.

Set Implicit Arguments.

Import GroupScope GRing.Theory FinRing.Theory Num.Theory.

Section Fourteen.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types (p q : nat) (x y z : gT).
Implicit Types H K L N P Q R S T U W : {group gT}.

Local Notation "#1" := (inord 1) (at level 0).

Variables S T U V W W1 W2 : {group gT}.
Hypotheses (defW : W1 \x W2 = W) (defW21 : W2 \x W1 = W).
Hypotheses (pairST : typeP_pair S T defW) (maxS : S \in 'M) (maxT : T \in 'M).
Hypotheses (StypeP : of_typeP S U defW) (TtypeP : of_typeP T V defW21).

Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope.
Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope.
Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope.
Local Notation What := (cyclicTIset defW).

Local Notation "` 'S'" := (gval S) (at level 0, only parsing) : group_scope.
Local Notation P := `S`_\F%G.
Local Notation "` 'P'" := `S`_\F (at level 0) : group_scope.
Local Notation PU := S^`(1)%G.
Local Notation "` 'PU'" := `S^`(1) (at level 0) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.

Local Notation "` 'T'" := (gval T) (at level 0, only parsing) : group_scope.
Local Notation Q := `T`_\F%G.
Local Notation "` 'Q'" := `T`_\F (at level 0) : group_scope.
Local Notation QV := T^`(1)%G.
Local Notation "` 'QV'" := `T^`(1) (at level 0) : group_scope.
Local Notation "` 'V'" := (gval V) (at level 0, only parsing) : group_scope.

Let defS : PU ><| W1 = S.
Let defPU : P ><| U = PU.

Let defT : QV ><| W2 = T.
Let defQV : Q ><| V = QV.

Let notStype1 : FTtype S != 1%N.
Let notStype5 : FTtype S != 5%N.

Let pddS := FT_prDade_hypF maxS StypeP.
Let ptiWS : primeTI_hypothesis S PU defW := FT_primeTI_hyp StypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddS.

Let pddT := FT_prDade_hypF maxT TtypeP.
Let ptiWT : primeTI_hypothesis T QV defW21 := FT_primeTI_hyp TtypeP.

Let ntW1 : W1 :!=: 1.
Let ntW2 : W2 :!=: 1.
Let cycW1 : cyclic W1.
Let cycW2 : cyclic W2.

Let p := #|W2|.
Let q := #|W1|.
Let u := #|U|.
Let v := #|V|.
Let nU := (p ^ q).-1 %/ p.-1.
Let nV := (q ^ p).-1 %/ q.-1.

Let pr_p : prime p.
Let pr_q : prime q.

Local Open Scope ring_scope.

This is Hypothesis (14.1).
Hypothesis ltqp: (q < p)%N.

This corresponds to Peterfalvi, Theorem (14.2). As we import the conclusion of BGappendixC, which covers Appendix C of the Bender and Glauberman text, we can state this theorem negatively. This will avoid having to repeat its statement thoughout the proof : we will simply end each nested set of assumptions (corresponding to (14.3) and (14.10)) with a contradiction.

Theorem no_full_FT_Galois_structure :
 ¬ [/\ (*a*) Fpq : finFieldImage P W2 U,
               [/\ #|P| = (p ^ q)%N, #|U| = nU & coprime nU p.-1]
    & (*b*) [/\ q.-abelem Q, W2 \subset 'N(Q)
              & exists2 y, y \in Q & W2 :^ y \subset 'N(U)]].

Let qgt2 : (q > 2)%N.
Let pgt2 : (p > 2)%N.

Let coPUq : coprime #|PU| q.

Let nirrW1 : #|Iirr W1| = q.
Let nirrW2 : #|Iirr W2| = p.
Let NirrW1 : Nirr W1 = q.
Let NirrW2 : Nirr W2 = p.

Let sigma := (cyclicTIiso ctiWG).
Let w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).

Local Notation Imu2 := (primeTI_Iirr ptiWS).
Let mu2_ i j := primeTIirr ptiWS i j.
Let mu_ := primeTIred ptiWS.
Local Notation chi_ j := (primeTIres ptiWS j).

Local Notation Inu2 := (primeTI_Iirr ptiWT).
Let nu2_ i j := primeTIirr ptiWT j i.
Let nu_ := primeTIred ptiWT.

Local Notation tauS := (FT_Dade0 maxS).
Local Notation tauT := (FT_Dade0 maxT).

Let calS0 := seqIndD PU S S`_\s 1.
Let rmR_S := FTtypeP_coh_base maxS StypeP.
Let scohS0 : subcoherent calS0 tauS rmR_S.

Let calS := seqIndD PU S P 1.
Let sSS0 : cfConjC_subset calS calS0.

Let calT := seqIndD QV T Q 1.

Justification for Hypothesis (14.3).
Fact FTtypeP_max_typeII : FTtype S == 2.
Local Notation Stype2 := FTtypeP_max_typeII.

These correspond to Peterfalvi, Hypothesis (14.3).
Variables (L : {group gT}) (tau1L : {additive 'CF(L)'CF(G)}) (phi : 'CF(L)).
Local Notation "` 'L'" := (gval L) (at level 0, only parsing).
Local Notation H := `L`_\F%G.
Local Notation "` 'H'" := `L`_\F%g (at level 0, format "` 'H'") : group_scope.

Hypothesis maxNU_L : L \in 'M('N(U)).

Consequences of the above.
Hypotheses (maxL : L \in 'M) (sNUL : 'N(U) \subset L).
Hypotheses (frobL : [Frobenius L with kernel H]) (Ltype1 : FTtype L == 1%N).

Let calL := seqIndD H L H 1.
Local Notation tauL := (FT_Dade maxL).

Hypothesis cohL : coherent_with calL L^# tauL tau1L.
Hypothesis irrL : {subset calL <= irr L}.
Hypotheses (Lphi : phi \in calL) (phi1 : phi 1%g = #|L : H|%:R).
Let irr_phi : phi \in irr L. Proof. exact: irrL. Qed.
This is the first assertion of Peterfalvi (14.4).
This is the second assertion of Peterfalvi (14.4).
Let oV : v = nV.

This is Peterfalvi (14.5).
Let defL : exists2 y, y \in Q & H ><| (W1 <*> W2 :^ y) = L.

This is Peterfalvi (14.6).
This is Peterfalvi (14.7).
This is Peterfalvi (14.8)(a). In order to avoid the use of real analysis and logarithms we bound the binomial expansion of n.+1 ^ q.+1 directly.
Let qp1_gt_pq1 : (q ^ p.+1 > p ^ q.+1)%N.

This is Peterfalvi (14.8)(b).
This is Peterfalvi (14.9).
Lemma FTtypeP_min_typeII : FTtype T == 2.
Local Notation Ttype2 := FTtypeP_min_typeII.

These declarations correspond to Hypothesis (14.10).
Variables (M : {group gT}) (tau1M : {additive 'CF(M)'CF(G)}) (psi : 'CF(M)).
Local Notation "` 'M'" := (gval M) (at level 0, only parsing).
Local Notation K := `M`_\F%G.
Local Notation "` 'K'" := `M`_\F%g (at level 0, format "` 'K'") : group_scope.

Hypothesis maxNV_M : M \in 'M('N(V)).

Consequences of the above.
Hypotheses (maxM : M \in 'M) (sNVM : 'N(V) \subset M).
Hypotheses (frobM : [Frobenius M with kernel K]) (Mtype1 : FTtype M == 1%N).

Let calM := seqIndD K M K 1.
Local Notation tauM := (FT_Dade maxM).

Hypothesis cohM : coherent_with calM M^# tauM tau1M.
Hypotheses (Mpsi : psi \in calM) (psi1 : psi 1%g = #|M : K|%:R).

Let betaM := 'Ind[M, K] 1 - psi.

Let pairTS : typeP_pair T S defW21.

Let FTsupp_res_core R nFR (maxR : R \in 'M) :
  let ddRF := restr_Dade_hyp (FT_Dade_hyp maxR) (Fcore_sub_FTsupp maxR) nFR in
  FTtype R == 1%NDade_support ddRF = 'A1~(R).

Let FTtype1_Dade_supp1 R : R \in 'MFTtype R == 1%N'A1~(R) = 'A~(R).

This is the first (and main) part of Peterfalvi (14.11).
Let defK : `K = V.

This is the first part of Peterfalvi (14.11).
Let indexMK: #|M : K| = (p × q)%N.

This is Peterfalvi (14.12), and also (14.13) since we have already proved the negation of Theorem (14.2).
Let not_MG_L : (L : {set gT}) \notin M :^: G.

Let pq : algC := (p × q)%:R.
Let h := #|H|.

This is Peterfalvi (14.14).
This is Peterfalvi (14.15).
Let oU : u = nU.

This is Peterfalvi (14.16), the last step towards the final contradiction.