proposition: Lemma strongest_coprime_quotient_cent A G H : let R := H :&: [~: G, A] in A \subset 'N(H) -> R \subset G -> coprime #|R| #|A| -> solvable R || solvable A -> 'C_G(A) / H = 'C_(G / H)(A / H).
proof: Proof. move=> R nHA sRG coRA solRA. have nRA: A \subset 'N(R) by rewrite normsI ?commg_normr. apply/eqP; rewrite eqEsubset subsetI morphimS ?subsetIl //=. rewrite (subset_trans _ (morphim_cent _ _)) ?morphimS ?subsetIr //=. apply/subsetP=> _ /setIP[/morphimP[x Nx Gx ->] cAHx]. have{cAHx} cAxR y: y \in A -> [~ x, y] \in R. move=> Ay; have Ny: y \in 'N(H) by apply: subsetP Ay. rewrite inE mem_commg // andbT coset_idr ?groupR // morphR //=. by apply/eqP; apply/commgP; apply: (centP cAHx); rewrite mem_quotient. have AxRA: A :^ x \subset R * A. apply/subsetP=> _ /imsetP[y Ay ->]. rewrite -normC // -(mulKVg y (y ^ x)) -commgEl mem_mulg //. by rewrite -groupV invg_comm cAxR. have [y Ry def_Ax]: exists2 y, y \in R & A :^ x = A :^ y. have oAx: #|A :^ x| = #|A| by rewrite cardJg. have [solR | solA] := orP solRA; first exact: SchurZassenhaus_trans_sol. by apply: SchurZassenhaus_trans_actsol; rewrite // joingC norm_joinEr. rewrite -imset_coset; apply/imsetP; exists (x * y^-1); last first. by rewrite conjgCV mkerl // ker_coset memJ_norm groupV; case/setIP: Ry. rewrite /= inE groupMl // ?(groupV, subsetP sRG) //=. apply/centP=> z Az; apply/commgP/eqP/set1P. rewrite -[[set 1]](coprime_TIg coRA) inE {1}commgEl commgEr /= -/R. rewrite invMg -mulgA invgK groupMl // conjMg mulgA -commgEl. rewrite groupMl ?cAxR // memJ_norm ?(groupV, subsetP nRA) // Ry /=. by rewrite groupMr // conjVg groupV conjgM -mem_conjg -def_Ax memJ_conjg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)