proposition: Lemma FTtypeII_prime_facts M U W W1 W2 (defW : W1 \x W2 = W) (maxM : M \in 'M) : of_typeP M U defW -> FTtype 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].
proof: Proof. move=> MtypeP Mtype2 H HU calS tau p q. have Mnot5: FTtype M != 5 by rewrite (eqP Mtype2). have [_ cUU _ _ _] := compl_of_typeII maxM MtypeP Mtype2. have [q_pr p_pr]: prime q /\ prime p := FTtypeP_primes maxM MtypeP. have:= typeII_IV_core maxM MtypeP Mnot5; rewrite Mtype2 -/p -/q => [[_ oH]]. have [] := Ptype_Fcore_kernel_exists maxM MtypeP Mnot5. have [_ _] := Ptype_Fcore_factor_facts maxM MtypeP Mnot5. rewrite -/H; set H0 := Ptype_Fcore_kernel _; set Hbar := (H / H0)%G. rewrite def_Ptype_factor_prime // -/p -/q => oHbar chiefHbar _. have trivH0: H0 :=: 1%g. have [/maxgroupp/andP[/andP[sH0H _] nH0M] /andP[sHM _]] := andP chiefHbar. apply: card1_trivg; rewrite -(setIidPr sH0H) -divg_index. by rewrite -card_quotient ?(subset_trans sHM) // oHbar -oH divnn cardG_gt0. have abelHbar: p.-abelem Hbar. have pHbar: p.-group Hbar by rewrite /pgroup oHbar pnatX pnat_id. by rewrite -is_abelem_pgroup // (sol_chief_abelem _ chiefHbar) ?mmax_sol. rewrite /= trivH0 -(isog_abelem (quotient1_isog _)) in abelHbar. have:= Ptype_core_coherence maxM MtypeP Mnot5; rewrite trivH0. set C := _ MtypeP; have sCU: C \subset U by rewrite [C]unlock subsetIl. by rewrite (derG1P (abelianS sCU cUU)) [(1 <*> 1)%G]join1G. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)