proposition: Lemma seqIndD_irr_coherence Z (calX := seqIndD K L Z 1) : odd_Frobenius_quotient 1 -> [/\ Z <| L, Z :!=: 1 & Z \subset 'Z(K)]%g -> {subset calX <= irr L} -> calX =i [pred chi in irr L | ~~ (Z \subset cfker chi)] /\ coherent calX L^#tau.
proof: Proof. move=> Frob_quo1 [nsZL ntZ sZ_ZK] irrX; have [sZL nZL] := andP nsZL. have abZ: abelian Z by rewrite (abelianS sZ_ZK) ?center_abelian. have /andP[sZK nZK]: Z <| K := sub_center_normal sZ_ZK. split=> [chi|]. apply/idP/andP=> [Xchi | [/irrP[r ->{chi}] nkerZr]]. rewrite irrX //; case/seqIndP: Xchi => t /setIdP[nkerZt _] ->. by rewrite inE in nkerZt; rewrite sub_cfker_Ind_irr. have [t Res_r_t] := neq0_has_constt (Res_irr_neq0 K r). pose chi := 'Ind[L] 'chi_t; have chi_r: '[chi, 'chi_r] != 0. by rewrite -cfdot_Res_r cfdotC fmorph_eq0 -irr_consttE. have Xchi: chi \in calX. apply/seqIndP; exists t; rewrite // !inE sub1G andbT. rewrite -(sub_cfker_Ind_irr t sKL nZL). apply: contra nkerZr => /subset_trans-> //. by rewrite cfker_constt // cfInd_char ?irr_char //. case/irrX/irrP: Xchi chi_r (Xchi) => r' ->. by rewrite cfdot_irr pnatr_eq0 -lt0n; case: eqP => // ->. apply: non_coherent_chief (subset_coherent (seqInd_sub sZK)) _ => //= -[_ [p]]. have [oddL _] := Frob_quo1; rewrite joingG1 -/calX => frobLb []. rewrite -(isog_pgroup p (quotient1_isog K)) => pK ab'K. set e := #|L : K| => not_e_dv_p1; have e_gt0: (e > 0)%N by apply: indexg_gt0. have ntK: K != 1%G by apply: contraNneq ab'K => ->; rewrite quotient1 abelian1. have{ab'K ntK} [p_pr p_dv_K _] := pgroup_pdiv pK ntK. set Y := calX; pose d (xi : 'CF(L)) := logn p (truncC (xi 1%g) %/ e). have: cfConjC_closed Y by apply: cfAut_seqInd. have: perm_eq (Y ++ [::]) calX by rewrite cats0. have: {in Y & [::], forall xi1 xi2, d xi1 <= d xi2}%N by []. elim: {Y}_.+1 {-2}Y [::] (ltnSn (size Y)) => // m IHm Y X' leYm leYX' defX ccY. have sYX: {subset Y <= calX}. by move=> xi Yxi; rewrite -(perm_mem defX) mem_cat Yxi. have sX'X: {subset X' <= calX}. by move=> xi X'xi; rewrite -(perm_mem defX) mem_cat X'xi orbT. have uniqY: uniq Y. have: uniq calX := seqInd_uniq L _. by rewrite -(perm_uniq defX) cat_uniq => /and3P[]. have sYS: {subset Y <= calS} by move=> xi /sYX/seqInd_sub->. case homoY: (constant [seq xi 1%g | xi : 'CF(L) <- Y]). exact: uniform_degree_coherence (subset_subcoherent scohS _) homoY. have Ndg: {in calX, forall xi : 'CF(L), xi 1%g = (e * p ^ d xi)%:R}. rewrite /d => _ /seqIndP[i _ ->]; rewrite cfInd1 // -/e. have:= dvd_irr1_cardG i; have /CnatP[n ->] := Cnat_irr1 i. rewrite -natrM natCK dvdC_nat mulKn // -p_part => dv_n_K. by rewrite part_pnat_id // (pnat_dvd dv_n_K). have [chi Ychi leYchi]: {chi | chi \in Y & {in Y, forall xi, d xi <= d chi}%N}. have [/eqP/nilP Y0 | ntY] := posnP (size Y); first by rewrite Y0 in homoY. pose i := [arg max_(i > Ordinal ntY) d Y`_i]. exists Y`_i; first exact: mem_nth. rewrite {}/i; case: fintype.arg_maxnP => //= i _ max_i. by move=> _ /(nthP 0)[j ltj <-]; apply: (max_i (Ordinal ltj)). have{homoY} /hasP[xi1 Yxi1 lt_xi1_chi]: has (fun xi => d xi < d chi)%N Y. apply: contraFT homoY => geYchi; apply: (@all_pred1_constant _ (chi 1%g)). rewrite all_map; apply/allP=> xi Yxi; rewrite /= !Ndg ?sYX // eqr_nat. rewrite eqn_pmul2l // eqn_exp2l ?prime_gt1 //. by rewrite eqn_leq leYchi //= leqNgt (hasPn geYchi). pose Y' := rem chi^*%CF (rem chi Y); pose X'' := [:: chi, chi^*%CF & X']. have ccY': cfConjC_closed Y'. move=> xi; rewrite !(inE, mem_rem_uniq) ?rem_uniq //. by rewrite !(inv_eq (@cfConjCK _ _)) cfConjCK => /and3P[-> -> /ccY->]. have Xchi := sYX _ Ychi; have defY: perm_eq [:: chi, chi^*%CF & Y'] Y. rewrite (permPr (perm_to_rem Ychi)) perm_cons perm_sym perm_to_rem //. by rewrite mem_rem_uniq ?inE ?ccY // (seqInd_conjC_neq _ _ _ Xchi). apply: perm_coherent (defY) _. have d_chic: d chi^*%CF = d chi. by rewrite /d cfunE/= conj_Cnat // (Cnat_seqInd1 Xchi). have /and3P[uniqY' Y'xi1 notY'chi]: [&& uniq Y', xi1 \in Y' & chi \notin Y']. rewrite !(inE, mem_rem_uniq) ?rem_uniq // Yxi1 eqxx andbF !andbT -negb_or. by apply: contraL lt_xi1_chi => /pred2P[] ->; rewrite ?d_chic ltnn. have sY'Y: {subset Y' <= Y} by move=> xi /mem_rem/mem_rem. have sccY'S: cfConjC_subset Y' calS by split=> // xi /sY'Y/sYS. apply: (extend_coherent scohS _ Y'xi1); rewrite ?sYS {sccY'S notY'chi}//. have{} defX: perm_eq (Y' ++ X'') calX. by rewrite (perm_catCA Y' [::_; _]) catA -(permPr defX) perm_cat2r. have{d_chic} le_chi_X'': {in X'', forall xi, d chi <= d xi}%N. by move=> xi /or3P[/eqP-> | /eqP-> | /leYX'->] //; rewrite d_chic. rewrite !Ndg ?sYX // dvdC_nat dvdn_pmul2l // dvdn_exp2l 1?ltnW //; split=> //. apply: IHm defX ccY' => [|xi xi' /sY'Y/leYchi-le_xi_chi /le_chi_X'']. by rewrite -ltnS // (leq_trans _ leYm) // -(perm_size defY) ltnW. exact: leq_trans. have p_gt0 n: (0 < p ^ n)%N by rewrite expn_gt0 prime_gt0. rewrite -!natrM; apply: (lt_le_trans (y := (e ^ 2 * (p ^ d chi) ^ 2)%:R)). rewrite ltr_nat -expnMn -mulnn mulnAC !mulnA 2?ltn_pmul2r //. rewrite -mulnA mulnCA ltn_pmul2l // -(subnK lt_xi1_chi) addnS expnS. rewrite expnD mulnA ltn_pmul2r // -(muln1 3%N) leq_mul //. rewrite ltn_neqAle prime_gt1 // eq_sym (sameP eqP (prime_oddPn p_pr)). by rewrite (dvdn_odd p_dv_K) // (oddSg sKL). have [r] := seqIndP (sYX _ Ychi); rewrite !inE => /andP[nkerZr _] def_chi. have d_r: 'chi_r 1%g = (p ^ d chi)%:R. by apply: (mulfI (neq0CiG L K)); rewrite -cfInd1 // -def_chi -natrM Ndg. pose sum_p2d S := (\sum_(xi <- S) p ^ (d xi * 2))%N. pose sum_xi1 (S : seq 'CF(L)) := \sum_(xi <- S) xi 1%g ^+ 2 / '[xi]. have def_sum_xi1 S: {subset S <= calX} -> sum_xi1 S = (e ^ 2 * sum_p2d S)%:R. move=> sSX; rewrite big_distrr natr_sum /=; apply: eq_big_seq => xi /sSX Xxi. rewrite expnM -expnMn natrX -Ndg //. by have /irrP[i ->] := irrX _ Xxi; rewrite cfnorm_irr divr1. rewrite -/(sum_xi1 _) def_sum_xi1 ?leC_nat 1?dvdn_leq => [|||_ /sY'Y/sYX] //. by rewrite muln_gt0 expn_gt0 e_gt0 [_ Y'](bigD1_seq xi1) //= addn_gt0 p_gt0. have coep: coprime e p. have:= Frobenius_ker_coprime frobLb; rewrite coprime_sym. have /andP[_ nK'L]: K^`(1) <| L by apply: gFnormal_trans. rewrite index_quotient_eq ?subIset ?der_sub ?orbT {nK'L}// -/e. have ntKb: (K / K^`(1))%g != 1%g by case/Frobenius_kerP: frobLb. have [_ _ [k ->]] := pgroup_pdiv (quotient_pgroup _ pK) ntKb. by rewrite coprime_pexpr. rewrite -expnM Gauss_dvd ?coprimeXl ?coprimeXr {coep}// dvdn_mulr //=. have /dvdn_addl <-: p ^ (d chi * 2) %| e ^ 2 * sum_p2d X''. rewrite big_distrr big_seq dvdn_sum //= => xi /le_chi_X'' le_chi_xi. by rewrite dvdn_mull // dvdn_exp2l ?leq_pmul2r. rewrite -mulnDr -big_cat (perm_big _ defX) -(natCK (e ^ 2 * _)) /=. rewrite -def_sum_xi1 // /sum_xi1 sum_seqIndD_square ?normal1 ?sub1G //. rewrite indexg1 -(natrB _ (cardG_gt0 Z)) -natrM natCK. rewrite -(Lagrange_index sKL sZK) mulnAC dvdn_mull //. have /p_natP[k defKZ]: p.-nat #|K : Z| by rewrite (pnat_dvd (dvdn_indexg K Z)). rewrite defKZ dvdn_exp2l // -(leq_exp2l _ _ (prime_gt1 p_pr)) -{k}defKZ. rewrite -leC_nat expnM natrX -d_r ?(le_trans (irr1_bound r).1) //. rewrite ler_nat dvdn_leq ?indexgS ?(subset_trans sZ_ZK) //=. by rewrite -cap_cfcenter_irr bigcap_inf. 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator gseries nilpotent) mathcomp(sylow abelian maximal hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC algnum) mathcomp(classfun character inertia vcharacter integral_char) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)