proposition: Lemma constant_irr_mod_TI_Sylow Z L P p i : p.-Sylow(G) P -> odd #|L| -> normedTI P^# G L -> [/\ Z <| L, Z :!=: 1%g & Z \subset 'Z(P)] -> {in Z^# &, forall x y, #|'C_L[x]| = #|'C_L[y]| } -> let phi := 'chi[G]_i in {in Z^# &, forall x y, phi x = phi y} -> {in Z^#, forall x, phi x \in Cint /\ (#|P| %| phi x - phi 1%g)%C}.
proof: Proof. move=> sylP oddL tiP [/andP[sZL nZL] ntZ sZ_ZP] prZL; move: i. pose a := @gring_classM_coef _ G; pose C (i : 'I_#|classes G|) := enum_val i. have [[sPG pP p'PiG] [sZP cPZ]] := (and3P sylP, subsetIP sZ_ZP). have [ntP sLG memJ_P1] := normedTI_memJ_P tiP; rewrite setD_eq0 subG1 in ntP. have nsPL: P <| L. by have [_ _ /eqP<-] := and3P tiP; rewrite normD1 normal_subnorm. have [p_pr _ [e oP]] := pgroup_pdiv pP ntP. have [sZG [sPL _]] := (subset_trans sZP sPG, andP nsPL). pose dC i (A : {set gT}) := [disjoint C i & A]. have actsGC i: {acts G, on C i | 'J}. apply/actsP; rewrite astabsJ /C; have /imsetP[x _ ->] := enum_valP i. by apply/normsP; apply: classGidr. have{actsGC} PdvKa i j s: ~~ dC i Z^# -> ~~ dC j Z^# -> dC s Z -> (#|P| %| a i j s * #|C s|)%N. - pose Omega := [set uv in [predX C i & C j] | mulgm uv \in C s]%g. pose to_fn uv x := uncurry (fun u v : gT => (u ^ x, v ^ x)%g) uv. have toAct: is_action setT to_fn. by apply: is_total_action => [[u v]|[u v] x y] /=; rewrite ?conjg1 ?conjgM. move=> Zi Zj Z's; pose to := Action toAct. have actsPO: [acts P, on Omega | to]. apply/(subset_trans sPG)/subsetP=> x Gx; rewrite !inE. apply/subsetP=> [[u v] /setIdP[/andP/=[Ciu Cjv] Csuv]]. by rewrite !inE /= -conjMg !actsGC // Ciu Cjv. have <-: #|Omega| = (a i j s * #|C s|)%N. have /repr_classesP[_ defCs] := enum_valP s; rewrite -/(C s) in defCs. rewrite -sum1_card mulnC -sum_nat_const. rewrite (partition_big mulgm (mem (C s))) => [|[u v] /setIdP[]//]. apply: eq_bigr; rewrite /= defCs => _ /imsetP[z Gz ->]. rewrite -[a i j s]sum1_card -!/(C _) (reindex_inj (act_inj to z)) /=. apply: eq_bigl => [[u v]]; rewrite !inE /= -conjMg (inj_eq (conjg_inj _)). by apply: andb_id2r => /eqP->; rewrite {2}defCs imset_f ?andbT ?actsGC. suffices regPO: {in Omega, forall uv, 'C_P[uv | to] = 1%g}. rewrite -(acts_sum_card_orbit actsPO) dvdn_sum // => _ /imsetP[uv Ouv ->]. by rewrite card_orbit regPO // indexg1. case=> u v /setIdP[/andP[/= Ciu Cjv] Csuv]; apply: contraTeq Z's. case/trivgPn=> x /setIP[Px /astab1P[/= cux cvx]] nt_x. suffices inZ k y: y \in C k -> ~~ dC k Z^# -> y ^ x = y -> y \in Z. apply/exists_inP; exists (u * v)%g => //=. by rewrite groupM // (inZ i u, inZ j v). rewrite /dC /C; have /imsetP[_ _ ->{k} /class_eqP <-] := enum_valP k. case/exists_inP=> _ /imsetP[g Gg ->] /setD1P[nt_yg Zyg] yx. have xy: (x ^ y = x)%g by rewrite /conjg (conjgCV x) -{2}yx conjgK mulKg. rewrite -(memJ_conjg _ g) (normsP nZL) //. rewrite -(memJ_P1 y) ?inE //=; first by rewrite nt_yg (subsetP sZP). rewrite -order_eq1 -(orderJ y g) order_eq1 nt_yg. rewrite (mem_normal_Hall (pHall_subl sPL sLG sylP)) //. by rewrite -(p_eltJ _ _ g) (mem_p_elt pP) ?(subsetP sZP). rewrite -(memJ_P1 x) // ?xy ?inE ?nt_x // -[y](conjgK g) groupJ ?groupV //. by rewrite (subsetP sZG). pose a2 i j := (\sum_(s | ~~ dC s Z^#) a i j s)%N. pose kerZ l := {in Z^# &, forall x y, 'chi[G]_l x = 'chi_l y}. move=> l phi kerZl z Z1z; move: l @phi {kerZl}(kerZl : kerZ l). have [ntz Zz] := setD1P Z1z. have [[Pz Lz] Gz] := (subsetP sZP z Zz, subsetP sZL z Zz, subsetP sZG z Zz). pose inC y Gy := enum_rank_in (@mem_classes _ y G Gy) (y ^: G). have CE y Gy: C (inC y Gy) = y ^: G by rewrite /C enum_rankK_in ?mem_classes. pose i0 := inC _ (group1 G); pose i1 := inC z Gz; pose i2 := inC _ (groupVr Gz). suffices Ea2 l (phi := 'chi[G]_l) (kerZphi : kerZ l): (phi z *+ a2 i1 i1 == phi 1%g + phi z *+ a2 i1 i2 %[mod #|P|])%A. - move=> l phi kerZphi. have Zphi1: phi 1%g \in Cint by rewrite irr1_degree rpred_nat. have chi0 x: x \in Z -> 'chi[G]_0 x = 1. by rewrite irr0 cfun1E => /(subsetP sZG) ->. have: kerZ 0 by move=> x y /setD1P[_ Zx] /setD1P[_ Zy]; rewrite !chi0. move/Ea2/(eqAmodMl (Aint_irr l z)); rewrite !{}chi0 // -/phi eqAmod_sym. rewrite mulrDr mulr1 !mulr_natr => /eqAmod_trans/(_ (Ea2 l kerZphi)). rewrite eqAmodDr -/phi eqAmod_rat ?rpred_nat ?(rpred_Cint _ Zphi1) //. move=> PdvDphi; split; rewrite // -[phi z](subrK (phi 1%g)) rpredD //. by have /dvdCP[b Zb ->] := PdvDphi; rewrite rpredM ?rpred_nat. have nz_Z1: #|Z^#|%:R != 0 :> algC. by rewrite pnatr_eq0 cards_eq0 setD_eq0 subG1. rewrite -[phi z](mulfK nz_Z1) rpred_div ?rpred_nat // mulr_natr. rewrite -(rpredDl _ (rpred_Cint _ Zphi1)) //. rewrite -[_ + _](mulVKf (neq0CG Z)) rpredM ?rpred_nat //. have: '['Res[Z] phi, 'chi_0] \in Crat. by rewrite rpred_Cnat ?Cnat_cfdot_char ?cfRes_char ?irr_char. rewrite irr0 cfdotE (big_setD1 _ (group1 Z)) cfun1E cfResE ?group1 //=. rewrite rmorph1 mulr1; congr (_ * (_ + _) \in Crat). rewrite -sumr_const; apply: eq_bigr => x Z1x; have [_ Zx] := setD1P Z1x. by rewrite cfun1E cfResE ?Zx // rmorph1 mulr1; apply: kerZphi. pose alpha := 'omega_l['K_i1]; pose phi1 := phi 1%g. have tiZG: {in Z^#, forall y, 'C_G[y] \subset L}. move=> y /setD1P[nty /(subsetP sZP)Py]. apply/subsetP=> u /setIP[Gu /cent1P-cuy]. by rewrite -(memJ_P1 y) // /conjg -?cuy ?mulKg !inE nty. have Dalpha s: ~~ dC s Z^# -> alpha = 'omega_l['K_s]. case/exists_inP=> x /= /gring_mode_class_sum_eq-> Z1x. have Ci1z: z \in C i1 by rewrite CE class_refl. rewrite [alpha](gring_mode_class_sum_eq _ Ci1z) -/phi (kerZphi z x) //. have{} tiZG: {in Z^#, forall y, 'C_G[y] = 'C_L[y]}. by move=> y /tiZG/setIidPr; rewrite setIA (setIidPl sLG). by rewrite -!index_cent1 -!divgS ?subsetIl //= !tiZG ?(prZL z x). have Ci01: 1%g \in C i0 by rewrite CE class_refl. have rCi10: repr (C i0) = 1%g by rewrite CE class1G repr_set1. have Dalpha2 i j: ~~ dC i Z^# -> ~~ dC j Z^# -> (phi1 * alpha ^+ 2 == phi1 * ((a i j i0)%:R + alpha *+ a2 i j) %[mod #|P|])%A. - move=> Z1i Z1j. have ->: phi1 * alpha ^+ 2 = \sum_s (phi1 *+ a i j s) * 'omega_l['K_s]. rewrite expr2 {1}(Dalpha i Z1i) (Dalpha j Z1j). rewrite -gring_irr_modeM ?gring_class_sum_central //. rewrite gring_classM_expansion raddf_sum mulr_sumr; apply: eq_bigr => s _. by rewrite scaler_nat raddfMn mulrnAl mulrnAr. rewrite (bigID (fun s => dC s Z^#)) (bigD1 i0) //=; last first. by rewrite [dC _ _]disjoints_subset CE class1G sub1set !inE eqxx. rewrite (gring_mode_class_sum_eq _ Ci01) mulfK ?irr1_neq0 //. rewrite class1G cards1 mulr1 mulrDr mulr_natr -addrA eqAmodDl. rewrite /eqAmod -addrA rpredD //; last first. rewrite -mulr_natr natr_sum !mulr_sumr -sumrB rpred_sum // => s Z1s. by rewrite -Dalpha // mulr_natr mulrnAl mulrnAr subrr rpred0. apply: rpred_sum => // s /andP[Z1'Cs ntCs]; rewrite mulrnAl mulrC. have /imsetP[x _ defCs] := enum_valP s. have Cs_x: x \in C s by rewrite /C defCs class_refl. rewrite (gring_mode_class_sum_eq _ Cs_x) divfK ?irr1_neq0 // -defCs -/(C s). rewrite -mulrnAl -mulrnA mulnC -[_%:R]subr0 mulrBl. apply: eqAmodMr; first exact: Aint_irr. rewrite eqAmod0_rat ?rpred_nat // dvdC_nat PdvKa //. rewrite -(setD1K (group1 Z)) [dC _ _]disjoint_sym disjoints_subset. rewrite subUset sub1set inE -disjoints_subset disjoint_sym. rewrite (contra _ ntCs) // [C s]defCs => /class_eqP. by rewrite -(inj_eq enum_val_inj) defCs -/(C _) CE => ->. have zG'z1: (z^-1 \notin z ^: G)%g. have genL2 y: y \in L -> <[y]> = <[y ^+ 2]>. move=> Ly; apply/eqP; rewrite [_ == _]generator_coprime. by rewrite coprime_sym prime_coprime // dvdn2 (oddSg _ oddL) ?cycle_subG. apply: contra (ntz) => /imsetP[y Gy zy]. have cz_y2: (y ^+ 2 \in 'C[z])%g. by rewrite !inE conjg_set1 conjgM -zy conjVg -zy invgK. rewrite -cycle_eq1 genL2 // cycle_eq1 -eq_invg_mul zy (sameP eqP conjg_fixP). rewrite (sameP commgP cent1P) cent1C -cycle_subG genL2 ?cycle_subG //. by rewrite -(memJ_P1 z) -?zy ?in_setD ?groupV ?inE ?ntz. have a110: a i1 i1 i0 = 0%N. apply: contraNeq zG'z1 => /existsP[[u v] /setIdP[/andP[/=]]]. rewrite rCi10 -!/(C _) !CE -eq_invg_mul => /imsetP[x Gx ->] /class_eqP <-. by move/eqP <-; rewrite -conjVg classGidl ?class_refl. have a120: a i1 i2 i0 = #|C i1|. rewrite -(card_imset _ (@can_inj _ _ (fun y => (y, y^-1)%g) (@fst _ _) _)) //. apply/eq_card=> [[u v]]; rewrite !inE rCi10 -eq_invg_mul -!/(C _) !CE -andbA. apply/and3P/imsetP=> /= [[zGu _ /eqP<-] | [y zGy [-> ->]]]; first by exists u. by rewrite classVg inE invgK. have Z1i1: ~~ dC i1 Z^#. by apply/exists_inP; exists z; rewrite //= CE class_refl. have Z1i2: ~~ dC i2 Z^#. apply/exists_inP; exists z^-1%g; first by rewrite /= CE class_refl. by rewrite /= in_setD !groupV !inE ntz. have{Dalpha2}: (phi1 * (alpha *+ a2 i1 i1) == phi1 * (#|C i1|%:R + alpha *+ a2 i1 i2) %[mod #|P|])%A. - rewrite -a120; apply: eqAmod_trans (Dalpha2 i1 i2 Z1i1 Z1i2). by have:= Dalpha2 _ _ Z1i1 Z1i1; rewrite a110 add0r eqAmod_sym. rewrite mulrDr !mulrnAr mulr1 -/phi1. have ->: phi1 * alpha = phi z *+ #|C i1|. have Ci1z: z \in C i1 by rewrite CE class_refl. rewrite [alpha](gring_mode_class_sum_eq _ Ci1z) mulrC divfK ?irr1_neq0 //. by rewrite mulr_natl CE. rewrite -!mulrnA !(mulnC #|C _|) !mulrnA -mulrnDl. have [|r _ /dvdnP[q Dqr]] := @Bezoutl #|C i1| #|P|. by rewrite CE -index_cent1. have Zq: q%:R \in Aint by apply: rpred_nat. move/(eqAmodMr Zq); rewrite ![_ *+ #|C _| * _]mulrnAl -!mulrnAr -mulrnA -Dqr. have /eqnP->: coprime #|C i1| #|P|. rewrite (p'nat_coprime _ pP) // (pnat_dvd _ p'PiG) // CE -index_cent1. by rewrite indexgS // subsetI sPG sub_cent1 (subsetP cPZ). rewrite add1n !mulrS !mulrDr !mulr1 natrM !mulrA. set u := _ * r%:R; set v := _ * r%:R; rewrite -[u](subrK v) mulrDl addrA. rewrite eqAmodDr; apply: eqAmod_trans; rewrite eqAmod_sym addrC. rewrite eqAmod_addl_mul // -mulrBl mulr_natr. by rewrite !(rpredB, rpredD, rpredMn, Aint_irr). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action zmodp) mathcomp(gfunctor gproduct cyclic pgroup commutator gseries nilpotent) mathcomp(sylow abelian maximal hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC algnum) mathcomp(classfun character inertia vcharacter integral_char) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)