proposition: Lemma Aut_extraspecial_full : Aut_in (Aut S) 'Z(S) \isog Aut 'Z(S).
proof: Proof. have [p_gt1 p_gt0] := (prime_gt1 p_pr, prime_gt0 p_pr). have [Es] := extraspecial_structure pS esS. elim: Es S oZ => [T _ _ <-| E s IHs T oZT] /=. rewrite big_nil cprod1g (center_idP (center_abelian T)). by apply/Aut_sub_fullP=> // g injg gZ; exists g. rewrite -andbA big_cons -cprodA => /and3P[/eqP-oE /eqP-defZE es_s]. case/cprodP=> -[_ U _ defU]; rewrite defU => defT cEU. have sUT: U \subset T by rewrite -defT mulG_subr. have sZU: 'Z(T) \subset U. by case/cprodP: defU => [[V _ -> _] <- _]; apply: mulG_subr. have defZU: 'Z(E) = 'Z(U). apply/eqP; rewrite eqEsubset defZE subsetI sZU subIset ?centS ?orbT //=. by rewrite subsetI subIset ?sUT //= -defT centM setSI. apply: (Aut_cprod_full _ defZU); rewrite ?cprodE //; last first. by apply: IHs; rewrite -?defZU ?defZE. have oZE: #|'Z(E)| = p by rewrite defZE. have [p2 | odd_p] := even_prime p_pr. suffices <-: restr_perm 'Z(E) @* Aut E = Aut 'Z(E) by apply: Aut_in_isog. apply/eqP; rewrite eqEcard restr_perm_Aut ?center_sub //=. by rewrite card_Aut_cyclic ?prime_cyclic ?oZE // {1}p2 cardG_gt0. have pE: p.-group E by rewrite /pgroup oE pnatX pnat_id. have nZE: E \subset 'N('Z(E)) by rewrite normal_norm ?center_normal. have esE: extraspecial E := card_p3group_extraspecial p_pr oE oZE. have [[defPhiE defE'] prZ] := esE. have{defPhiE} sEpZ x: x \in E -> (x ^+ p)%g \in 'Z(E). move=> Ex; rewrite -defPhiE (Phi_joing pE) mem_gen // inE orbC. by rewrite (Mho_p_elt 1) // (mem_p_elt pE). have ltZE: 'Z(E) \proper E by rewrite properEcard subsetIl oZE oE (ltn_exp2l 1). have [x [Ex notZx oxp]]: exists x, [/\ x \in E, x \notin 'Z(E) & #[x] %| p]%N. have [_ [x Ex notZx]] := properP ltZE. case: (prime_subgroupVti <[x ^+ p]> prZ) => [sZxp | ]; last first. move/eqP; rewrite (setIidPl _) ?cycle_subG ?sEpZ //. by rewrite cycle_eq1 -order_dvdn; exists x. have [y Ey notxy]: exists2 y, y \in E & y \notin <[x]>. apply/subsetPn; apply: contra (extraspecial_nonabelian esE) => sEx. by rewrite (abelianS sEx) ?cycle_abelian. have: (y ^+ p)%g \in <[x ^+ p]> by rewrite (subsetP sZxp) ?sEpZ. case/cycleP=> i def_yp; set xi := (x ^- i)%g. have Exi: xi \in E by rewrite groupV groupX. exists (y * xi)%g; split; first by rewrite groupM. have sxpx: <[x ^+ p]> \subset <[x]> by rewrite cycle_subG mem_cycle. apply: contra notxy; move/(subsetP (subset_trans sZxp sxpx)). by rewrite groupMr // groupV mem_cycle. pose z := [~ xi, y]; have Zz: z \in 'Z(E) by rewrite -defE' mem_commg. case: (setIP Zz) => _; move/centP=> cEz. rewrite order_dvdn expMg_Rmul; try by apply: commute_sym; apply: cEz. rewrite def_yp expgVn -!expgM mulnC mulgV mul1g -order_dvdn. by rewrite (dvdn_trans (order_dvdG Zz)) //= oZE bin2odd // dvdn_mulr. have{oxp} ox: #[x] = p. apply/eqP; case/primeP: p_pr => _ dvd_p; case/orP: (dvd_p _ oxp) => //. by rewrite order_eq1; case: eqP notZx => // ->; rewrite group1. have [y Ey not_cxy]: exists2 y, y \in E & y \notin 'C[x]. by apply/subsetPn; rewrite sub_cent1; rewrite inE Ex in notZx. have notZy: y \notin 'Z(E). apply: contra not_cxy; rewrite inE Ey; apply: subsetP. by rewrite -cent_set1 centS ?sub1set. pose K := 'C_E[y]; have maxK: maximal K E by apply: cent1_extraspecial_maximal. have nsKE: K <| E := p_maximal_normal pE maxK; have [sKE nKE] := andP nsKE. have oK: #|K| = (p ^ 2)%N. by rewrite -(divg_indexS sKE) oE (p_maximal_index pE) ?mulKn. have cKK: abelian K := card_p2group_abelian p_pr oK. have sZK: 'Z(E) \subset K by rewrite setIS // -cent_set1 centS ?sub1set. have defE: K ><| <[x]> = E. have notKx: x \notin K by rewrite inE Ex cent1C. rewrite sdprodE ?(mulg_normal_maximal nsKE) ?cycle_subG ?(subsetP nKE) //. by rewrite setIC prime_TIg -?orderE ?ox ?cycle_subG. have /cyclicP[z defZ]: cyclic 'Z(E) by rewrite prime_cyclic ?oZE. apply/(Aut_sub_fullP (center_sub E)); rewrite /= defZ => g injg gZ. pose k := invm (injm_Zp_unitm z) (aut injg gZ). have fM: {in K &, {morph expgn^~ (val k): u v / u * v}}. by move=> u v Ku Kv; rewrite /= expgMn // /commute (centsP cKK). pose f := Morphism fM; have fK: f @* K = K. apply/setP=> u; rewrite morphimEdom. apply/imsetP/idP=> [[v Kv ->] | Ku]; first exact: groupX. exists (u ^+ expg_invn K (val k)); first exact: groupX. rewrite /f /= expgAC expgK // oK coprimeXl // -unitZpE //. by case: (k) => /=; rewrite orderE -defZ oZE => j; rewrite natr_Zp. have fMact: {in K & <[x]>, morph_act 'J 'J f (idm <[x]>)}. by move=> u v _ _; rewrite /= conjXg. exists (sdprodm_morphism defE fMact). rewrite im_sdprodm injm_sdprodm injm_idm -card_im_injm im_idm fK. have [_ -> _ ->] := sdprodP defE; rewrite !eqxx; split=> //= u Zu. rewrite sdprodmEl ?(subsetP sZK) ?defZ // -(autE injg gZ Zu). rewrite -[aut _ _](invmK (injm_Zp_unitm z)); first by rewrite permE Zu. by rewrite im_Zp_unitm Aut_aut. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)