proposition: Lemma cfInd_central_Inertia : exists2 e, [/\ e \in Cnat, e != 0 & {in calA, forall t, e_ t = e}] & [/\ 'Ind[G] theta = e *: \sum_(j in calB) 'chi_j, #|calB|%:R = #|T : H|%:R / e ^+ 2 & {in calB, forall i, 'chi_i 1%g = #|G : T|%:R * e * theta 1%g}].
proof: Proof. have [t1 At1] := constt_cfInd_irr s sHT; pose psi1 := 'chi_t1. pose e := '['Ind theta, psi1]. have NthT: 'Ind[T] theta \is a character by rewrite cfInd_char ?irr_char. have Ne: e \in Cnat by rewrite Cnat_cfdot_char_irr. have Dpsi1H: 'Res[H] psi1 = e *: theta. have psi1Hs: s \in irr_constt ('Res psi1) by rewrite -constt_Ind_Res. rewrite (Clifford_Res_sum_cfclass nsHT psi1Hs) cfclass_invariant ?subsetIr //. by rewrite big_seq1 cfdot_Res_l cfdotC conj_Cnat. have linL j: 'chi[T / H]_j \is a linear_char by apply/char_abelianP. have linLH j: ('chi_j %% H)%CF \is a linear_char := cfMod_lin_char (linL j). pose LtoT (j : Iirr (T / H)) := mul_mod_Iirr t1 j. have LtoTE j: 'chi_(LtoT j) = ('chi_j %% H)%CF * psi1. by rewrite !(mod_IirrE, cfIirrE) // mul_lin_irr ?mem_irr ?cfMod_lin_char. have psiHG: 'Ind ('Res[H] psi1) = \sum_j 'chi_(LtoT j). transitivity ((cfReg (T / H) %% H)%CF * psi1); last first. rewrite cfReg_sum linear_sum /= mulr_suml; apply: eq_bigr => i _. by rewrite LtoTE // lin_char1 ?scale1r. apply/cfun_inP=> x Tx; rewrite cfunE cfModE // cfRegE mulrnAl mulrb. rewrite (sameP eqP (kerP _ (subsetP nHT x Tx))) ker_coset. case: ifPn => [Hx | H'x]; last by rewrite (cfun_on0 (cfInd_normal _ _)). rewrite card_quotient // -!(cfResE _ sHT) // cfRes_Ind_invariant ?cfunE //. by rewrite -subsetIidl (subset_trans _ (sub_inertia_Res _ _)) ?sub_Inertia. have imLtoT: {subset calA <= codom LtoT}. move=> t At; apply/codomP/exists_eqP. have{At}: t \in irr_constt ('Ind ('Res[H] 'chi_t1)). by rewrite Dpsi1H linearZ irr_consttE cfdotZl mulf_neq0. apply: contraR; rewrite negb_exists => /forallP imL't. by rewrite psiHG cfdot_suml big1 // => j _; rewrite cfdot_irr mulrb ifN_eqC. have De_ t: t \in calA -> e_ t = e. case/imLtoT/codomP=> j ->; rewrite /e_ LtoTE /e -!cfdot_Res_r rmorphM /=. by rewrite cfRes_sub_ker ?cfker_mod // mulr_algl lin_char1 ?scale1r. have{imLtoT} A_1 t: t \in calA -> 'chi_t 1%g = e * theta 1%g. case/imLtoT/codomP=> j ->; rewrite LtoTE //= cfunE. by rewrite (lin_char1 (linLH j)) mul1r -(cfRes1 H) Dpsi1H cfunE. exists e => //; have [_ defAtoB injAtoB imAtoB ->] := cfInd_sum_Inertia. rewrite -(eq_bigl _ _ imAtoB) -(eq_card imAtoB) big_imset //= scaler_sumr. split=> [||i]; first by apply: eq_bigr => t2 At2; rewrite De_ ?defAtoB. apply: (mulIf (irr1_neq0 s)); rewrite mulrAC -cfInd1 // mulr_natl mulrC invfM. rewrite ['Ind _]cfun_sum_constt sum_cfunE mulr_sumr card_in_imset //. rewrite -sumr_const; apply: eq_bigr => t At. by rewrite -mulrA -/(e_ t) De_ // cfunE A_1 ?mulKf. by rewrite -imAtoB => /imsetP[t At ->]; rewrite defAtoB ?cfInd1 ?A_1 ?mulrA. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop prime order ssralg finset fingroup morphism) mathcomp(perm automorphism quotient action zmodp finalg center commutator) mathcomp(poly cyclic pgroup nilpotent matrix mxalgebra mxrepresentation) mathcomp(vector falgebra fieldext ssrnum algC rat algnum galois) mathcomp(classfun character inertia integral_char vcharacter)