proposition: Proposition coprime_abelian_gen_cent gT (A G : {group gT}) : abelian A -> A \subset 'N(G) -> coprime #|G| #|A| -> <<\bigcup_(B : {group gT} | cyclic (A / B) && (B <| A)) 'C_G(B)>> = G.
proof: Proof. move=> abelA nGA coGA; symmetry; move: {2}_.+1 (ltnSn #|G|) => n. elim: n gT => // n IHn gT in A G abelA nGA coGA *; rewrite ltnS => leGn. without loss nilG: G nGA coGA leGn / nilpotent G. move=> {} IHn; apply/eqP; rewrite eqEsubset gen_subG. apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl. pose T := [set P : {group gT} | Sylow G P & A \subset 'N(P)]. rewrite -{1}(@Sylow_transversal_gen _ T G) => [|P | p _]; first 1 last. - by rewrite inE -!andbA; case/and4P. - have [//|P sylP nPA] := sol_coprime_Sylow_exists p (abelian_sol abelA) nGA. by exists P; rewrite ?inE ?(p_Sylow sylP). rewrite gen_subG; apply/bigcupsP=> P {T}/setIdP[/SylowP[p _ sylP] nPA]. have [sPG pP _] := and3P sylP. rewrite (IHn P) ?(pgroup_nil pP) ?(coprimeSg sPG) ?genS //. by apply/bigcupsP=> B cycBq; rewrite (bigcup_max B) ?setSI. by rewrite (leq_trans (subset_leq_card sPG)). apply/eqP; rewrite eqEsubset gen_subG. apply/andP; split; last by apply/bigcupsP=> B _; apply: subsetIl. have [Z1 | ntZ] := eqsVneq 'Z(G) 1. by rewrite (TI_center_nil _ (normal_refl G)) ?Z1 ?(setIidPr _) ?sub1G. have{ntZ} [M /= minM] := minnormal_exists ntZ (gFnorm_trans _ nGA). rewrite subsetI centsC => /andP[sMG /cents_norm nMG]. have coMA := coprimeSg sMG coGA; have{nilG} solG := nilpotent_sol nilG. have [nMA ntM abelM] := minnormal_solvable minM sMG solG. set GC := <<_>>; have sMGC: M \subset GC. rewrite sub_gen ?(bigcup_max 'C_A(M)%G) //=; last first. by rewrite subsetI sMG centsC subsetIr. case/is_abelemP: abelM => p _ abelM; rewrite -(rker_abelem abelM ntM nMA). rewrite rker_normal -(setIidPl (quotient_abelian _ _)) ?center_kquo_cyclic //. exact/abelem_mx_irrP. rewrite -(quotientSGK nMG sMGC). have: A / M \subset 'N(G / M) by rewrite morphim_norms. move/IHn->; rewrite ?morphim_abelian ?coprime_morph {IHn}//; first 1 last. by rewrite (leq_trans _ leGn) ?ltn_quotient. rewrite gen_subG; apply/bigcupsP=> Bq; rewrite andbC => /andP[]. have: M :&: A = 1 by rewrite coprime_TIg. move/(quotient_isom nMA); case/isomP=> /=; set qM := restrm _ _ => injqM <-. move=> nsBqA; have sBqA := normal_sub nsBqA. rewrite -(morphpreK sBqA) /= -/qM; set B := qM @*^-1 Bq. move: nsBqA; rewrite -(morphpre_normal sBqA) ?injmK //= -/B => nsBA. rewrite -(morphim_quotm _ nsBA) /= -/B injm_cyclic ?injm_quotm //= => cycBA. rewrite morphim_restrm -quotientE morphpreIdom -/B; have sBA := normal_sub nsBA. rewrite -coprime_quotient_cent ?(coprimegS sBA, subset_trans sBA) //= -/B. by rewrite quotientS ?sub_gen // (bigcup_max [group of B]) ?cycBA. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)