Skip to content

Adapt to MC#1439 #72

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
proux01 merged 1 commit into from
Sep 3, 2025
Merged

Adapt to MC#1439 #72

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
40 changes: 25 additions & 15 deletions theories/BGappendixC.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -596,15 +596,17 @@ have nt_sUs m j n a u s1 v:
have sUs_modP m a j n u s1 v: is_sUs m a j n u s1 v -> a ^ t ^+ j = u * v.
have [nUP /isom_inj/injmP/=quoUP_inj] := sdprod_isom defH.
case=> Ua Uu Uv P0s1 /(congr1 (coset P)); rewrite (conjgCV u) -(mulgA _ u).
rewrite coset_kerr ?groupV 2?coset_kerl ?groupX //; last first.
rewrite coset_kerr ?groupV ?groupX //.
rewrite coset_kerl ?groupX // [RHS]coset_kerl; last first.
by rewrite -mem_conjg (normsP nUP) // (subsetP sP0P).
by move/quoUP_inj->; rewrite ?nUtn ?groupM.
have expUMp u v Uu Uv := expgMn p (centsP cUU u v Uu Uv).
have sUsXp m a j n u s1 v:
is_sUs m a j n u s1 v -> is_sUs m (a ^+ p) j n (u ^+ p) s1 (v ^+ p).
- move=> Dusv; have{Dusv} [/sUs_modP Duv [Ua Uu Vv P0s1 Dusv]] := (Dusv, Dusv).
split; rewrite ?groupX //; move: P0s1 Dusv; rewrite -defP0 => /cycleP[k ->].
rewrite conjXg -!(mulgA _ (s ^+ k)) ![s ^+ k * _]conjgC 2!mulgA -expUMp //.
rewrite conjXg -!(mulgA _ (s ^+ k)) ![s ^+ k * _]conjgC [RHS]mulgA.
rewrite (mulgA (u ^+ p)) -expUMp //.
rewrite {}Duv ![s ^+ m * _]conjgC !conjXg -![_ * _ * s ^- n]mulgA.
move/mulgI/(congr1 (Frobenius_aut charFp \o sigma))=> /= Duv_p.
congr (_ * _); apply/(injmP inj_sigma); rewrite ?in_PU //.
Expand All @@ -630,23 +632,27 @@ pose s2def w1 w2 w3 := t * s2^-1 * t = w1 * s3 * w2 * t ^+ 2 * s1 * w3.
pose w1 := v2 ^ t^-1 * u3; pose w2 := v3 * u1 ^ t ^- 2; pose w3 := v1 * u2 ^ t.
have stXC m n: (m <= n)%N -> s ^- n ^ t ^+ m = s ^- m ^ t ^+ n * s ^- (n - m).
move/subnK=> Dn; apply/(mulgI (s ^- (n - m) * t ^+ n))/(mulIg (t ^+ (n - m))).
rewrite -{1}[in t ^+ n]Dn expgD !mulgA !mulgK -invMg -2!mulgA -!expgD.
by rewrite addnC Dn (centsP (abelem_abelian abelQ)) ?mulgA.
rewrite -{1}[in t ^+ n]Dn expgD !mulgA !mulgK -invMg -3![LHS]mulgA -!expgD.
by rewrite addnC Dn mulgA (centsP (abelem_abelian abelQ)) ?mulgA.
wlog suffices Ds2: a b u1 v1 u2 v2 u3 v3 @w1 @w2 @w3 Dab usv1P usv2P usv3P /
s2def w1 w2 w3; last first.
- apply/esym; rewrite -[_ * t]mulgA [_ * t]conjgC mulgA -(expgS _ 1) conjVg.
rewrite /w2 mulgA; apply: (canRL (mulKVg _)); rewrite 2!mulgA -conjgE.
- apply/esym; rewrite -[_ * t]mulgA [_ * t]conjgC [RHS]mulgA -(expgS _ 1) conjVg.
rewrite /w2 (mulgA _ v3); apply: (canRL (mulKVg _)).
rewrite 2!(mulgA (t ^- 2)) -conjgE.
rewrite conjMg conjgKV /w3 mulgA; apply: (canLR (mulgKV _)).
rewrite /w1 -4!mulgA (mulgA u1) (mulgA u3) conjMg -conjgM mulKg -mulgA.
rewrite /w1 -2!mulgA -(mulgA _ s3) -(mulgA _ u3).
rewrite (mulgA u1) (mulgA u3) conjMg -conjgM mulKg -[LHS]mulgA.
have [[[Ua _ _ _ <-] [_ _ _ _ Ds2]] [Ub _ _ _ <-]] := (usv1P, usv2P, usv3P).
apply: (canLR (mulKVg _)); rewrite -!invMg -!conjMg -{}Ds2 groupV in Ua *.
rewrite -[t]expg1 2!conjMg -conjgM -expgS 2!conjMg -conjgM -expgSr mulgA.
apply: (canLR (mulgK _)); rewrite 2!invMg -!conjVg invgK invMg invgK -4!mulgA.
rewrite -[t]expg1 2!conjMg -conjgM -expgS 2![in RHS]conjMg -conjgM -expgSr mulgA.
apply: (canLR (mulgK _)); rewrite [in RHS]invMg (invMg (_ ^ _)).
rewrite -!conjVg invgK (invMg a) invgK.
rewrite -2!mulgA -[RHS]mulgA -[X in _ = _ * X]mulgA.
rewrite (mulgA _ s) stXC // mulgKV -!conjMg stXC // mulgKV -conjMg conjgM.
apply: (canLR (mulKVg _)); rewrite -2!conjVg 2!mulgA -conjMg (stXC 1%N) //.
rewrite mulgKV -conjgM -expgSr -mulgA -!conjMg; congr (_ ^ t ^+ 3).
apply/(canLR (mulKVg _))/(canLR (mulgK _))/(canLR invgK).
rewrite -!mulgA (mulgA _ b) mulgA invMg -!conjVg !invgK.
rewrite -!mulgA (mulgA _ b) (mulgA b^-1) invMg -!conjVg !invgK.
by apply/(injmP inj_sigma); rewrite 1?groupM ?sigmaE ?memJ_P.
have [[Ua Uu1 Uv1 P0s1 Dusv1] /sUs_modP-Duv1] := (usv1P, usv1P).
have [[_ Uu2 Uv2 P0s2 _] [Ub Uu3 Uv3 P0s3 _]] := (usv2P, usv3P).
Expand All @@ -667,8 +673,10 @@ wlog [Uw1 Uw2 Uw3]: w1 w2 w3 Ds2p Ds2 / [/\ w1 \in U, w2 \in U & w3 \in U].
by move/(_ w1 w2 w3)->; rewrite ?(nUtVn, nUtVn 1%N, nUtn 1%N, in_group).
have{Ds2p} Dw3p: (w2 ^- p * w1 ^- p.-1 ^ s3 * w2) ^ t ^+ 2 = w3 ^+ p.-1 ^ s1^-1.
rewrite -[w1 ^+ _](mulKg w1) -[w3 ^+ _](mulgK w3) -expgS -expgSr !prednK //.
rewrite -(canLR (mulKg _) Ds2p) -(canLR (mulKg _) Ds2) 6!invMg !invgK.
by rewrite mulgA mulgK [2%N]lock /conjg !mulgA mulVg mul1g mulgK.
rewrite -(canLR (mulKg _) Ds2p) -(canLR (mulKg _) Ds2).
rewrite 3!invMg (invMg _ (w2 ^+ p)) (invMg _ s3) (invMg (_^-1)) !invgK.
rewrite [X in _ = X ^ _](mulgA _ _^-1).
by rewrite mulgK [2%N]lock /conjg !mulgA mulVg mul1g mulgK.
have w_id w: w \in U -> w ^+ p.-1 == 1 -> w = 1.
by move=> Uw /eqP/(canRL_in (expgK _) Uw)->; rewrite ?expg1n ?oU.
have{Uw3} Dw3: w3 = 1.
Expand Down Expand Up @@ -706,15 +714,17 @@ pose x := (y ^ s3)^-1 * y ^ s^-1 * (y ^ (s * s1)^-1)^-1 * y.
have{abP0} Dx: x ^ s^-1 = x.
rewrite 3!conjMg !conjVg -!conjgM -!invMg (mulgA s) -(expgS _ 1).
rewrite [x]abQP0 ?memQP0 // [rhs in y * rhs]abQP0 ?memQP0 //.
apply/(canRL (mulKVg _)); rewrite 4!mulgA; congr (_ * _).
apply/(canRL (mulKVg _)); rewrite 3!(mulgA y^-1) [RHS]mulgA; congr (_ * _).
rewrite [RHS]abQP0 ?memQP0 //; apply/(canRL (mulgK _))/eqP.
rewrite -3!mulgA [rhs in y^-1 * rhs]abQP0 ?memQP0 // -eq_invg_sym eq_invg_mul.
rewrite -3![eqbLHS]mulgA.
rewrite [rhs in y^-1 * rhs]abQP0 ?memQP0 // -eq_invg_sym eq_invg_mul.
apply/eqP; transitivity (t ^+ 2 * s1 * (t^-1 * s2 * t^-1) * s3); last first.
by rewrite -[s2]invgK -!invMg mulgA Ds2 -(mulgA s3) invMg mulKVg mulVg.
rewrite (canRL (mulKg _) Ds312) -2![_ * t^-1]mulgA.
have Dt1 si: si \in P0 -> t^-1 = (s^-1 ^ si) ^ y.
by move=> P0si; rewrite {2}/conjg -conjVg -(abP0 si) ?groupV ?mulKg.
by rewrite {1}(Dt1 s1) // (Dt1 s3^-1) ?groupV // -conjXg /conjg !{1}gnorm.
rewrite {1}(Dt1 s1) // (Dt1 s3^-1) ?groupV // -conjXg /conjg.
by rewrite !mulgA !invgK !invMg !invgK !mulgA !mulgKV mulg1.
have{Dx memQP0} Dx1: x = 1.
apply/set1P; rewrite -set1gE; have [_ _ _ <-] := dprodP defQ.
rewrite setIAC (setIidPr sQP0_Q) inE -{2}defP0 -cycleV cent_cycle.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection11.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -164,7 +164,7 @@ move=> notMg sAMg; set Ms := M`_\sigma; set H := [group of Ms :&: M :^ g].
have [H1 | ntH] := eqsVneq H 1.
by split=> //; apply/trivgP; rewrite -H1 setIS //= centJ conjSg.
pose q := pdiv #|H|.
suffices: #|H|`_q == 1%N by rewrite p_part_eq1 pi_pdiv cardG_gt1 ntH.
suffices: (#|H|`_q)%N == 1%N by rewrite p_part_eq1 pi_pdiv cardG_gt1 ntH.
have nsMsM: Ms <| M := pcore_normal _ _; have [_ nMsM] := andP nsMsM.
have sHMs: H \subset Ms := subsetIl _ _.
have sHMsg: H \subset Ms :^ g.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection12.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,7 @@ have{groupE21} defE: E3 ><| (E2 ><| E1) = E.
apply/eqP; rewrite eqEcard mul_subG // coprime_cardMg //= -defE21.
rewrite -(partnC \tau3(M) (cardG_gt0 E)) (card_Hall hallE3) leq_mul //.
rewrite coprime_cardMg // (card_Hall hallE1) (card_Hall hallE2).
rewrite -[#|E|`__](partnC \tau2(M)) ?leq_mul ?(partn_part _ tau3'2) //.
rewrite -[(#|E|`__)%N](partnC \tau2(M)) ?leq_mul ?(partn_part _ tau3'2) //.
rewrite -partnI dvdn_leq // sub_in_partn // => p piEp; apply/implyP.
rewrite inE /= -negb_or /= orbC implyNb orbC.
by rewrite -(partition_pi_sigma_compl maxM hallE).
Expand Down
5 changes: 3 additions & 2 deletions theories/BGsection4.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,10 +75,11 @@ have{fS gS} expMR_fg: {in R &, forall u v n (r := [~ v, u]),
have ->: [~ v ^+ n, u] = r ^+ n * [~ r, v] ^+ 'C(n, 2).
elim: n => [|n IHn]; first by rewrite comm1g mulg1.
rewrite !expgS commMgR -/r {}IHn commgX; last exact: cRr.
rewrite binS bin1 addnC expgD -2!mulgA; congr (_ * _); rewrite 2!mulgA.
rewrite binS bin1 addnC expgD -mulgA -[RHS]mulgA; congr (_ * _); rewrite 2!mulgA.
by rewrite commuteX2 // /commute cRr.
rewrite commXg 1?commuteX2 -?[_ * v]commuteX; try exact: cRr.
rewrite mulgA {1}[mulg]lock mulgA -mulgA -(mulgA v) -!expgD -fS -lock.
rewrite mulgA {1}[mulg]lock [in LHS]mulgA -(mulgA _ (r ^+ n)) -(mulgA v).
rewrite -!expgD -fS -lock.
rewrite -{2}(bin1 n) addnC -binS -2!mulgA (mulgA _ v) (commgC _ v).
rewrite -commuteX; last by red; rewrite cRr ?(Rr, groupR, groupX, groupM).
rewrite -3!mulgA; congr (_ * (_ * _)); rewrite 2!mulgA.
Expand Down
19 changes: 11 additions & 8 deletions theories/BGsection7.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -77,17 +77,20 @@ elim: n => // n IHn in gT G *; rewrite ltnS => leGn oddG.
have oG: #|[subg G]| = #|G| by rewrite (card_isog (isog_subg G)).
apply/idPn=> nsolG; apply: IH_FT.
pose gT' : finGroupType := subg_of G.
apply: (HB.pack gT' (IsMinSimpleOddGroup.Build gT' _ _ _ _));
do ?[move=> /= ??????].
- by rewrite oG.
- rewrite -(isog_simple (isog_subg _)); apply/simpleP; split=> [|H nsHG].
have godd: odd #|[set: [subg G]]| by rewrite oG.
have gsimp: simple [set: [subg G]].
rewrite -(isog_simple (isog_subg _)).
apply/simpleP; split=> [|H nsHG].
by apply: contra nsolG; move/eqP->; rewrite abelian_sol ?abelian1.
have [sHG _]:= andP nsHG; apply/pred2P; apply: contraR nsolG; case/norP=> ntH.
rewrite eqEcard sHG -ltnNge (series_sol nsHG) => ltHG.
by rewrite !IHn ?(oddSg sHG) ?quotient_odd ?(leq_trans _ leGn) ?ltn_quotient.
- by apply: contra nsolG => solG; rewrite -(im_sgval G) morphim_sol.
move=> M; rewrite properEcard oG; case/andP=> sMG ltMG.
by apply: IHn (leq_trans ltMG leGn) (oddSg sMG _); rewrite oG.
have gsol: ~~ solvable [set: [subg G]].
by apply: contra nsolG => solG; rewrite -(im_sgval G) morphim_sol.
have gmin (M : {group [subg G]}) : M \proper [set: [subg G]] -> solvable M.
rewrite properEcard oG; case/andP=> sMG ltMG.
by apply: IHn (leq_trans ltMG leGn) (oddSg sMG _); rewrite oG.
exact: (HB.pack gT' (IsMinSimpleOddGroup.Build gT' godd gsimp gsol gmin)).
Qed.

Lemma minSimpleOdd_prime gT (G : {group gT}) :
Expand Down Expand Up @@ -731,7 +734,7 @@ have [qQ2 nQ2P] := mem_max_normed maxQ2.
have hallP: pi.-Hall('N_KBP(Q2)) P.
have sPN: P \subset 'N_KBP(Q2) by rewrite subsetI joing_subr.
rewrite pHallE eqn_leq -{1}(part_pnat_id piP) dvdn_leq ?partn_dvd ?cardSg //.
have ->: #|P| = #|KBP|`_pi.
have ->: #|P| = (#|KBP|`_pi)%N.
rewrite /KBP joingC norm_joinEl // coprime_cardMg ?(pnat_coprime piP) //.
by rewrite partnM // part_pnat_id // part_p'nat // muln1.
by rewrite sPN dvdn_leq ?partn_dvd ?cardSg ?cardG_gt0 ?subsetIl.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection8.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -329,7 +329,7 @@ have{} p'nbyA_1 X:
have [R] := max_normed_exists (pcore_pgroup q X) (gFnorm_trans _ nXA).
by rewrite p'nbyA_1 // => /set1P->.
apply/subsetPn=> -[H0 MA_H0 neH0M].
pose H := [arg max_(H > H0 | (H \in 'M(A)) && (H != M)) #|H :&: M|`_p].
pose H := [arg max_(H > H0 | (H \in 'M(A)) && (H != M)) (#|H :&: M|`_p)%N].
case: arg_maxnP @H => [|H {H0 MA_H0 neH0M}]; first by rewrite MA_H0 -in_set1.
rewrite /= inE -andbA => /and3P[maxH sAH neHM] maxHM.
have prH: H \proper G by rewrite inE in maxH; apply: maxgroupp maxH.
Expand Down
2 changes: 1 addition & 1 deletion theories/BGsection9.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -37,7 +37,7 @@ move=> maxM /pElemP[sBM abelB] ncycB snbBp'_M; have [pB cBB _] := and3P abelB.
have prM := mmax_proper maxM; have solM := mFT_sol prM.
apply/uniq_mmaxP; exists M; symmetry; apply/eqP.
rewrite eqEsubset sub1set inE maxM sBM; apply/subsetPn=> [[H0 MB_H0 neH0M]].
have:= erefl [arg max_(H > H0 | (H \in 'M(B)) && (H :!=: M)) #|H :&: M|`_p].
have:= erefl [arg max_(H > H0 | (H \in 'M(B)) && (H :!=: M)) (#|H :&: M|`_p)%N].
have [|H] := arg_maxnP; first by rewrite MB_H0; rewrite inE in neH0M.
rewrite inE -andbA => /and3P[maxH sBH neHM] maxHM _ {H0 MB_H0 neH0M}.
have sB_HM: B \subset H :&: M by rewrite subsetI sBH.
Expand Down
Loading