proposition: Lemma FTtype1_seqInd_facts chi : chi \in calS -> [/\ chi = \sum_(i in S_ chi) 'chi_i, constant [seq 'chi_i 1%g | i in S_ chi] & {in S_ chi, forall i, 'chi_i \in 'CF(L, 1%g |: 'A(L))}].
proof: Proof. move=> calS_chi; have [t nz_t Dchi] := seqIndC1P calS_chi. pose T := 'I_L['chi_t]%g. have sTL: T \subset L by apply: Inertia_sub. have sHT: H \subset T by apply/sub_Inertia/gFsub. have sHL: H \subset L by apply: normal_sub. have hallH: Hall T H := pHall_Hall (pHall_subl sHT sTL (Fcore_Hall L)). have [U [LtypeF _]] := FTtypeP _ maxL Ltype1. have [[_ _ sdHU] [U1 inertU1] _] := LtypeF. have defT: H ><| 'I_U['chi_t] = T := sdprod_modl sdHU (sub_inertia 'chi_t). have abTbar : abelian (T / H). have [_ _ /(_ _ _ inertU1 nz_t)sItU1] := typeF_context LtypeF. by rewrite -(isog_abelian (sdprod_isog defT)) (abelianS sItU1); case: inertU1. have [DtL _ X_1] := cfInd_Hall_central_Inertia nsHL abTbar hallH. have Dchi_sum : chi = \sum_(i in S_ chi) 'chi_i. by rewrite {1}Dchi DtL -Dchi; apply: eq_bigl => i; rewrite !inE. have lichi : constant [seq 'chi_i 1%g | i in S_ chi]. pose c := #|L : T|%:R * 'chi_t 1%g; apply: (@all_pred1_constant _ c). by apply/allP=> _ /imageP[s tLs ->] /=; rewrite inE Dchi in tLs; rewrite X_1. split=> // j Schi_j /=; apply/cfun_onP=> y A'y. have [Ly | /cfun0->//] := boolP (y \in L). have CHy1: 'C_H[y] = 1%g. apply: contraNeq A'y => /trivgPn[z /setIP[Hz cyz] ntz]. rewrite !inE -implyNb; apply/implyP=> nty; apply/bigcupP. rewrite FTsupp1_type1 Ltype1 //=; exists z; first by rewrite !inE ntz. by rewrite 3!inE nty Ly cent1C. have: j \in calX by apply/FTtype1_irrP; exists chi. by rewrite !inE => /andP[/irr_reg_off_ker_0->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg 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 mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)