proposition: Theorem inertia_Frobenius_ker i : i != 0 -> 'I_G['chi[K]_i] = K.
proof: Proof. have [_ _ nsKG regK] := Frobenius_kerP frobGK; have [sKG nKG] := andP nsKG. move=> nzi; apply/eqP; rewrite eqEsubset sub_Inertia // andbT. apply/subsetP=> x /setIP[Gx /setIdP[nKx /eqP x_stab_i]]. have actIirrK: is_action G (@conjg_Iirr _ K). split=> [y j k eq_jk | j y z Gy Gz]. by apply/irr_inj/(can_inj (cfConjgK y)); rewrite -!conjg_IirrE eq_jk. by apply: irr_inj; rewrite !conjg_IirrE (cfConjgM _ nsKG). pose ito := Action actIirrK; pose cto := ('Js \ (subsetT G))%act. have acts_Js : [acts G, on classes K | 'Js]. apply/subsetP=> y Gy; have nKy := subsetP nKG y Gy. rewrite !inE; apply/subsetP=> _ /imsetP[z Gz ->] /[!inE]/=. rewrite -class_rcoset norm_rlcoset // class_lcoset. by apply: imset_f; rewrite memJ_norm. have acts_cto : [acts G, on classes K | cto] by rewrite astabs_ract subsetIidl. pose m := #|'Fix_(classes K | cto)[x]|. have def_m: #|'Fix_ito[x]| = m. apply: card_afix_irr_classes => // j y _ Ky /imsetP[_ /imsetP[z Kz ->] ->]. by rewrite conjg_IirrE cfConjgEJ // cfunJ. have: (m != 1)%N. rewrite -def_m (cardD1 (0 : Iirr K)) (cardD1 i) !(inE, sub1set) /=. by rewrite conjg_Iirr0 nzi eqxx -(inj_eq irr_inj) conjg_IirrE x_stab_i eqxx. apply: contraR => notKx; apply/cards1P; exists 1%g; apply/esym/eqP. rewrite eqEsubset !(sub1set, inE) classes1 /= conjs1g eqxx /=. apply/subsetP=> _ /setIP[/imsetP[y Ky ->] /afix1P /= cyKx]. have /imsetP[z Kz def_yx]: y ^ x \in y ^: K. by rewrite -cyKx; apply: imset_f; apply: class_refl. rewrite inE classG_eq1; apply: contraR notKx => nty. rewrite -(groupMr x (groupVr Kz)). apply: (subsetP (regK y _)); first exact/setD1P. rewrite !inE groupMl // groupV (subsetP sKG) //=. by rewrite conjg_set1 conjgM def_yx conjgK. 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)