proposition: Lemma FTtype34_Fcore_kernel_trivial : [/\ p.-abelem H, #|H| = (p ^ q)%N & `H0 = 1%g].
proof: Proof. have [[_ _ nHU tiHU] [pH cH0U defH' _]] := (sdprodP defHU, FTtype34_facts). have [/mulG_sub[_ sW1M] nH0H] := (sdprodW defM, normal_norm nsH0H). have nHW1: W1 \subset 'N(H) := subset_trans sW1M (gFnorm _ M). have nUW1: W1 \subset 'N(U) by have [_ []] := MtypeP. pose bar := coset_morphism H0; pose Hbar := (H / H0)%g; pose Ubar := (U / H0)%g. have [Cbar_neqU _ /= oHbar] := Ptype_Fcore_factor_facts maxM MtypeP notMtype5. rewrite -/Hbar def_p // -/q in oHbar. have [nH0U nH0W1] := (subset_trans sUM nH0M, subset_trans sW1M nH0M). suffices H0_1 : `H0 = 1%g. have isoHbar: H \isog H / H0 by rewrite H0_1 quotient1_isog. by rewrite (isog_abelem isoHbar) (card_isog isoHbar). apply: contraNeq Cbar_neqU => ntH0; rewrite [Ptype_Fcompl_kernel _]unlock. suffices: Hbar \subset 'C(Ubar). by rewrite (sameP eqP setIidPl) sub_astabQ nH0U centsC. have pH0 := pgroupS sH0H pH; have{ntH0} [_ _ [k oH0]] := pgroup_pdiv pH0 ntH0. have{k oH0} [Q maxQ nsQH]: exists2 Q : {group gT}, maximal Q H0 & Q <| H. have [Q [sQH0 nsQH oQ]] := normal_pgroup pH nsH0H (leq_pred _). exists Q => //; apply: p_index_maximal => //. by rewrite -divgS // oQ oH0 pfactorK //= expnS mulnK ?expn_gt0 ?cardG_gt0. have nsQH0: Q <| H0 := p_maximal_normal (pgroupS sH0H pH) maxQ. have [[sQH0 nQH0] nQH] := (andP nsQH0, normal_norm nsQH). have nQU: U \subset 'N(Q) by rewrite cents_norm ?(centsS sQH0). pose hat := coset_morphism Q; pose Hhat := (H / Q)%g; pose H0hat := (H0 / Q)%g. have{maxQ} oH0hat: #|H0hat| = p by rewrite card_quotient ?(p_maximal_index pH0). have defHhat': Hhat^`(1)%g = H0hat by rewrite -quotient_der -?defH'. have ntH0hat: H0hat != 1%g by rewrite -cardG_gt1 oH0hat prime_gt1. have pHhat: p.-group Hhat by apply: quotient_pgroup. have nsH0Hhat: H0hat <| Hhat by apply: quotient_normal. have sH0hatZ: H0hat \subset 'Z(Hhat). by rewrite prime_meetG ?oH0hat // meet_center_nil ?(pgroup_nil pHhat). have{pHhat} gal'M: ~~ typeP_Galois MtypeP. have sZHhat: 'Z(Hhat) \subset Hhat := center_sub _. have nsH0hatZ: H0hat <| 'Z(Hhat) := normalS sH0hatZ sZHhat nsH0Hhat. have [f injf im_f] := third_isom sQH0 nsQH nsH0H. have fHhat: f @* (Hhat / H0hat) = Hbar by rewrite im_f. apply: contra (odd (logn p #|Hhat|)) _ _; last first. rewrite -(divnK (cardSg (quotientS Q sH0H))) divg_normal // oH0hat. by rewrite -(card_injm injf) // fHhat oHbar -expnSr pfactorK //= mFT_odd. rewrite /typeP_Galois acts_irrQ // => /mingroupP[_ minUHbar]. suffices /(card_extraspecial pHhat)[n _ ->]: extraspecial Hhat. by rewrite pfactorK //= odd_double. have abelH: p.-abelem (Hhat / H0hat)%g by rewrite -(injm_abelem injf) ?fHhat. suffices{abelH} defZHhat: 'Z(Hhat) = H0hat. do 2?split; rewrite defZHhat ?oH0hat //. apply/eqP; rewrite eqEsubset (Phi_min pHhat) ?normal_norm //=. by rewrite (Phi_joing pHhat) defHhat' joing_subl. apply: contraNeq ntH0hat; rewrite eqEsubset sH0hatZ andbT => not_esHhat. rewrite -defHhat'; apply/eqP/derG1P/center_idP/(quotient_inj nsH0hatZ)=> //. apply: (injm_morphim_inj injf); rewrite ?quotientS //= fHhat -/Hhat -/H0hat. rewrite minUHbar //= -/Hbar -?fHhat 1?morphim_injm_eq1 ?morphimS // -subG1. rewrite quotient_sub1 ?(normal_norm nsH0hatZ) // not_esHhat -['Z(_)]cosetpreK. rewrite im_f ?sub_cosetpre_quo // quotient_norms ?norm_quotient_pre //. by rewrite gFnorm_trans ?quotient_norms. have [H1 []] := typeP_Galois_Pn maxM notMtype5 gal'M. rewrite def_p => oH1 nH1Ubar _ /bigdprodWY-defHbar _. have /cyclicP[xbar defH1]: cyclic H1 by rewrite prime_cyclic ?oH1. have H1xbar: xbar \in H1 by rewrite defH1 cycle_id. have sH1_Hbar: H1 \subset Hbar. by rewrite -[Hbar]defHbar (bigD1 1%g) ?group1 ?conjsg1 ?joing_subl. have{sH1_Hbar} Hxbar: xbar \in Hbar := subsetP sH1_Hbar xbar H1xbar. have /morphimP[x nH0x Hx /= Dxbar] := Hxbar. have{oH1} oxbar: #[xbar] = p by rewrite orderE -defH1. have memH0: {in H &, forall y z, [~ y, z] \in H0}. by rewrite defH'; apply: mem_commg. have [_ /centsP-cHH0hat] := subsetIP sH0hatZ; move/subsetP in nQH. pose D y z := [~ hat z, hat y]. have D_H0_1 y z: y \in H -> z \in H0 -> D y z = 1%g. by move=> Hy H0z; apply/eqP/commgP/cHH0hat; apply: mem_quotient. have H0_D: {in H &, forall y z, D y z \in H0hat}. by move=> y z Hy Hz; rewrite -defHhat' mem_commg ?mem_quotient. have Dsym y z: (D y z)^-1%g = D z y by rewrite invg_comm. have Dmul y: y \in H -> {in H &, {morph D y: z t / z * t}}%g. move=> Hy z t Hz Ht; rewrite {1}/D morphM ?nQH // commMgR; congr (_ * _)%g. by rewrite -{2}morphR ?nQH // -/(D t _) D_H0_1 ?memH0 // mulg1. pose Dm y Hy : {morphism H >-> coset_of Q} := Morphism (Dmul y Hy). have{D_H0_1} kerDmH0 y Hy: H0 \subset 'ker (Dm y Hy). by rewrite subsetI sH0H; apply/subsetP=> z H0z; rewrite !inE /= D_H0_1. pose x_ w := (x ^ w)%g; pose xbar_ w := (xbar ^ bar w)%g. move/subsetP in nHW1; move/subsetP in nHU. have Hx_ w: w \in W1 -> (x_ w \in H) * {in U, forall u, x_ w ^ u \in H}%g. by move/nHW1=> nHw; split=> [|u /nHU-nHu]; rewrite !memJ_norm. have Dx: {in H &, forall y z, {in W1, forall w, D (x_ w) y = 1} -> D y z = 1}%g. move=> y z Hy Hz Dxy1; apply/(kerP (Dm y Hy) Hz); apply: subsetP z Hz. rewrite -(quotientSGK nH0H) ?kerDmH0 // -defHbar gen_subG. apply/bigcupsP=> _ /morphimP[w nH0w W1w ->] /=. rewrite defH1 Dxbar -quotient_cycle -?quotientJ ?quotientS // -cycleJ. by rewrite cycle_subG !inE /= Hx_ //= -Dsym eq_invg1 Dxy1. pose ntrivD := [exists w in [predX W1 & W1], #[D (x_ w.1) (x_ w.2)] == p]. have{ntrivD Dx} /exists_inP[[w1 w2] /andP/=[Ww1 Ww2] /eqP-oDx12]: ntrivD. apply: contraR ntH0hat => Dx_1; rewrite -defHhat' -subG1 gen_subG. apply/subsetP=> _ /imset2P[_ _ /morphimP[y ? Hy ->] /morphimP[z ? Hz ->] ->]. apply/set1P/Dx=> // w2 Ww2; rewrite Dx ?Hx_ // => w1 Ww1. have abelH0hat: p.-abelem H0hat by apply: prime_abelem. apply: contraNeq Dx_1 => /(abelem_order_p abelH0hat)oDx12. by apply/exists_inP; exists (w1, w2); rewrite ?inE ?Ww1 // oDx12 ?H0_D ?Hx_. have /subsetP-nUW1bar: (W1 / H0)%g \subset 'N(Ubar) := quotient_norms H0 nUW1. move/subsetP in nH0H; move/subsetP in nH0W1. pose n (phi : {morphism Ubar >-> {unit 'F_p}}) ubar : nat := val (phi ubar). have [phi Dphi]: {phi | {in Ubar, forall ub, xbar ^ ub =xbar ^+ n phi ub}}%g. pose xbar_Autm := invm (injm_Zp_unitm xbar). have /restrmP[phi [Dphi _ _ _]]: Ubar \subset 'dom (xbar_Autm \o conj_aut H1). by rewrite -sub_morphim_pre //= im_Zp_unitm -defH1 Aut_conj_aut. rewrite /n pdiv_id // -oxbar; exists phi => ubar /(subsetP nH1Ubar)Uubar. transitivity (Zp_unitm (phi ubar) xbar); last by rewrite autE /= -?defH1. by rewrite Dphi invmK ?im_Zp_unitm -?defH1 ?Aut_aut ?norm_conj_autE. pose QV ubar w := (ubar ^ (bar w)^-1)%g. have UbarQV: {in Ubar & W1, forall ubar w, QV ubar w \in Ubar}. by move=> ub w Uub W1w; rewrite /= memJ_norm ?groupV ?nUW1bar ?mem_quotient. pose phi_ w ub := phi (QV ub w); pose nphi_ w ub := n phi (QV ub w). have xbarJ: {in W1 & Ubar, forall w ub, xbar_ w ^ ub = xbar_ w ^+ nphi_ w ub}%g. by move=> w ubar * /=; rewrite -conjgM conjgCV conjgM Dphi ?UbarQV // conjXg. have{oDx12} phi_w12 ubar: ubar \in Ubar -> (phi_ w1 ubar * phi_ w2 ubar = 1)%g. pose n_u := nphi_ ^~ ubar => Uubar; have [u nH0u Uu Dubar] := morphimP Uubar. suffices: n_u w1 * n_u w2 == 1 %[mod #[D (x_ w1) (x_ w2)]]. by apply: contraTeq; rewrite oDx12 -!val_Fp_nat // natrM !natr_Zp. have DXn: {in H & W1, forall y w, D y (x_ w) ^+ n_u w = D y (x_ w ^ u)}%g. move=> y w Hy W1w; set z := x_ w; have [Hz /(_ u Uu) Hzu] := Hx_ w W1w. rewrite -(morphX (Dm y Hy)) //; apply/rcoset_kerP; rewrite ?groupX //. have /subsetP: H0 :* z ^ u \subset 'ker (Dm y Hy) :* z ^ u by rewrite mulSg. apply; apply/rcoset_kercosetP; rewrite ?groupX ?nH0H //. by rewrite morphX ?morphJ ?(nH0W1 w) // ?nH0H //= -Dubar -Dxbar xbarJ. rewrite -eq_expg_mod_order -{1}Dsym expgM expgVn ?(DXn, Dsym) ?Hx_ //. rewrite /D -!morphR ?nQH ?Hx_ // -conjRg (conjg_fixP _) //. by apply/commgP/esym/(centsP cH0U); rewrite ?memH0 ?Hx_. pose wbar := bar (w1 * w2 ^-1)%g; pose W1bar := (W1 / H0)%g. have W1wbar: wbar \in W1bar by rewrite mem_quotient ?groupM ?groupV. have{phi_w12} phiJ: {in Ubar, forall ubar, phi (ubar ^ wbar) = (phi ubar)^-1}%g. move=> ubar Uubar; apply/esym/eqP; rewrite eq_invg_mul. rewrite [wbar]morphM ?morphV ?nH0W1 ?groupV // -{1}[ubar](conjgK (bar w1)). by rewrite conjgM phi_w12 // memJ_norm ?nUW1bar ?mem_quotient. have coW1bar2: coprime #|W1bar| 2 by rewrite coprimen2 quotient_odd ?mFT_odd. have coUbar2: coprime #|Ubar| 2 by rewrite coprimen2 quotient_odd ?mFT_odd. have{wbar phiJ W1wbar} phiV: {in Ubar, forall ubar, phi ubar = (phi ubar)^-1}%g. move=> ubar Uubar; rewrite /= -phiJ // -(expgK coW1bar2 W1wbar) -expgM mul2n. elim: (expg_invn _ _) => [|k IHk]; first by rewrite conjg1. by do 2!rewrite expgSr conjgM phiJ ?memJ_norm ?nUW1bar ?groupX // ?invgK. rewrite -[Hbar]defHbar gen_subG defH1; apply/bigcupsP=> _ /morphimP[w _ Ww ->]. rewrite -cycleJ cycle_subG -/(xbar_ _); apply/centP=> ubar Uubar; apply/commgP. apply/conjg_fixP; rewrite xbarJ // /nphi_ -[QV _ w](expgK coUbar2) ?UbarQV //. by rewrite /n !morphX ?groupX 1?expgS 1?{1}phiV ?UbarQV // mulVg expg1n. 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 finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10)