(Joint Center)Library PFsection11

This file covers Peterfalvi, Section 11: Maximal subgroups of Types III and IV.

Set Implicit Arguments.

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

Section Eleven.

This is Peterfalvi (11.1).
Lemma lbound_expn_odd_prime p q :
   odd podd qprime pprime qp != q → 4 × q ^ 2 + 1 < p ^ q.

Local Open Scope ring_scope.

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

Variables M U W W1 W2 : {group gT}.
Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP : of_typeP M U defW).
Hypothesis Mtypen2 : FTtype M != 2.

Let Mtypen5 : FTtype M != 5.
Let Mtypen1 : FTtype M != 1%N.
Let Mtype_gt2 : (FTtype M > 2)%N.
Let Mtype34 : FTtype M \in pred2 3 4.

Local Notation H0 := (Ptype_Fcore_kernel MtypeP).
Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope.
Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope.
Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope.
Local Notation "` 'W'" := (gval W) (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 H := `M`_\F%G.
Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope.
Local Notation HU := M^`(1)%G.
Local Notation "` 'HU'" := `M^`(1) (at level 0) : group_scope.
Local Notation U' := U^`(1)%G.
Local Notation "` 'U''" := `U^`(1) (at level 0) : group_scope.
Local Notation C := 'C_U(`H)%G.
Local Notation "` 'C'" := 'C_`U(`H) (at level 0) : group_scope.
Local Notation HC := (`H <*> `C)%G.
Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope.
Local Notation H0C := (`H0 <*> `C)%G.
Local Notation "` 'H0C'" := (gval H0 <*> `C) (at level 0) : group_scope.

Let Mtype24 := compl_of_typeII_IV maxM MtypeP Mtypen5.

Let p := #|W2|.
Let pr_p : prime p.

Let q := #|W1|.
Let pr_q : prime q.

Let nsHUM : HU <| M := der_normal _ _.

Let defM : HU ><| W1 = M.
Let defHU : H ><| U = HU.

Let chiefH0 : chief_factor M H0 H.

Let defMs : M`_\s = HU.

Notation S_ := (seqIndD HU M HU).

Local Notation tau := (FT_Dade0 maxM).
Local Notation R := (FTtypeP_coh_base maxM MtypeP).

Let subc_M : subcoherent (S_ 1) tau R.

Let sH0H : H0 \subset H.

Let nsH0H : H0 <| H.

Let nsCM : C <| M.

Let defHC : H \x C = HC.

Let defH0C : H0 \x C = H0C.

Let normal_hyps : [/\ 1 <| M, HC <| M & H0C <| M].

This is Peterfalvi (11.3).
Lemma ncoH0C : ¬ coherent (S_ H0C) M^# tau.

Let minHbar : minnormal (H / H0)%g (M / H0)%g.

Let pabHbar : p.-abelem (H / H0)%g.

This is Peterfalvi (11.4).
Lemma bounded_proper_coherent H1 :
  H1 <| MH1 \proper HUcoherent (S_ H1) M^# tau
    (#|HU : H1| 2 × q × #|U : C| + 1)%N.

This is Peterfalvi (11.5).
Lemma derM2_HC : (M^`(2) = HC)%g.

This is Peterfalvi (11.6).
This is Peterfalvi (11.7). We revert to the proof of the original Odd Order paper, using the fact that H / Q is extra special in the typeP_Galois case.
Lemma FTtype34_Fcore_kernel_trivial :
  [/\ p.-abelem H, #|H| = (p ^ q)%N & `H0 = 1%g].

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

Local Notation sigma := (cyclicTIiso ctiWG).
Local Notation w_ i j := (cyclicTIirr defW i j).
Local Notation eta_ i j := (sigma (w_ i j)).
Local Notation mu_ := (primeTIred ptiWM).
Local Notation Idelta := (primeTI_Isign ptiWM).
Local Notation delta_ j := (primeTIsign ptiWM j).
Local Notation d := (FTtype345_TIirr_degree MtypeP).
Local Notation n := (FTtype345_ratio MtypeP).
Local Notation delta := (FTtype345_TIsign MtypeP).

Let mu2_ i j := primeTIirr ptiWM i j.

Let codom_sigma := map sigma (irr W).
Let ntW1 : (W1 :!=: 1)%g.
Let ntW2 : (W2 :!=: 1)%g.

Let sHHU : H \subset HU.
Let sUHU : U \subset HU.
Let sHC_HU : (HC \subset HU)%g.
Let sHUM : HU \subset M.
Let nsHC_HU : HC <| HU.
Let nsCU : C <| U.

Let frobMbar : [Frobenius M / HC = (HU / HC) ><| (W1 / HC)].

Let cW1 : cyclic W1.
Let nirrW1 : #|Iirr W1| = q.
Let NirrW1 : Nirr W1 = q.

Let cW2 : cyclic W2.
Let nirrW2 : #|Iirr W2| = p.
Let NirrW2 : Nirr W2 = p.

Lemma Ptype_Fcompl_kernel_cent : Ptype_Fcompl_kernel MtypeP :=: C.

Let AUC : abelian (U / C).

Let SHC1 : {in S_ HC, xi : 'CF(M), xi 1%g = q%:R}.

Let sub_co_SHC_tau : subcoherent (S_ HC) tau R.
Let co_SHC_tau : coherent (S_ HC) M^# tau.

Let defA1 : 'A1(M) = HU^#.
Let defA : 'A(M) = HU^#.
Notation V := (class_support (cyclicTIset defW) M).
Let defA0 : 'A0(M) = HU^# :|: V.

Let SHC_irr : {subset (S_ HC) irr M}.

Let cfdot_SHC : {in S_ HC &, phi psi, '[phi, psi] = (phi == psi)%:R}.

Let omu2 i j (z : 'CF(M)) (SHCz : z \in S_ HC) : '[mu2_ i j, z] = 0.

Let omu j (z : 'CF(M)) (SHCz : z \in S_ HC) : '[mu_ j, z] = 0.

Let cf_mu0Bz (z : 'CF(M)) (SHCz : z \in S_ HC) : mu_ 0 - z \in 'CF(M, 'A0(M)).

This is 11.8.4
Let ex_co_w_SHC_tau (z : 'CF(_)) (SHCz : z \in S_ HC) :
 orthogonal (tau (mu_ 0 - z) - \sum_i eta_ i 0) codom_sigma
 exists2 tau1, coherent_with (S_ HC) M^# tau tau1 &
               tau (mu_ 0 - z) = \sum_i eta_ i 0 - tau1 z.

Let SC := seqIndD HU M HC C.
Let SHCdSC : {subset S_ HC [predC SC]}.

Let Smu := [seq mu_ j | j in predC1 0].
Let Smu_nirr : {subset Smu [predC irr M]}.

Let S1nirr := filter [predC irr M] (seqIndD HU M H H0).
Let S1nirr_i_Smu : S1nirr =i Smu.

Let u := #|(U/C)%g|.
Let mu1 j (nz_j : j != 0) : mu_ j 1%g = (q × u)%:R.

Let Smu_i_SCnirr : Smu =i filter [predC irr M] SC.

Notation "#1" := (inord 1).

Let coUq : coprime #|U| q.

Let nC_UW1 : U <*> W1 \subset 'N(C).

Let FrobUW1QC : [Frobenius U <*> W1 / C = (U / C) ><| (W1 / C)].

This is PF (11.8).
Lemma FTtype34_not_ortho_cycTIiso (z : 'CF(_)) (SHCz : z \in S_ HC) :
  ~~ orthogonal (tau (mu_ 0 - z) - \sum_i eta_ i 0) codom_sigma.

Implicit Types r : {rmorphism algCalgC}.

This is PF (11.9).
Lemma FTtype34_structure :
  [/\ (*a*) {in S_ HC, z : 'CF(M),
             orthogonal (tau (mu_ 0 - z) - \sum_j eta_ 0 j) codom_sigma},
      (*b*) (p < q)%N
    & (*c*) FTtype M == 3 typeP_Galois MtypeP].

End Eleven.