(Joint Center)Library PFsection10

This file covers Peterfalvi, Section 10: Maximal subgroups of Types III, IV and V. For defW : W1 \x W2 = W and MtypeP : of_typeP M U defW, and setting ptiW := FT_primeTI_hyp MtypeP, mu2_ i j := primeTIirr ptiW i j and delta_ j := primeTIsign j, we define here, for M of type III-V: FTtype345_TIirr_degree MtypeP == the common degree of the components of (locally) d the images of characters of irr W that don't have W2 in their kernel by the cyclicTI isometry to M. Thus mu2_ i j 1%g = d%:R for all j != 0. FTtype345_TIsign MtypeP == the common sign of the images of characters (locally) delta of characters of irr W that don't have W2 in their kernel by the cyclicTI isometry to M. Thus delta_ j = delta for all j != 0. FTtype345_ratio MtypeP == the ratio (d - delta) / #|W1|. Even though it (locally) n is always a positive integer we take n : algC. FTtype345_bridge MtypeP s i j == a virtual character that can be used to (locally) alpha_ i j bridge coherence between the mu2_ i j and other irreducibles of M; here s should be the index of an irreducible character of M induced from M^(1). := mu2_ i j - delta *: mu2_ i 0 -n *: 'chi_s.

Set Implicit Arguments.

Import GroupScope GRing.Theory Num.Theory.

Section Ten.

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

Section OneMaximal.

These assumptions correspond to Peterfalvi, Hypothesis (10.1). We also declare the group U_M, even though it is not used in this section, because it is a parameter to the theorems and definitions of PFsection8 and PFsection9.
Variables M U_M W W1 W2 : {group gT}.
Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W).
Hypotheses (MtypeP : of_typeP M U_M defW) (notMtype2: FTtype M != 2).

Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
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 V := (cyclicTIset defW).
Local Notation M' := M^`(1)%G.
Local Notation "` 'M''" := `M^`(1) (at level 0) : group_scope.
Local Notation M'' := M^`(2)%G.
Local Notation "` 'M'''" := `M^`(2) (at level 0) : group_scope.

Let defM : M' ><| W1 = M.
Let nsM''M' : M'' <| M'.
Let nsM'M : M' <| M.
Let sM'M : M' \subset M.
Let nsM''M : M'' <| M.

Let notMtype1 : FTtype M != 1%N.
Let typeMgt2 : FTtype M > 2.

Let defA1 : 'A1(M) = M'^#.
Let defA : 'A(M) = M'^#.
Let defA0 : 'A0(M) = M'^# :|: class_support V M.
Let defMs : M`_\s :=: M'.

Let pddM := FT_prDade_hyp maxM MtypeP.
Let ptiWM : primeTI_hypothesis M M' defW := FT_primeTI_hyp MtypeP.
Let ctiWG : cyclicTI_hypothesis G defW := pddM.
Let ctiWM : cyclicTI_hypothesis M defW := prime_cycTIhyp ptiWM.

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

Let w1 := #|W1|.
Let w2 := #|W2|.
Let nirrW1 : #|Iirr W1| = w1.
Let nirrW2 : #|Iirr W2| = w2.
Let NirrW1 : Nirr W1 = w1.
Let NirrW2 : Nirr W2 = w2.

Let w1gt2 : w1 > 2.
Let w2gt2 : w2 > 2.

Let coM'w1 : coprime #|M'| w1.

This is used both in (10.2) and (10.8).
Let frobMbar : [Frobenius M / M'' = (M' / M'') ><| (W1 / M'')].

Local Open Scope ring_scope.

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 ptiWM).
Let mu2_ i j := primeTIirr ptiWM i j.
Let mu_ := primeTIred ptiWM.
Local Notation chi_ j := (primeTIres ptiWM j).

Local Notation Idelta := (primeTI_Isign ptiWM).
Local Notation delta_ j := (primeTIsign ptiWM j).

Local Notation tau := (FT_Dade0 maxM).
Local Notation "chi ^\tau" := (tau chi).

Let calS0 := seqIndD M' M M`_\s 1.
Let rmR := FTtypeP_coh_base maxM MtypeP.
Let scohS0 : subcoherent calS0 tau rmR.

