diff options
Diffstat (limited to 'mathcomp/odd_order/PFsection9.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection9.v | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v index 0cd1109..d8ec417 100644 --- a/mathcomp/odd_order/PFsection9.v +++ b/mathcomp/odd_order/PFsection9.v @@ -89,7 +89,7 @@ Let defW2 : 'C_H(W1) = W2. Proof. exact: typeP_cent_core_compl MtypeP. Qed. Lemma Ptype_Fcore_sdprod : H ><| (U <*> W1) = M. Proof. -have [_ /= sW1M mulHUW1 _ tiHUW1] := sdprod_context defM. +have [_ /= sW1M mulHUW1 _ tiHUW1] := sdprod_context defM. have [/= /andP[sHHU _] sUHU mulHU nHU tiHU] := sdprod_context defHU. rewrite sdprodE /= norm_joinEr // ?mulgA ?mulHU //. by rewrite mulG_subG nHU (subset_trans sW1M) ?gFnorm. @@ -322,7 +322,7 @@ Proof. apply: Frobenius_quotient frobUW1 _ nsCUW1 _. by apply: nilpotent_sol; have [_ []] := MtypeP. by have [] := Ptype_Fcore_factor_facts; rewrite eqEsubset sCU. -Qed. +Qed. Definition typeP_Galois := acts_irreducibly U Hbar 'Q. @@ -397,7 +397,7 @@ have [oH1 defHbar]: #|H1| = p /\ \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar. by rewrite -(big_imset id injW1) -defH1W0 big_imset. split=> //; set a := #|_ : _|; pose q1 := #|(W1 / H0)^#|. have a_gt1: a > 1. - rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. + rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. apply: contra neqCU => cH1U; rewrite [C]unlock (sameP eqP setIidPl) /= astabQ. rewrite -sub_quotient_pre // -(bigdprodWY defHbar) cent_gen centsC. by apply/bigcupsP=> w Ww; rewrite centsC centJ -(normsP nUW1b w) ?conjSg. @@ -663,7 +663,7 @@ pose nF := <[1%R : F]>; have o_nF: #|nF| = p. have cyc_uF := @field_unit_group_cyclic F. exists F. exists phi; last first. - split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. + split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. by rewrite (@cycle_subG F) mem_morphim //= card_injm ?subsetIl ?oW2b. exists psi => //; last first. by split=> // h x Hh Ux; rewrite qactJ (subsetP nH0U) ?phiJ. @@ -834,7 +834,7 @@ Lemma typeP_nonGalois_characters (not_Galois : ~~ typeP_Galois) : (lb_d %| lb_n /\ lb_n %/ lb_d <= count irr_qa (S_ H0U'))%N]. Proof. case: (typeP_Galois_Pn _) => H1 [oH1 nH1U nH1Uq defHbar aP]; rewrite [sval _]/=. -move => a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb. +move=> a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb. set part_a := ({in _, _}); pose HCbar := (HC / H0)%G. have [_ /mulG_sub[sHUM sW1M] nHUW1 tiHUW1] := sdprodP defM. have [nsHHU _ /mulG_sub[sHHU sUHU] nHU tiHU] := sdprod_context defHU. @@ -870,7 +870,7 @@ have Part_a: part_a. have{kersH0} kertH0: H0 \subset cfker 'chi_t. by rewrite (sub_cfker_constt_Res_irr sHt). have Ltheta: theta \is a linear_char. - by rewrite /theta -quo_IirrE // (char_abelianP _ _). + by rewrite /theta -quo_IirrE // (char_abelianP _ _). have Dtheta : _ = theta := cfBigdprod_Res_lin defHbar Ltheta. set T := 'I_HU['chi_t]; have sHT: H \subset T by rewrite sub_Inertia. have sTHU: T \subset HU by rewrite Inertia_sub. @@ -1086,11 +1086,11 @@ split=> {Part_a part_a}//. rewrite odd_exp -(subnKC (prime_gt1 pr_q)) /= -subn1 odd_sub ?prime_gt0 //. by rewrite -oH1 (oddSg sH1H) ?quotient_odd // mFT_odd. have p1_gt0: (0 < p.-1)%N by rewrite -(subnKC (prime_gt1 p_pr)). - apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. + apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. by rewrite -oXtheta -defXmu card_in_imset // cardC1 card_Iirr_abelian ?oH1. clear Xmu def_IXmu Smu sSmu_mu ResIndXmu uSmu sz_Smu sz_mu s_mu_H0C Dmu. clear Mtheta Xtheta irrXtheta oXtheta sXthXH0C mu_f Fmu_f mk_mu sW1_Imu inj_mu. -clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. +clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. clear theta Dtheta => irr_qa lb_n lb_d. have sU'U: U' \subset U := der_sub 1 U. have nH0U := subset_trans sUHU nH0HU; have nH0U' := subset_trans sU'U nH0U. @@ -1157,7 +1157,7 @@ have{lam_lin} thetaH1 i j: 'Res[H1] (theta i j) = 'chi_i. have Itheta r: r \in Mtheta -> 'I_HU['chi_r]%CF = HCH1. case/imset2P=> i j; rewrite /= in_setC1 => nz_i _ Dr; apply/eqP. rewrite eqEsubset sub_Inertia //= Dr mod_IirrE // cfIirrE ?lin_char_irr //. - rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. + rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. rewrite inertia_mod_quo //. apply: subset_trans (sub_inertia_Res _ (nH1wHUb _ (group1 _))) _. rewrite /= conjsg1 thetaH1 (inertia_irr_prime _ p_pr) //. @@ -1533,7 +1533,7 @@ have sS10: cfConjC_subset S1 (S_ H0C'). have cohS1: coherent S1 M^# tau. apply: uniform_degree_coherence (subset_subcoherent scohS0 sS10) _. by apply: all_pred1_constant (q * a)%:R _ _; rewrite all_map filter_all. -pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. +pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. move: @S3 (sS10) (cohS1); have: {subset S1 <= S1} by []. elim: nS {-1}S1 => // nS IHnS S2 => sS12 S3 sS20 cohS2; rewrite ltnS => leS3nS. have [ntS3|] := boolP (size S3 > 0)%N; last first. @@ -1563,7 +1563,7 @@ without loss [[eqS12 irrS1 H0C_S1] [Da_p defC] [S3qu ne_qa_qu] [oS1 oS1ua]]: pose is_qu := [pred chi : 'CF(M) | chi 1%g == (q * u)%:R]. pose isn't_qu := [pred chi | is_qu chi ==> all is_qu S3]. have /hasP[chi S3chi qu'chi]: has isn't_qu S3. - rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. + rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. by rewrite (eq_has (fun _ => implybT _)) has_predT. have [S2'chi S0chi]: chi \notin S2 /\ chi \in S_ H0C'. by apply/andP; rewrite mem_filter in S3chi. |