proposition: Theorem invariant_chief_irr_cases G K L s (theta := 'chi[K]_s) : chief_factor G L K -> abelian (K / L) -> G \subset 'I[theta] -> let t := #|K : L| in [\/ 'Res[L] theta \in irr L, exists2 e, exists p, 'Res[L] theta = e%:R *: 'chi_p & (e ^ 2)%N = t | exists2 p, injective p & 'Res[L] theta = \sum_(i < t) 'chi_(p i)].
proof: Proof. case/andP=> /maxgroupP[/andP[ltLK nLG] maxL] nsKG abKbar IGtheta t. have [sKG nKG] := andP nsKG; have sLG := subset_trans (proper_sub ltLK) sKG. have nsLG: L <| G by apply/andP. have nsLK := normalS (proper_sub ltLK) sKG nsLG; have [sLK nLK] := andP nsLK. have [p0 sLp0] := constt_cfRes_irr L s; rewrite -/theta in sLp0. pose phi := 'chi_p0; pose T := 'I_G[phi]. have sTG: T \subset G := subsetIl G _. have /eqP mulKT: (K * T)%g == G. rewrite eqEcard mulG_subG sKG sTG -LagrangeMr -indexgI -(Lagrange sTG) /= -/T. rewrite mulnC leq_mul // setIA (setIidPl sKG) -!size_cfclass // -/phi. rewrite uniq_leq_size ?cfclass_uniq // => _ /cfclassP[x Gx ->]. have: conjg_Iirr p0 x \in irr_constt ('Res theta). have /inertiaJ <-: x \in 'I[theta] := subsetP IGtheta x Gx. by rewrite -(cfConjgRes _ nsKG) // irr_consttE conjg_IirrE // cfConjg_iso. apply: contraR; rewrite -conjg_IirrE // => not_sLp0x. rewrite (Clifford_Res_sum_cfclass nsLK sLp0) cfdotZl cfdot_suml. rewrite big1_seq ?mulr0 // => _ /cfclassP[y Ky ->]; rewrite -conjg_IirrE //. rewrite cfdot_irr mulrb ifN_eq ?(contraNneq _ not_sLp0x) // => <-. by rewrite conjg_IirrE //; apply/cfclassP; exists y. have nsKT_G: K :&: T <| G. rewrite /normal subIset ?sKG // -mulKT setIA (setIidPl sKG) mulG_subG. rewrite normsIG // sub_der1_norm ?subsetIl //. exact: subset_trans (der1_min nLK abKbar) (sub_Inertia _ sLK). have [e DthL]: exists e, 'Res theta = e%:R *: \sum_(xi <- (phi ^: K)%CF) xi. rewrite (Clifford_Res_sum_cfclass nsLK sLp0) -/phi; set e := '[_, _]. exists (Num.trunc e). by rewrite truncK ?Cnat_cfdot_char ?cfRes_char ?irr_char. have [defKT | ltKT_K] := eqVneq (K :&: T) K; last first. have defKT: K :&: T = L. apply: maxL; last by rewrite subsetI sLK sub_Inertia. by rewrite normal_norm // properEneq ltKT_K subsetIl. have t_cast: size (phi ^: K)%CF = t. by rewrite size_cfclass //= -{2}(setIidPl sKG) -setIA defKT. pose phiKt := Tuple (introT eqP t_cast); pose p i := cfIirr (tnth phiKt i). have pK i: 'chi_(p i) = (phi ^: K)%CF`_i. rewrite cfIirrE; first by rewrite (tnth_nth 0). by have /cfclassP[y _ ->] := mem_tnth i phiKt; rewrite cfConjg_irr ?mem_irr. constructor 3; exists p => [i j /(congr1 (tnth (irr L)))/eqP| ]. by apply: contraTeq; rewrite !pK !nth_uniq ?t_cast ?cfclass_uniq. have{} DthL: 'Res theta = e%:R *: \sum_(i < t) (phi ^: K)%CF`_i. by rewrite DthL (big_nth 0) big_mkord t_cast. suffices /eqP e1: e == 1 by rewrite DthL e1 scale1r; apply: eq_bigr. have Dth1: theta 1%g = e%:R * t%:R * phi 1%g. rewrite -[t]card_ord -mulrA -(cfRes1 L) DthL cfunE; congr (_ * _). rewrite mulr_natl -sumr_const sum_cfunE -t_cast; apply: eq_bigr => i _. by have /cfclassP[y _ ->] := mem_nth 0 (valP i); rewrite cfConjg1. rewrite eqn_leq lt0n (contraNneq _ (irr1_neq0 s)); last first. by rewrite Dth1 => ->; rewrite !mul0r. rewrite -leC_nat -(ler_pM2r (gt0CiG K L)) -/t -(ler_pM2r (irr1_gt0 p0)). rewrite mul1r -Dth1 -cfInd1 //. by rewrite char1_ge_constt ?cfInd_char ?irr_char ?constt_Ind_Res. have IKphi: 'I_K[phi] = K by rewrite -{1}(setIidPl sKG) -setIA. have{} DthL: 'Res[L] theta = e%:R *: phi. by rewrite DthL -[rhs in (_ ^: rhs)%CF]IKphi cfclass_inertia big_seq1. pose mmLth := @mul_mod_Iirr K L s. have linKbar := char_abelianP _ abKbar. have LmodL i: ('chi_i %% L)%CF \is a linear_char := cfMod_lin_char (linKbar i). have mmLthE i: 'chi_(mmLth i) = ('chi_i %% L)%CF * theta. by rewrite cfIirrE ?mod_IirrE // mul_lin_irr ?mem_irr. have mmLthL i: 'Res[L] 'chi_(mmLth i) = 'Res[L] theta. rewrite mmLthE rmorphM /= cfRes_sub_ker ?cfker_mod ?lin_char1 //. by rewrite scale1r mul1r. have [inj_Mphi | /injectivePn[i [j i'j eq_mm_ij]]] := boolP (injectiveb mmLth). suffices /eqP e1: e == 1 by constructor 1; rewrite DthL e1 scale1r mem_irr. rewrite eqn_leq lt0n (contraNneq _ (irr1_neq0 s)); last first. by rewrite -(cfRes1 L) DthL cfunE => ->; rewrite !mul0r. rewrite -leq_sqr -leC_nat natrX -(ler_pM2r (irr1_gt0 p0)) -mulrA mul1r. have ->: e%:R * 'chi_p0 1%g = 'Res[L] theta 1%g by rewrite DthL cfunE. rewrite cfRes1 -(ler_pM2l (gt0CiG K L)) -cfInd1 // -/phi. rewrite -card_quotient // -card_Iirr_abelian // mulr_natl. rewrite ['Ind phi]cfun_sum_cfdot sum_cfunE (bigID [in codom mmLth]) /=. rewrite ler_wpDr ?sumr_ge0 // => [i _|]. by rewrite char1_ge0 ?rpredZ_nat ?Cnat_cfdot_char ?cfInd_char ?irr_char. rewrite -big_uniq //= big_image -sumr_const ler_sum // => i _. rewrite cfunE -[in leRHS](cfRes1 L) -cfdot_Res_r mmLthL cfRes1. by rewrite DthL cfdotZr rmorph_nat cfnorm_irr mulr1. constructor 2; exists e; first by exists p0. pose mu := (('chi_i / 'chi_j)%R %% L)%CF; pose U := cfker mu. have lin_mu: mu \is a linear_char by rewrite cfMod_lin_char ?rpred_div. have Uj := lin_char_unitr (linKbar j). have ltUK: U \proper K. rewrite /proper cfker_sub /U; have /irrP[k Dmu] := lin_char_irr lin_mu. rewrite Dmu subGcfker -irr_eq1 -Dmu cfMod_eq1 //. by rewrite (can2_eq (divrK Uj) (mulrK Uj)) mul1r (inj_eq irr_inj). suffices: theta \in 'CF(K, L). rewrite -cfnorm_Res_leif // DthL cfnormZ !cfnorm_irr !mulr1 normr_nat. by rewrite -natrX eqC_nat => /eqP. have <-: gcore U G = L. apply: maxL; last by rewrite sub_gcore ?cfker_mod. by rewrite gcore_norm (sub_proper_trans (gcore_sub _ _)). apply/cfun_onP=> x; apply: contraNeq => nz_th_x. apply/bigcapP=> y /(subsetP IGtheta)/setIdP[nKy /eqP th_y]. apply: contraR nz_th_x; rewrite mem_conjg -{}th_y cfConjgE {nKy}//. move: {x y}(x ^ _) => x U'x; have [Kx | /cfun0-> //] := boolP (x \in K). have /eqP := congr1 (fun k => (('chi_j %% L)%CF^-1 * 'chi_k) x) eq_mm_ij. rewrite -rmorphV // !mmLthE !mulrA -!rmorphM mulVr // rmorph1 !cfunE. rewrite (mulrC _^-1) -/mu -subr_eq0 -mulrBl cfun1E Kx mulf_eq0 => /orP[]//. rewrite mulrb subr_eq0 -(lin_char1 lin_mu) [_ == _](contraNF _ U'x) //. by rewrite /U cfkerEchar ?lin_charW // inE Kx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype div tuple finfun bigop prime order) mathcomp(ssralg ssrnum finset fingroup morphism perm) mathcomp(automorphism quotient action zmodp cyclic center) mathcomp(gproduct commutator gseries nilpotent pgroup) mathcomp(sylow maximal frobenius matrix mxalgebra) mathcomp(mxrepresentation vector algC classfun character) mathcomp(archimedean)