proposition: Theorem constt_Inertia_bijection : [/\ {in calA, forall s, 'Ind[G] 'chi_s \in irr G}, {in calA &, injective (Ind_Iirr G)}, Ind_Iirr G @: calA =i calB, {in calA, forall s (psi := 'chi_s) (chi := 'Ind[G] psi), [predI irr_constt ('Res chi) & calA] =i pred1 s} & {in calA, forall s (psi := 'chi_s) (chi := 'Ind[G] psi), '['Res psi, theta] = '['Res chi, theta]}].
proof: Proof. have [sHG sTG]: H \subset G /\ T \subset G by rewrite subsetIl normal_sub. have nsHT : H <| T := normal_Inertia theta sHG; have sHT := normal_sub nsHT. have AtoB_P s (psi := 'chi_s) (chi := 'Ind[G] psi): s \in calA -> [/\ chi \in irr G, AtoB s \in calB & '['Res psi, theta] = '['Res chi, theta]]. - rewrite !constt_Ind_Res => sHt; have [r sGr] := constt_cfInd_irr s sTG. have rTs: s \in irr_constt ('Res[T] 'chi_r) by rewrite -constt_Ind_Res. have NrT: 'Res[T] 'chi_r \is a character by rewrite cfRes_char ?irr_char. have rHt: t \in irr_constt ('Res[H] 'chi_r). by have:= constt_Res_trans NrT rTs sHt; rewrite cfResRes. pose e := '['Res[H] 'chi_r, theta]; set f := '['Res[H] psi, theta]. have DrH: 'Res[H] 'chi_r = e *: \sum_(xi <- (theta ^: G)%CF) xi. exact: Clifford_Res_sum_cfclass. have DpsiH: 'Res[H] psi = f *: theta. rewrite (Clifford_Res_sum_cfclass nsHT sHt). by rewrite cfclass_invariant ?subsetIr ?big_seq1. have ub_chi_r: 'chi_r 1%g <= chi 1%g ?= iff ('chi_r == chi). have Nchi: chi \is a character by rewrite cfInd_char ?irr_char. have [chi1 Nchi1->] := constt_charP _ Nchi sGr. rewrite addrC cfunE -leifBLR subrr eq_sym -subr_eq0 addrK. by split; rewrite ?char1_ge0 // eq_sym char1_eq0. have lb_chi_r: chi 1%g <= 'chi_r 1%g ?= iff (f == e). rewrite cfInd1 // -(cfRes1 H) DpsiH -(cfRes1 H 'chi_r) DrH !cfunE sum_cfunE. rewrite (eq_big_seq (fun _ => theta 1%g)) => [|i]; last first. by case/cfclassP=> y _ ->; rewrite cfConjg1. rewrite reindex_cfclass //= sumr_const -(eq_card (cfclass_IirrE _ _)). rewrite mulr_natl mulrnAr card_cfclass_Iirr //. rewrite (mono_leif (ler_pMn2r (indexg_gt0 G T))). rewrite (mono_leif (ler_pM2r (irr1_gt0 t))); apply: leif_eq. by rewrite /e -(cfResRes _ sHT) ?cfdot_Res_ge_constt. have [_ /esym] := leif_trans ub_chi_r lb_chi_r; rewrite eqxx. by case/andP=> /eqP Dchi /eqP->; rewrite cfIirrE -/chi -?Dchi ?mem_irr. have part_c: {in calA, forall s (chi := 'Ind[G] 'chi_s), [predI irr_constt ('Res[T] chi) & calA] =i pred1 s}. - move=> s As chi s1; have [irr_chi _ /eqP Dchi_theta] := AtoB_P s As. have chiTs: s \in irr_constt ('Res[T] chi). by rewrite irr_consttE cfdot_Res_l irrWnorm ?oner_eq0. apply/andP/eqP=> [[/= chiTs1 As1] | -> //]. apply: contraTeq Dchi_theta => s's1; rewrite lt_eqF // -/chi. have [|phi Nphi DchiT] := constt_charP _ _ chiTs. by rewrite cfRes_char ?cfInd_char ?irr_char. have [|phi1 Nphi1 Dphi] := constt_charP s1 Nphi _. rewrite irr_consttE -(canLR (addKr _) DchiT) addrC cfdotBl cfdot_irr. by rewrite mulrb ifN_eqC ?subr0. rewrite -(cfResRes chi sHT sTG) DchiT Dphi !rmorphD !cfdotDl /=. rewrite -ltrBDl subrr ltr_wpDr ?lt_def //; rewrite natr_ge0 ?Cnat_cfdot_char ?cfRes_char ?irr_char //. by rewrite andbT -irr_consttE -constt_Ind_Res. do [split=> //; try by move=> s /AtoB_P[]] => [s1 s2 As1 As2 | r]. have [[irr_s1G _ _] [irr_s2G _ _]] := (AtoB_P _ As1, AtoB_P _ As2). move/(congr1 (tnth (irr G))); rewrite !cfIirrE // => eq_s12_G. apply/eqP; rewrite -[_ == _]part_c // inE /= As1 -eq_s12_G. by rewrite -As1 [_ && _]part_c // inE /=. apply/imsetP/idP=> [[s /AtoB_P[_ BsG _] -> //] | Br]. have /exists_inP[s rTs As]: [exists s in irr_constt ('Res 'chi_r), s \in calA]. rewrite -negb_forall_in; apply: contra Br => /eqfun_inP => o_tT_rT. rewrite -(cfIndInd _ sTG sHT) -cfdot_Res_r ['Res _]cfun_sum_constt. by rewrite cfdot_sumr big1 // => i rTi; rewrite cfdotZr o_tT_rT ?mulr0. exists s => //; have [/irrP[r1 DsG] _ _] := AtoB_P s As. by apply/eqP; rewrite /AtoB -constt_Ind_Res DsG irrK constt_irr in rTs *. 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)