proposition: Theorem solvable_irr_extendible_from_det G N s (theta := 'chi[N]_s) : N <| G -> solvable (G / N) -> G \subset 'I[theta] -> coprime #|G : N| (Num.trunc (theta 1%g)) -> [exists c, 'Res 'chi[G]_c == theta] = [exists u, 'Res 'chi[G]_u == cfDet theta].
proof: Proof. set e := #|G : N|; set f := Num.trunc _ => nsNG solG IGtheta co_e_f. apply/exists_eqP/exists_eqP=> [[c cNth] | [u uNdth]]. have /lin_char_irr/irrP[u Du] := cfDet_lin_char 'chi_c. by exists u; rewrite -Du -cfDetRes ?irr_char ?cNth. move: {2}e.+1 (ltnSn e) => m. elim: m => // m IHm in G u e nsNG solG IGtheta co_e_f uNdth *. rewrite ltnS => le_e; have [sNG nNG] := andP nsNG. have [<- | ltNG] := eqsVneq N G; first by exists s; rewrite cfRes_id. have [G0 maxG0 sNG0]: {G0 | maxnormal (gval G0) G G & N \subset G0}. by apply: maxgroup_exists; rewrite properEneq ltNG sNG. have [/andP[ltG0G nG0G] maxG0_P] := maxgroupP maxG0. set mu := 'chi_u in uNdth; have lin_mu: mu \is a linear_char. by rewrite qualifE/= irr_char -(cfRes1 N) uNdth /= lin_char1 ?cfDet_lin_char. have sG0G := proper_sub ltG0G; have nsNG0 := normalS sNG0 sG0G nsNG. have nsG0G: G0 <| G by apply/andP. have /lin_char_irr/irrP[u0 Du0] := cfRes_lin_char G0 lin_mu. have u0Ndth: 'Res 'chi_u0 = cfDet theta by rewrite -Du0 cfResRes. have IG0theta: G0 \subset 'I[theta]. by rewrite (subset_trans sG0G) // -IGtheta subsetIr. have coG0f: coprime #|G0 : N| f by rewrite (coprime_dvdl _ co_e_f) ?indexSg. have{m IHm le_e} [c0 c0Ns]: exists c0, 'Res 'chi[G0]_c0 = theta. have solG0: solvable (G0 / N) := solvableS (quotientS N sG0G) solG. apply: IHm nsNG0 solG0 IG0theta coG0f u0Ndth (leq_trans _ le_e). by rewrite -(ltn_pmul2l (cardG_gt0 N)) !Lagrange ?proper_card. have{c0 c0Ns} [c0 [c0Ns dc0_u0] Uc0] := extend_to_cfdet nsNG0 coG0f c0Ns u0Ndth. have IGc0: G \subset 'I['chi_c0]. apply/subsetP=> x Gx; rewrite inE (subsetP nG0G) //= -conjg_IirrE. apply/eqP; congr 'chi__; apply: Uc0; rewrite conjg_IirrE. by rewrite -(cfConjgRes _ nsG0G nsNG) // c0Ns inertiaJ ?(subsetP IGtheta). by rewrite cfDetConjg dc0_u0 -Du0 (cfConjgRes _ _ nsG0G) // cfConjg_id. have prG0G: prime #|G : G0|. have [h injh im_h] := third_isom sNG0 nsNG nsG0G. rewrite -card_quotient // -im_h // card_injm //. rewrite simple_sol_prime 1?quotient_sol //. by rewrite /simple -(injm_minnormal injh) // im_h // maxnormal_minnormal. have [t tG0c0] := prime_invariant_irr_extendible nsG0G (erefl _) prG0G IGc0. by exists t; rewrite /theta -c0Ns -tG0c0 cfResRes. 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)