proposition: Theorem extend_linear_char_from_Sylow G N (lambda : 'CF(N)) : N <| G -> lambda \is a linear_char -> G \subset 'I[lambda] -> (forall p, p \in \pi('o(lambda)%CF) -> exists2 Hp : {group gT}, [/\ N \subset Hp, Hp \subset G & p.-Sylow(G / N) (Hp / N)%g] & exists u, 'Res 'chi[Hp]_u = lambda) -> exists u, 'Res[N, G] 'chi_u = lambda.
proof: Proof. set m := 'o(lambda)%CF => nsNG lam_lin IGlam p_ext_lam. have [sNG nNG] := andP nsNG; have linN := @cfRes_lin_lin _ _ N. wlog [p p_lam]: lambda @m lam_lin IGlam p_ext_lam / exists p : nat, \pi(m) =i (p : nat_pred). - move=> IHp; have [linG [cf [inj_cf _ lin_cf onto_cf]]] := lin_char_group N. case=> cf1 cfM cfX _ cf_order; have [lam cf_lam] := onto_cf _ lam_lin. pose mu p := cf lam.`_p; pose pi_m p := p \in \pi(m). have Dm: m = #[lam] by rewrite /m cfDet_order_lin // cf_lam cf_order. have Dlambda: lambda = \prod_(p < m.+1 | pi_m p) mu p. rewrite -(big_morph cf cfM cf1) big_mkcond cf_lam /pi_m Dm; congr (cf _). rewrite -{1}[lam]prod_constt big_mkord; apply: eq_bigr => p _. by case: ifPn => // p'lam; apply/constt1P; rewrite /p_elt p'natEpi. have lin_mu p: mu p \is a linear_char by rewrite /mu cfX -cf_lam rpredX. suffices /fin_all_exists [u uNlam] (p : 'I_m.+1): exists u, pi_m p -> 'Res[N, G] 'chi_u = mu p. - pose nu := \prod_(p < m.+1 | pi_m p) 'chi_(u p). have lin_nu: nu \is a linear_char. by apply: rpred_prod => p m_p; rewrite linN ?irr_char ?uNlam. have /irrP[u1 Dnu] := lin_char_irr lin_nu. by exists u1; rewrite Dlambda -Dnu rmorph_prod; apply: eq_bigr. have [m_p | _] := boolP (pi_m p); last by exists 0. have o_mu: \pi('o(mu p)%CF) =i (p : nat_pred). rewrite cfDet_order_lin // cf_order orderE /=. have [|pr_p _ [k ->]] := pgroup_pdiv (p_elt_constt p lam). by rewrite cycle_eq1 (sameP eqP constt1P) /p_elt p'natEpi // negbK -Dm. by move=> q; rewrite pi_of_exp // pi_of_prime. have IGmu: G \subset 'I[mu p]. rewrite (subset_trans IGlam) // /mu cfX -cf_lam. elim: (chinese _ _ _ _) => [|k IHk]; first by rewrite inertia1 norm_inertia. by rewrite exprS (subset_trans _ (inertia_mul _ _)) // subsetIidl. have [q||u] := IHp _ (lin_mu p) IGmu; [ | by exists p | by exists u]. rewrite o_mu => /eqnP-> {q}. have [Hp sylHp [u uNlam]] := p_ext_lam p m_p; exists Hp => //. rewrite /mu cfX -cf_lam -uNlam -rmorphXn /=; set nu := _ ^+ _. have /lin_char_irr/irrP[v ->]: nu \is a linear_char; last by exists v. by rewrite rpredX // linN ?irr_char ?uNlam. have pi_m_p: p \in \pi(m) by rewrite p_lam !inE. have [pr_p mgt0]: prime p /\ (m > 0)%N. by have:= pi_m_p; rewrite mem_primes => /and3P[]. have p_m: p.-nat m by rewrite -(eq_pnat _ p_lam) pnat_pi. have{p_ext_lam} [H [sNH sHG sylHbar] [v vNlam]] := p_ext_lam p pi_m_p. have co_p_GH: coprime p #|G : H|. rewrite -(index_quotient_eq _ sHG nNG) ?subIset ?sNH ?orbT //. by rewrite (pnat_coprime (pnat_id pr_p)) //; have [] := and3P sylHbar. have lin_v: 'chi_v \is a linear_char by rewrite linN ?irr_char ?vNlam. pose nuG := 'Ind[G] 'chi_v. have [c vGc co_p_f]: exists2 c, c \in irr_constt nuG & ~~ (p %| 'chi_c 1%g)%C. apply/exists_inP; rewrite -negb_forall_in. apply: contraL co_p_GH => /forall_inP p_dv_v1. rewrite prime_coprime // negbK -dvdC_nat -[rhs in (_ %| rhs)%C]mulr1. rewrite -(lin_char1 lin_v) -cfInd1 // ['Ind _]cfun_sum_constt /=. rewrite sum_cfunE rpred_sum // => i /p_dv_v1 p_dv_chi1i. rewrite cfunE dvdC_mull // intr_nat //. by rewrite Cnat_cfdot_char ?cfInd_char ?irr_char. pose f := Num.trunc ('chi_c 1%g); pose b := (egcdn f m).1. have fK: f%:R = 'chi_c 1%g by rewrite truncK ?Cnat_irr1. have fb_mod_m: f * b = 1 %[mod m]. have co_m_f: coprime m f. by rewrite (pnat_coprime p_m) ?p'natE // -dvdC_nat CdivE fK. by rewrite -(chinese_modl co_m_f 1 0) /chinese !mul0n addn0 mul1n. have /irrP[s Dlam] := lin_char_irr lam_lin. have cHv: v \in irr_constt ('Res[H] 'chi_c) by rewrite -constt_Ind_Res. have{cHv} cNs: s \in irr_constt ('Res[N] 'chi_c). rewrite -(cfResRes _ sNH) ?(constt_Res_trans _ cHv) ?cfRes_char ?irr_char //. by rewrite vNlam Dlam constt_irr !inE. have DcN: 'Res[N] 'chi_c = lambda *+ f. have:= Clifford_Res_sum_cfclass nsNG cNs. rewrite cfclass_invariant -Dlam // big_seq1 Dlam => DcN. have:= cfRes1 N 'chi_c; rewrite DcN cfunE -Dlam lin_char1 // mulr1 => ->. by rewrite -scaler_nat fK. have /lin_char_irr/irrP[d Dd]: cfDet 'chi_c ^+ b \is a linear_char. by rewrite rpredX // cfDet_lin_char. exists d; rewrite -{}Dd rmorphXn /= -cfDetRes ?irr_char // DcN. rewrite cfDetMn ?lin_charW // -exprM cfDet_id //. rewrite -(expr_mod _ (exp_cforder _)) -cfDet_order_lin // -/m. by rewrite fb_mod_m /m cfDet_order_lin // expr_mod ?exp_cforder. 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)