proposition: Lemma Frobenius_kernel_exists : [Frobenius G with complement H] -> {K : {group gT} | [Frobenius G = K ><| H]}.
proof: Proof. move=> frobG; have [_ ntiHG] := andP frobG. have [[_ sHG regGH][_ tiHG /eqP defNH]] := (normedTI_memJ_P ntiHG, and3P ntiHG). suffices /sigW[K defG]: exists K, gval K ><| H == G by exists K; apply/andP. pose K1 := G :\: cover (H^# :^: G). have oK1: #|K1| = #|G : H|. rewrite cardsD (setIidPr _); last first. rewrite cover_imset; apply/bigcupsP=> x Gx. by rewrite sub_conjg conjGid ?groupV // (subset_trans (subsetDl _ _)). rewrite (cover_partition (partition_normedTI ntiHG)) -(Lagrange sHG). by rewrite (card_support_normedTI ntiHG) (cardsD1 1%g) group1 mulSn addnK. suffices extG i: {j | {in H, 'chi[G]_j =1 'chi[H]_i} & K1 \subset cfker 'chi_j}. pose K := [group of \bigcap_i cfker 'chi_(s2val (extG i))]. have nKH: H \subset 'N(K). by apply/norms_bigcap/bigcapsP=> i _; apply: subset_trans (cfker_norm _). have tiKH: K :&: H = 1%g. apply/trivgP; rewrite -(TI_cfker_irr H) /= setIC; apply/bigcapsP=> i _. apply/subsetP=> x /setIP[Hx /bigcapP/(_ i isT)/=]; rewrite !cfkerEirr !inE. by case: (extG i) => /= j def_j _; rewrite !def_j. exists K; rewrite sdprodE // eqEcard TI_cardMg // mul_subG //=; last first. by rewrite (bigcap_min (0 : Iirr H)) ?cfker_sub. rewrite -(Lagrange sHG) mulnC leq_pmul2r // -oK1 subset_leq_card //. by apply/bigcapsP=> i _; case: (extG i). case i0: (i == 0). exists 0 => [x Hx|]; last by rewrite irr0 cfker_cfun1 subsetDl. by rewrite (eqP i0) !irr0 !cfun1E // (subsetP sHG) ?Hx. have ochi1: '['chi_i, 1] = 0 by rewrite -irr0 cfdot_irr i0. pose a := 'chi_i 1%g; have Za: a \in Num.int by rewrite intrE Cnat_irr1. pose theta := 'chi_i - a%:A; pose phi := 'Ind[G] theta + a%:A. have /cfun_onP theta0: theta \in 'CF(H, H^#). by rewrite cfunD1E !cfunE cfun11 mulr1 subrr. have RItheta: 'Res ('Ind[G] theta) = theta. apply/cfun_inP=> x Hx; rewrite cfResE ?cfIndE // (big_setID H) /= addrC. apply: canLR (mulKf (neq0CG H)) _; rewrite (setIidPr sHG) mulr_natl. rewrite big1 ?add0r => [|y /setDP[/regGH tiHy H'y]]; last first. have [-> | ntx] := eqVneq x 1%g; first by rewrite conj1g theta0 ?inE ?eqxx. by rewrite theta0 ?tiHy // !inE ntx. by rewrite -sumr_const; apply: eq_bigr => y Hy; rewrite cfunJ. have ophi1: '[phi, 1] = 0. rewrite cfdotDl -cfdot_Res_r cfRes_cfun1 // cfdotBl !cfdotZl !cfnorm1. by rewrite ochi1 add0r addNr. have{ochi1} n1phi: '[phi] = 1. have: '[phi - a%:A] = '[theta] by rewrite addrK -cfdot_Res_l RItheta. rewrite !cfnormBd ?cfnormZ ?cfdotZr ?ophi1 ?ochi1 ?mulr0 //. by rewrite !cfnorm1 cfnorm_irr => /addIr. have Zphi: phi \in 'Z[irr G]. by rewrite rpredD ?cfInd_vchar ?rpredB ?irr_vchar // scale_zchar ?rpred1. have def_phi: {in H, phi =1 'chi_i}. move=> x Hx /=; rewrite !cfunE -[_ x](cfResE _ sHG) ?RItheta //. by rewrite !cfunE !cfun1E ?(subsetP sHG) ?Hx ?subrK. have [j def_chi_j]: {j | 'chi_j = phi}. apply/sig_eqW; have [[] [j]] := vchar_norm1P Zphi n1phi; last first. by rewrite scale1r; exists j. move/cfunP/(_ 1%g)/eqP; rewrite scaleN1r def_phi // cfunE -addr_eq0 eq_le. by rewrite lt_geF // ltr_pDl ?irr1_gt0. exists j; rewrite ?cfkerEirr def_chi_j //; apply/subsetP => x /setDP[Gx notHx]. rewrite inE cfunE def_phi // cfunE -/a cfun1E // Gx mulr1 cfIndE //. rewrite big1 ?mulr0 ?add0r // => y Gy; apply/theta0/(contra _ notHx) => Hxy. by rewrite -(conjgK y x) cover_imset -class_supportEr imset2_f ?groupV. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(frobenius vector ssrnum ssrint archimedean intdiv) mathcomp(algC algnum classfun character integral_char)