proposition: Lemma typeF_context M U (H := M`_\F) : of_typeF M U -> [/\ forall U0, is_typeF_complement M U U0 -> #|U0| = exponent U, [Frobenius M = H ><| U] = Zgroup U & forall U1 (i : Iirr H), is_typeF_inertia M U U1 -> i != 0 -> 'I_U['chi_i] \subset U1].
proof: Proof. case; rewrite -/H => [[ntH ntM defM] _ exU0]; set part_a := forall U0, _. have [nsHM sUG mulHU nHU _] := sdprod_context defM. have oU0: part_a. move=> U0 [sU0U <- /Frobenius_reg_ker regU0]; rewrite exponent_Zgroup //. apply/forall_inP=> S /SylowP[p _ /and3P[sSU0 pS _]]. apply: odd_regular_pgroup_cyclic pS (mFT_odd S) ntH _ _. by rewrite (subset_trans (subset_trans sSU0 sU0U)). by move=> x /setD1P[ntx /(subsetP sSU0) U0x]; rewrite regU0 // !inE ntx. split=> // [|U1 i [nsU1U abU1 s_cUH_U1] nz_i]. apply/idP/idP=> [frobU | ZgU]. apply/forall_inP=> S /SylowP[p _ /and3P[sSU pS _]]. apply: odd_regular_pgroup_cyclic pS (mFT_odd S) ntH _ _. by rewrite (subset_trans sSU). move=> x /setD1P[ntx /(subsetP sSU) Ux]. by rewrite (Frobenius_reg_ker frobU) // !inE ntx. have [U0 [sU0U expU0 frobU0]] := exU0; have regU0 := Frobenius_reg_ker frobU0. suffices defU0: U0 :=: U by rewrite defU0 norm_joinEr ?mulHU // in frobU0. by apply/eqP; rewrite eqEcard sU0U /= (oU0 U0) // exponent_Zgroup. have itoP: is_action M (fun (j : Iirr H) x => conjg_Iirr j x). split=> [x | j x y Mx My]. apply: can_inj (fun j => conjg_Iirr j x^-1) _ => j. by apply: irr_inj; rewrite !conjg_IirrE cfConjgK. by apply: irr_inj; rewrite !conjg_IirrE (cfConjgM _ nsHM). pose ito := Action itoP; pose cto := ('Js \ subsetT M)%act. have actsMcH: [acts M, on classes H | cto]. apply/subsetP=> x Mx; rewrite !inE Mx; apply/subsetP=> _ /imsetP[y Hy ->]. have nHx: x \in 'N(H) by rewrite (subsetP (gFnorm _ _)). rewrite !inE /= -class_rcoset norm_rlcoset // class_lcoset mem_classes //. by rewrite memJ_norm. apply/subsetP=> g /setIP[Ug /setIdP[nHg c_i_g]]; have Mg := subsetP sUG g Ug. apply: contraR nz_i => notU1g; rewrite (sameP eqP set1P). suffices <-: 'Fix_ito[g] = [set 0 : Iirr H]. by rewrite !inE sub1set inE -(inj_eq (@irr_inj _ _)) conjg_IirrE. apply/eqP; rewrite eq_sym eqEcard cards1 !(inE, sub1set) /=. rewrite -(inj_eq (@irr_inj _ _)) conjg_IirrE irr0 cfConjg_cfun1 eqxx. rewrite (card_afix_irr_classes Mg actsMcH) => [|j y z Hy /=]; last first. case/imsetP=> _ /imsetP[t Ht ->] -> {z}. by rewrite conjg_IirrE cfConjgE // conjgK cfunJ. rewrite -(cards1 [1 gT]) subset_leq_card //= -/H. apply/subsetP=> _ /setIP[/imsetP[a Ha ->] /afix1P caHg]; rewrite inE classG_eq1. have{caHg} /imsetP[x Hgx cax]: a \in a ^: (H :* g). by rewrite class_rcoset caHg class_refl. have coHg: coprime #|H| #[g]. apply: (coprime_dvdr (order_dvdG Ug)). by rewrite (coprime_sdprod_Hall_l defM) (pHall_Hall (Fcore_Hall M)). have /imset2P[z y cHgg_z Hy defx]: x \in class_support ('C_H[g] :* g) H. have [/and3P[/eqP defUcHgg _ _] _] := partition_cent_rcoset nHg coHg. by rewrite class_supportEr -cover_imset defUcHgg. rewrite -(can_eq (conjgKV y)) conj1g; apply: contraR notU1g => nt_ay'. have{nt_ay'} Hay': a ^ y^-1 \in H^# by rewrite !inE nt_ay' groupJ ?groupV. rewrite (subsetP (s_cUH_U1 _ Hay')) // inE Ug. have ->: g = z.`_(\pi(H)^'). have [h /setIP[Hh /cent1P cgh] ->] := rcosetP cHgg_z. rewrite consttM // (constt1P _) ?mul1g ?constt_p_elt //. by rewrite /p_elt -coprime_pi' ?cardG_gt0. by rewrite (mem_p_elt _ Hh) // pgroupNK pgroup_pi. by rewrite groupX //= -conjg_set1 normJ mem_conjgV -defx !inE conjg_set1 -cax. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)