Skip to content

Commit

Permalink
WIP
Browse files Browse the repository at this point in the history
  • Loading branch information
@proux01
proux01 committed Nov 28, 2023
1 parent 6fa8ce4 commit 84fd62d
Show file tree
Hide file tree
Showing 5 changed files with 13 additions and 7 deletions.
2 changes: 1 addition & 1 deletion theories/BGsection12.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -306,7 +306,7 @@ have SylowE3 P: Sylow E3 P -> [/\ cyclic P, P \subset E^`(1) & 'C_P(E) = 1].
have sP_Ep'P: P \subset 'O_p^'(E) <*> P := joing_subr _ _.
have sylP_Ep'P := pHall_subl sP_Ep'P (normal_sub nsEp'P_E) sylP_E.
rewrite -{2}(Frattini_arg nsEp'P_E sylP_Ep'P) /= !norm_joinEr //.
by rewrite -mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
by rewrite -[LHS]mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA.
have ntPE': P :&: E^`(1) != 1.
have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E.
rewrite -rank_gt0 (rank_Sylow sylPE') p_rank_gt0.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection16.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -411,7 +411,7 @@ rewrite /FTtype (eq_p'group _ (kappaJ _ _)) pgroupJ MsigmaJ FcoreJ derJ.
rewrite !(can_eq (conjsgK x)); do 4!congr (if _ then _ else _).
rewrite -quotientInorm normJ -conjIg /= setIC -{1 3}(setIidPr (normG M`_\F)).
rewrite -!morphim_conj -morphim_quotm ?normalG //= => nsMFN.
by rewrite injm_abelian /= ?im_quotient // injm_quotm ?injm_conj.
by rewrite injm_abelian/= ?im_quotient?/reverse_coercion ?injm_quotm ?injm_conj.
Qed.

Lemma FTcoreJ M x : (M :^ x)`_\s = M`_\s :^ x.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection2.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1138,7 +1138,7 @@ split.
have Ur: r \in GRing.unit.
by rewrite -(unitrX_pos _ (prime_gt0 q_pr)) rq1 unitr1.
pose u_r : {unit 'F_p} := Sub r Ur; have:= order_dvdG (in_setT u_r).
rewrite card_units_Zp ?pdiv_gt0 // {2}/pdiv primes_prime //=.
rewrite card_units_Zp ?pdiv_gt0 // [X in totient X]/pdiv primes_prime //=.
rewrite (@totient_pfactor p 1) // muln1; apply: dvdn_trans.
have: (u_r ^+ q == 1)%g.
by rewrite -val_eqE unit_Zp_expg -Zp_nat natrX natr_Zp rq1.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection3.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -548,7 +548,7 @@ have irrK'K: mx_absolutely_irreducible rK'K.
by rewrite mem_enum.
by rewrite PackSocleK.
have [i def_i]: exists i, [set: sK'G'] = [set i].
apply/cards1P; rewrite -dvdn1 -{7}(eqnP coKp) dvdn_gcd.
apply/cards1P; rewrite -dvdn1 -[X in _ %| X](eqnP coKp) dvdn_gcd.
by rewrite -{1}eq_sK' sK'_dv_K sK'_dv_p.
pose M := socle_base i; have simM : mxsimple rK'G' M := socle_simple i.
have cycGq: cyclic (G' / K^`(1)).
Expand Down
12 changes: 9 additions & 3 deletions theories/PFsection9.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -411,7 +411,8 @@ pose phi w := invm (inj_Zp_h w) \o restr_perm <[h ^ w]> \o actperm 'Q.
have dU w: w \in W1bar -> {subset U <= 'dom (phi w)}.
move=> Ww x Ux; have Qx := subsetP (acts_dom actsUH1) x Ux.
rewrite inE Qx /= im_Zp_unitm inE mem_morphpre //=; last first.
by apply: Aut_restr_perm (actperm_Aut 'Q _); rewrite //= quotientT.
by apply: Aut_restr_perm (actperm_Aut 'Q _);
rewrite //= quotientT?/reverse_coercion.
rewrite cycleJ -defH1 !inE /=; apply/subsetP=> z H1w_z; rewrite inE actpermK.
rewrite qactJ (subsetP nH0U) ?memJ_norm // normJ mem_conjg.
by rewrite (subsetP nH1U) // -mem_conjg (normsP nUW1b) ?mem_quotient.
Expand Down Expand Up @@ -531,8 +532,8 @@ have cEE A: A \in E_U -> centgmx rU A.
apply/row_matrixP=> i; rewrite row_mul; move: (row i _) => h.
have cHbH': (U / H0)^`(1) \subset 'C(Hbar).
by rewrite -quotient_der ?quotient_cents.
apply: rVabelem_inj; rewrite rVabelemJ ?groupR //.
by apply: (canLR (mulKg _)); rewrite -(centsP cHbH') ?mem_commg ?mem_rVabelem.
apply: rVabelem_inj; rewrite rVabelemJ ?groupR //; apply: (canLR (mulKg _)).
by rewrite -[LHS](centsP cHbH')// ?mem_commg ?mem_rVabelem.
have{cEE} [F [outF [inF outFK inFK] E_F]]:
{F : finFieldType & {outF : {rmorphism F -> 'M(Hbar)%Mg}
& {inF : {additive _ -> _} | cancel outF inF & {in E_U, cancel inF outF}}
Expand Down Expand Up @@ -1014,6 +1015,11 @@ have sW1_Imu i: W1 \subset 'I[theta (mu_f i) %% H0]%CF.
rewrite -(cfResE _ (sH1wH _ W1w1w)) -?mem_conjg -?conjsgM ?mulgKV ?H1x //.
rewrite -(cfResE _ (sH1wH _ W1w1)) ?H1x ?cfBigdprodKabelian //.
rewrite !ffunE W1w1 W1w1w -[x w1](conjgKV w1) -conjgM !isom_IirrE.
pose RR := @cfIsomE _ _ _ _ _ (isoJ (w1 * (inMb w)^-1)%g) 'chi_i.
clearbody RR.
rewrite /reverse_coercion in RR.

Check failure on line 1020 in theories/PFsection9.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.16) 

The reference reverse_coercion was not found in the current

Check failure on line 1020 in theories/PFsection9.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.0.0-coq-8.17) 

The variable reverse_coercion was not found in the current

Check failure on line 1020 in theories/PFsection9.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.16) 

The reference reverse_coercion was not found in the current

Check failure on line 1020 in theories/PFsection9.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-8.17) 

The variable reverse_coercion was not found in the current
rewrite RR.
rewrite [LHS]cfIsomE.

Check failure on line 1022 in theories/PFsection9.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp-dev:coq-dev) 

pattern ('chi_i (x w1 ^ w1^-1)) does not match LHS of cfIsomE
by rewrite !cfIsomE -?mem_conjg ?H1x.
have inj_mu: {in predC1 0 &, injective (fun i => cfIirr (mk_mu i))}.
move=> i1 i2 nz_i1 nz_i2 /(congr1 (tnth (irr HU))).
Expand Down

0 comments on commit 84fd62d

Please sign in to comment.