Let calS := seqIndD M' M M' 1.
Let sSS0 : cfConjC_subset calS calS0.

Let mem_calS s : ('Ind 'chi[M']_s \in calS) = (s != 0).

Let calSmu j : j != 0 → mu_ j \in calS.

Let tauM' : {subset 'Z[calS, M'^#] 'CF(M, 'A0(M))}.

This is Peterfalvi (10.2). Note that this result is also valid for type II groups.
This is Peterfalvi (10.3), first assertion.
Lemma FTtype345_core_prime : prime w2.
Let w2_pr := FTtype345_core_prime.

Definition FTtype345_TIirr_degree := truncC (mu2_ 0 #1 1%g).
Definition FTtype345_TIsign := delta_ #1.
Local Notation d := FTtype345_TIirr_degree.
Local Notation delta := FTtype345_TIsign.
Definition FTtype345_ratio := (d%:R - delta) / w1%:R.
Local Notation n := FTtype345_ratio.

This is the remainder of Peterfalvi (10.3).
Lemma FTtype345_constants :
  [/\ i j, j != 0 → mu2_ i j 1%g = d%:R,
       j, j != 0 → delta_ j = delta,
      (d > 1)%N
    & n \in Cnat].

Let o_mu2_irr zeta i j :
  zeta \in calSzeta \in irr M'[mu2_ i j, zeta] = 0.

Let ZmuBzeta zeta j :
    zeta \in calSzeta 1%g = w1%:Rj != 0 →
  mu_ j - d%:R *: zeta \in 'Z[calS, M'^#].

Let mu0Bzeta_on zeta :
  zeta \in calSzeta 1%g = w1%:Rmu_ 0 - zeta \in 'CF(M, 'A(M)).

We need to prove (10.5) - (10.7) for an arbitrary choice of zeta, to allow part of the proof of (10.5) to be reused in that of (11.8).
Variable i_zeta : Iirr M.
Local Notation zeta := 'chi_i_zeta.
Hypotheses (Szeta : zeta \in calS) (zeta1w1 : zeta 1%g = w1%:R).

Let o_mu2_zeta i j : '[mu2_ i j, zeta] = 0.

Let o_mu_zeta j : '[mu_ j, zeta] = 0.

Definition FTtype345_bridge i j := mu2_ i j - delta *: mu2_ i 0 - n *: zeta.
Local Notation alpha_ := FTtype345_bridge.

This is the first part of Peterfalvi (10.5), which does not depend on the coherence assumption that will ultimately be falsified on (10.8).
Lemma supp_FTtype345_bridge i j : j != 0 → alpha_ i j \in 'CF(M, 'A0(M)).
Local Notation alpha_on := supp_FTtype345_bridge.

Lemma vchar_FTtype345_bridge i j : alpha_ i j \in 'Z[irr M].
Local Notation Zalpha := vchar_FTtype345_bridge.
Local Hint Resolve Zalpha.

Lemma vchar_Dade_FTtype345_bridge i j :
  j != 0 → (alpha_ i j)^\tau \in 'Z[irr G].
Local Notation Zalpha_tau := vchar_Dade_FTtype345_bridge.

This covers the last paragraph in the proof of (10.5); it's isolated here because it is reused in the proof of (10.10) and (11.8).

Lemma norm_FTtype345_bridge i j :
  j != 0 → '[(alpha_ i j)^\tau] = 2%:R + n ^+ 2.
Local Notation norm_alpha := norm_FTtype345_bridge.

Implicit Type tau : {additive 'CF(M)'CF(G)}.

This exported version is adapted to its use in (11.8).
Lemma FTtype345_bridge_coherence calS1 tau1 i j X Y :
     coherent_with calS1 M^# tau tau1(alpha_ i j)^\tau = X + Y
     cfConjC_subset calS1 calS0{subset calS1 irr M}
     j != 0 → Y \in 'Z[map tau1 calS1]'[Y, X] = 0 → '[Y] = n ^+ 2 →
  X = delta *: (eta_ i j - eta_ i 0).

This is a specialization of the above, used in (10.5) and (10.10).
Let def_tau_alpha calS1 tau1 i j :
     coherent_with calS1 M^# tau tau1cfConjC_subset calS1 calS0
     j != 0 → zeta \in calS1'[(alpha_ i j)^\tau, tau1 zeta] = - n
  (alpha_ i j)^\tau = delta *: (eta_ i j - eta_ i 0) - n *: tau1 zeta.

Section NonCoherence.

We will ultimately contradict these assumptions. Note that we do not need to export any lemma save the final contradiction.
Variable tau1 : {additive 'CF(M)'CF(G)}.
Hypothesis cohS : coherent_with calS M^# tau tau1.

Local Notation "mu ^\tau1" := (tau1 mu%CF)
  (at level 2, format "mu ^\tau1") : ring_scope.

Let Dtau1 : {in 'Z[calS, M'^#], tau1 =1 tau}.

Let o_zeta_s: '[zeta, zeta^*] = 0.

Import ssrint rat.

This is the second part of Peterfalvi (10.5).
Let tau_alpha i j : j != 0 →
  (alpha_ i j)^\tau = delta *: (eta_ i j - eta_ i 0) - n *: zeta^\tau1.

This is the first part of Peterfalvi (10.6)(a).
Let tau1mu j : j != 0 → (mu_ j)^\tau1 = delta *: \sum_i eta_ i j.

This is the second part of Peterfalvi (10.6)(a).
Let tau1mu0 : (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - zeta^\tau1.

This is Peterfalvi (10.6)(b).
Let zeta_tau1_coprime g :
  g \notin 'A~(M)coprime #[g] w1`|zeta^\tau1 g| 1.

Let Frob_der1_type2 S :
  S \in 'MFTtype S == 2 → [Frobenius S^`(1) with kernel S`_\F].

This is the bulk of the proof of Peterfalvi (10.8); however the result will be restated below to avoid the quantification on zeta and tau1.
This is Peterfalvi (10.9).
Lemma FTtype345_Dade_bridge0 :
    (w1 < w2)%N
  {chi | [/\ (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - chi,
             chi \in 'Z[irr G], '[chi] = 1
           & i j, '[chi, eta_ i j] = 0]}.

Local Notation H := M'.
Local Notation "` 'H'" := `M' (at level 0) : group_scope.
Local Notation H' := M''.
Local Notation "` 'H''" := `M'' (at level 0) : group_scope.

This is the bulk of the proof of Peterfalvi, Theorem (10.10); as with (10.8), it will be restated below in order to remove dependencies on zeta, U_M and W1.
Lemma FTtype5_exclusion_main : FTtype M != 5.

End OneMaximal.

Implicit Type M : {group gT}.

This is the exported version of Peterfalvi, Theorem (10.8).
Theorem FTtype345_noncoherence M (M' := M^`(1)%G) (maxM : M \in 'M) :
  (FTtype M > 2)%N¬ coherent (seqIndD M' M M' 1) M^# (FT_Dade0 maxM).

This is the exported version of Peterfalvi, Theorem (10.10).
Theorem FTtype5_exclusion M : M \in 'MFTtype M != 5.

This the first assertion of Peterfalvi (10.11).
Lemma FTtypeP_pair_primes S T W W1 W2 (defW : W1 \x W2 = W) :
  typeP_pair S T defWprime #|W1| prime #|W2|.

Corollary FTtypeP_primes M U W W1 W2 (defW : W1 \x W2 = W) :
  M \in 'Mof_typeP M U defWprime #|W1| prime #|W2|.

This is the remainder of Peterfalvi (10.11).
Lemma FTtypeII_prime_facts M U W W1 W2 (defW : W1 \x W2 = W) (maxM : M \in 'M) :
    of_typeP M U defWFTtype M == 2 →
    let H := M`_\F%G in let HU := M^`(1)%G in
    let calS := seqIndD HU M H 1 in let tau := FT_Dade0 maxM in
    let p := #|W2| in let q := #|W1| in
  [/\ p.-abelem H, (#|H| = p ^ q)%N & coherent calS M^# tau].

End Ten.