proposition: Lemma extend_to_cfdet G N s c0 u : let theta := 'chi_s in let lambda := cfDet theta in let mu := 'chi_u in N <| G -> coprime #|G : N| (Num.trunc (theta 1%g)) -> 'Res[N, G] 'chi_c0 = theta -> 'Res[N, G] mu = lambda -> exists2 c, 'Res 'chi_c = theta /\ cfDet 'chi_c = mu & forall c1, 'Res 'chi_c1 = theta -> cfDet 'chi_c1 = mu -> c1 = c.
proof: Proof. move=> theta lambda mu nsNG; set e := #|G : N|; set f := Num.trunc _. set eta := 'chi_c0 => co_e_f etaNth muNlam; have [sNG nNG] := andP nsNG. have fE: f%:R = theta 1%g by rewrite truncK ?Cnat_irr1. pose nu := cfDet eta; have lin_nu: nu \is a linear_char := cfDet_lin_char _. have nuNlam: 'Res nu = lambda by rewrite -cfDetRes ?irr_char ?etaNth. have lin_lam: lambda \is a linear_char := cfDet_lin_char _. have lin_mu: mu \is a linear_char. by have:= lin_lam; rewrite -muNlam; apply: cfRes_lin_lin; apply: irr_char. have [Unu Ulam] := (lin_char_unitr lin_nu, lin_char_unitr lin_lam). pose alpha := mu / nu. have alphaN_1: 'Res[N] alpha = 1 by rewrite rmorph_div //= muNlam nuNlam divrr. have lin_alpha: alpha \is a linear_char by apply: rpred_div. have alpha_e: alpha ^+ e = 1. have kerNalpha: N \subset cfker alpha. by rewrite -subsetIidl -cfker_Res ?lin_charW // alphaN_1 cfker_cfun1. apply/eqP; rewrite -(cfQuoK nsNG kerNalpha) -rmorphXn cfMod_eq1 //. rewrite -dvdn_cforder /e -card_quotient //. by rewrite cforder_lin_char_dvdG ?cfQuo_lin_char. have det_alphaXeta b: cfDet (alpha ^+ b * eta) = alpha ^+ (b * f) * nu. by rewrite cfDet_mul_lin ?rpredX ?irr_char // -exprM -(cfRes1 N) etaNth. have [b bf_mod_e]: exists b, b * f = 1 %[mod e]. rewrite -(chinese_modl co_e_f 1 0) /chinese !mul0n addn0 !mul1n mulnC. by exists (egcdn f e).1. have alpha_bf: alpha ^+ (b * f) = alpha. by rewrite -(expr_mod _ alpha_e) bf_mod_e expr_mod. have /irrP[c Dc]: alpha ^+ b * eta \in irr G. by rewrite mul_lin_irr ?rpredX ?mem_irr. have chiN: 'Res 'chi_c = theta. by rewrite -Dc rmorphM rmorphXn /= alphaN_1 expr1n mul1r. have det_chi: cfDet 'chi_c = mu by rewrite -Dc det_alphaXeta alpha_bf divrK. exists c => // c2 c2Nth det_c2_mu; apply: irr_inj. have [irrMc _ imMc _] := constt_Ind_ext nsNG chiN. have /codomP[s2 Dc2]: c2 \in codom (@mul_mod_Iirr G N c). by rewrite -imMc constt_Ind_Res c2Nth constt_irr ?inE. have{} Dc2: 'chi_c2 = ('chi_s2 %% N)%CF * 'chi_c. by rewrite Dc2 cfIirrE // mod_IirrE. have s2_lin: 'chi_s2 \is a linear_char. rewrite qualifE/= irr_char; apply/eqP/(mulIf (irr1_neq0 c)). rewrite mul1r -[in RHS](cfRes1 N) chiN -c2Nth cfRes1. by rewrite Dc2 cfunE cfMod1. have s2Xf_1: 'chi_s2 ^+ f = 1. apply/(can_inj (cfModK nsNG))/(mulIr (lin_char_unitr lin_mu))/esym. rewrite rmorph1 rmorphXn /= mul1r -{1}det_c2_mu Dc2 -det_chi. by rewrite cfDet_mul_lin ?cfMod_lin_char ?irr_char // -(cfRes1 N) chiN. suffices /eqP s2_1: 'chi_s2 == 1 by rewrite Dc2 s2_1 rmorph1 mul1r. rewrite -['chi_s2]expr1 -dvdn_cforder -(eqnP co_e_f) dvdn_gcd. by rewrite /e -card_quotient ?cforder_lin_char_dvdG //= dvdn_cforder s2Xf_1. 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)