proposition: Theorem solvable_Wielandt_fixpoint (I : finType) gT (A : I -> {group gT}) (n m : I -> nat) (G V : {group gT}) : (forall i, m i + n i > 0 -> A i \subset G) -> G \subset 'N(V) -> coprime #|V| #|G| -> solvable V -> {in G, forall a, \sum_(i | a \in A i) m i = \sum_(i | a \in A i) n i}%N -> (\prod_i #|'C_V(A i)| ^ (m i * #|A i|) = \prod_i #|'C_V(A i)| ^ (n i * #|A i|))%N.
proof: Proof. move: {2}_.+1 (ltnSn #|V|) => c leVc sA_G nVG coVG solV partG; move: leVc. pose nz_k i := (0 < m i + n i)%N; rewrite !(bigID nz_k xpredT) /= {2 4}/nz_k. rewrite !(big1 _ (predC _)) /= => [|i|i]; try by case: (m i) (n i) => [[]|]. pose sum_k A_ a k := (\sum_(i | (a \in (A_ i : {set _})) && nz_k i) k i)%N. have{} partG: {in G, forall a, sum_k _ A a m = sum_k _ A a n}. move=> a /partG; rewrite !(bigID nz_k (fun i => a \in _)) -!/(sum_k _ A a _). by rewrite /= !big1 ?addn0 /nz_k // => i /andP[_]; case: (m i) (n i) => [[]|]. rewrite !muln1; elim: c => // c IHc in gT G A V nVG coVG solV partG sA_G *. rewrite ltnS => leVc; have [-> | ntV] := eqsVneq V 1. by rewrite !big1 // => i _; rewrite setI1g cards1 exp1n. have nsVVG: V <| V <*> G by rewrite normalYl. without loss{c leVc IHc} minV: / minnormal V (V <*> G). have [B minB sBV]: {B : {group gT} | minnormal B (V <*> G) & B \subset V}. by apply: mingroup_exists; rewrite ntV normal_norm. have [nBVG ntB abB] := minnormal_solvable minB sBV solV. have [nBV nBG] := joing_subP nBVG; have solB := solvableS sBV solV. have [{1}<- -> // | ltBV _] := eqVproper sBV. have ltBc: #|B| < c := leq_trans (proper_card ltBV) leVc. have coBG: coprime #|B| #|G| := coprimeSg sBV coVG. have factorCA_B k i: nz_k i -> (#|'C_B(A i)| ^ (k i * #|A i|) * #|'C_(V / B)(A i / B)| ^ (k i * #|A i / B|) = #|'C_V(A i)| ^ (k i * #|A i|))%N. - move/sA_G => sAiG; have nBAi := subset_trans sAiG nBG. have [coVAi coBAi] := (coprimegS sAiG coVG, coprimegS sAiG coBG). rewrite -(card_isog (quotient_isog _ _)) ?(coprime_TIg coBAi) // -expnMn. rewrite -coprime_quotient_cent // -{1}(setIidPr sBV) setIAC. by rewrite card_quotient ?LagrangeI // subIset ?nBV. rewrite -!{1}(eq_bigr _ (factorCA_B _)) {factorCA_B} !big_split /=. pose A_B i := A i / B; congr (_ * _)%N; first exact: (IHc _ G). have: #|V / B| < c by apply: leq_trans leVc; rewrite ltn_quotient. have (i): nz_k i -> A i / B \subset G / B by move/sA_G/quotientS->. apply: IHc; rewrite ?morphim_sol ?coprime_morph ?quotient_norms //. move=> _ /morphimP[a Na Ga ->]. suffices eqAB: sum_k _ A_B (coset B a) =1 sum_k _ A a by rewrite !eqAB partG. move=> k; apply: eq_bigl => i; apply: andb_id2r => /sA_G sAiG. rewrite -sub1set -quotient_set1 // quotientSK ?sub1set //. by rewrite -{2}(mul1g (A i)) -(coprime_TIg coBG) setIC group_modr // inE Ga. have /is_abelemP[p p_pr abelV] := minnormal_solvable_abelem minV solV. have [p_gt1 [pV cVV _]] := (prime_gt1 p_pr, and3P abelV). have{} minV: minnormal V G. apply/mingroupP; split=> [|B nBG sBV]; first by rewrite ntV nVG. by case/mingroupP: minV => _ -> //; rewrite join_subG (sub_abelian_norm cVV). have co_pG: coprime p #|G|. by have [_ _ [e oV]] := pgroup_pdiv pV ntV; rewrite oV coprime_pexpl in coVG. have p'G: p^'.-group G by rewrite pgroupE p'natE -?prime_coprime. pose rC i := logn p #|'C_V(A i)|. have ErC k i: (#|'C_V(A i)| ^ (k i * #|A i|) = p ^ (rC i * k i * #|A i|))%N. suffices /card_pgroup->: p.-group 'C_V(A i) by rewrite -expnM mulnA. by rewrite (pgroupS (subsetIl _ _)). rewrite !{1}(eq_bigr _ (fun i _ => ErC _ i)) {ErC} -!expn_sum; congr (_ ^ _)%N. have eqmodX x y: (forall e, x = y %[mod p ^ e]) -> x = y. pose e := maxn x y; move/(_ e); have:= ltn_expl e p_gt1. by rewrite gtn_max /= => /andP[x_ltq y_ltq]; rewrite !modn_small. apply: eqmodX => e; have [-> | e_gt0] := posnP e; first by rewrite !modn1. set q := (p ^ e)%N; have q_gt1: q > 1 by rewrite -(exp1n e) ltn_exp2r. have{e_gt0 co_pG} [wT W D G1 f homoW oW kerf imfW imfG1 defD] := iso_quotient_homocyclic_sdprod minV co_pG abelV e_gt0. have [[cWW _] [_ /mulG_sub[sWD sG1D] nWG1 tiWG1]] := (andP homoW, sdprodP defD). have pW: p.-group W by rewrite /pgroup oW pnatX [p.-nat _]pV. have rW_V: 'r(W) = 'dim V. rewrite (rank_abelian_pgroup pW cWW) -(mulnK #|_| (cardG_gt0 'Mho^1(W))). rewrite mul_card_Ohm_Mho_abelian // divg_normal ?Mho_normal //=. rewrite -(setIidPr (Mho_sub 1 W)) -kerf. by rewrite (card_isog (first_isog_loc _ _)) //= imfW (dim_abelemE abelV). have expW: exponent W = q. apply/eqP; rewrite -(@eqn_exp2r _ _ ('dim V)) // -{1}rW_V -expnM mulnC expnM. by rewrite (dim_abelemE abelV) -?card_pgroup // -oW eq_sym max_card_abelian. have{rW_V} /isogP[fW injfW im_fW]: [set: 'rV['Z_q](V)] \isog W. rewrite eq_abelian_type_isog ?zmod_abelian // abelian_type_mx_group ?mul1n //. by rewrite abelian_type_homocyclic // rW_V expW. have WfW u: fW u \in W by rewrite -im_fW mem_morphim ?inE. have [fW' [DfW' KfW' _ _]] := domP (invm_morphism injfW) im_fW. have{KfW'} injfW': 'injm fW' by rewrite KfW' injm_invm. have fW'K: {in W, cancel fW' fW} by move=> w Ww; rewrite DfW' invmK //= im_fW. have toWlin a1: linear (fun u => fW' (fW u ^ val (subg G1 a1))). move=> z /= x y; rewrite (morphM fW) /= ?in_setT // conjMg /=. rewrite morphM ?memJ_norm ?(subsetP nWG1) ?subgP //=; congr (_ * _). rewrite -(natr_Zp z) !scaler_nat morphX ?in_setT // conjXg morphX //. by rewrite memJ_norm // (subsetP nWG1) ?subgP. pose toWlM a1 := GRing.isLinear.Build _ _ _ _ _ (toWlin a1). pose rWL a1 : {linear _ -> _} := HB.pack (fun u => fW' (fW u ^ val (subg G1 a1))) (toWlM a1). pose rW a1 := lin1_mx (rWL a1). pose fG := restrm sG1D f; have im_fG : fG @* G1 = G by rewrite im_restrm. have injfG: 'injm fG by rewrite -tiWG1 setIC ker_restrm kerf setIS ?Mho_sub. pose fG' := invm injfG; have im_fG': fG' @* G = G1 by rewrite -im_fG im_invm. pose gamma i := \sum_(a in A i) rW (fG' a). suffices{sum_k partG} tr_rW_Ai i: nz_k i -> \tr (gamma i) = (rC i * #|A i|)%:R. have Dtr k i: nz_k i -> (rC i * k i * #|A i|)%:R = \tr (gamma i *+ k i). by rewrite mulnAC natrM raddfMn mulr_natr /= => /tr_rW_Ai->. rewrite -!val_Zp_nat // !natr_sum !{1}(eq_bigr _ (Dtr _)){Dtr}; congr (val _). rewrite -!raddf_sum -!(eq_bigr _ (fun i _ => sumrMnl _ _ _ _)); congr (\tr _). have sA_GP i a nz_i := subsetP (sA_G i nz_i) a. rewrite !(exchange_big_dep (mem G)) {sA_GP}//=; apply: eq_bigr => a Ga. by rewrite !sumrMnr !(big_andbC _ _ _ nz_k) -!/(sum_k _ A a _) partG. move/sA_G=> {sA_G} sAiG; pose Ai1 := fG' @* A i; pose rR := 'r([~: W, Ai1]). have sAiG1: Ai1 \subset G1 by rewrite -im_fG' morphimS. have AfG' a: a \in A i -> fG' a \in Ai1. by move=> Aa; rewrite mem_morphim //= im_restrm imfG1 ?(subsetP sAiG). have coWAi1: coprime #|W| #|Ai1|. by rewrite coprime_morphr ?(coprimegS sAiG) ?(pnat_coprime pW). suffices [Pl [Pr [Pu [Pd [PlrudK ErC ErR]]]]]: exists Pl, exists Pr, exists Pu, exists Pd, [/\ row_mx Pl Pr *m col_mx Pu Pd = 1%R, {in A i, forall a, Pd *m (rW (fG' a) *m Pr) = 1%:M :> 'M_(rC i)} & \sum_(a in A i) Pu *m (rW (fG' a) *m Pl) = 0 :> 'M_rR]. - rewrite -(mulmx1 (gamma i)) idmxE -PlrudK mulmxA mxtrace_mulC mul_mx_row. rewrite mul_col_row mxtrace_block !mulmx_suml !mulmx_sumr ErR mxtrace0 add0r. by rewrite (eq_bigr _ ErC) sumr_const raddfMn /= mxtrace1 natrM mulr_natr. have defW: [~: W, Ai1] \x 'C_W(Ai1) = W. by rewrite coprime_abelian_cent_dprod ?(subset_trans sAiG1). have [_ mulRCW _ tiRCW] := dprodP defW; have [sRW sCW] := mulG_sub mulRCW. have [homoRW homoCW] := dprod_homocyclic defW pW homoW. have [] := abelian_type_dprod_homocyclic defW pW homoW. rewrite expW -/rR => atypeRW atypeCW. have [[cRR _] [cCC _]] := (andP homoRW, andP homoCW). have{cRR atypeRW} /isogP[hR injhR im_hR]: [~: W, Ai1] \isog [set: 'rV['Z_q]_rR]. rewrite eq_abelian_type_isog ?zmod_abelian ?atypeRW //. by rewrite abelian_type_mx_group // mul1n eqxx. have{tiRCW} rCW : 'r('C_W(Ai1)) = rC i. rewrite -['r(_)]rank_Ohm1; have /rank_abelem ->: p.-abelem 'Ohm_1('C_W(Ai1)). by rewrite Ohm1_abelem ?(pgroupS (subsetIl _ _)). congr (logn p _); transitivity #|'C_W(Ai1) : 'Mho^1('C_W(Ai1))|. by rewrite -divgS ?Mho_sub // -(mul_card_Ohm_Mho_abelian 1 cCC) mulnK. transitivity #|'C_W(Ai1) : 'Mho^1(W)|. symmetry; have /dprodP[_ /= defW1 _ _] := Mho_dprod 1 defW. rewrite -indexgI; congr #|_ : _|; rewrite /= -defW1 -group_modr ?Mho_sub //. by rewrite [_ :&: _](trivgP _) ?mul1g //= setIC -tiRCW setSI ?Mho_sub. suffices /card_isog ->: 'C_V(A i) \isog 'C_W(Ai1) / 'Mho^1(W). by rewrite card_quotient // subIset // normal_norm ?Mho_normal. rewrite coprime_quotient_cent ?Mho_sub ?abelian_sol //= -/Ai1; last first. by rewrite (subset_trans sAiG1) // gFnorm_trans. have ->: A i :=: fG @* Ai1. by rewrite /Ai1 morphim_invmE morphpreK // im_restrm imfG1. rewrite -imfW morphim_restrm (setIidPr sAiG1). have [f1 injf1 im_f1] := first_isom f. rewrite -!im_f1 -injm_subcent ?quotientS ?(subset_trans sAiG1) //. by rewrite -kerf isog_sym sub_isog // subIset ?quotientS. have{atypeCW} /isogP[hC injhC im_hC]: 'C_W(Ai1) \isog [set: 'rV['Z_q]_(rC i)]. rewrite eq_abelian_type_isog ?zmod_abelian // atypeCW rCW. by rewrite abelian_type_mx_group ?mul1n. have mkMx m1 m2 (U : {group 'rV['Z_q]_m1}) (g : {morphism U >-> 'rV['Z_q]_m2}): setT \subset 'dom g -> {Mg | mulmx^~ Mg =1 g}. move/subsetP=> allU. have lin_g : linear g. move=> z u v; rewrite morphM ?allU ?in_setT //. by rewrite -(natr_Zp z) !scaler_nat -zmodXgE morphX ?allU ?in_setT. pose glM := GRing.isLinear.Build _ _ _ _ _ lin_g. pose gL : {linear _ -> _} := HB.pack (mfun g) glM. by exists (lin1_mx gL) => u; rewrite mul_rV_lin1. have /mkMx[Pu defPu]: setT \subset 'dom (invm injfW \o invm injhR). by rewrite -sub_morphim_pre -im_hR // im_invm //= im_fW. have /mkMx[Pd defPd]: setT \subset 'dom (invm injfW \o invm injhC). by rewrite -sub_morphim_pre -im_hC //= im_fW im_invm subsetIl. pose fUl := pairg1 ('rV['Z_q]_(rC i) : finGroupType) \o hR. pose fUr := @pair1g ('rV['Z_q]_rR : finGroupType) _ \o hC. have cRCW: fUr @* 'C_W(Ai1) \subset 'C(fUl @* [~: W, Ai1]). rewrite !morphim_comp morphim_pair1g morphim_pairg1. set UR := hR @* _; set UC := hC @* _. by have/dprodP[] : _ = setX UR UC := setX_dprod _ _. have /domP[fUr' [DfUr' _ _ im_fUr']]: 'dom fUr = 'C_W(Ai1). by rewrite /dom -im_hC injmK. have /domP[fUl' [DfUl' _ _ im_fUl']]: 'dom fUl = [~: W, Ai1]. by rewrite /dom -im_hR injmK. rewrite -{}im_fUr' -{}im_fUl' in cRCW; pose hW := dprodm defW cRCW. pose fPl := @fst _ _ \o (hW \o fW); pose fPr := @snd _ _ \o (hW \o fW). have /mkMx[/= Pl defPl]: setT \subset 'dom fPl. by rewrite -!sub_morphim_pre ?subsetT ?im_fW. have /mkMx[/= Pr defPr]: setT \subset 'dom fPr. by rewrite -!sub_morphim_pre ?subsetT ?im_fW. exists Pl, Pr, Pu, Pd; split. - apply/row_matrixP=> j; rewrite rowE -row1 mul_row_col mulmxDr !mulmxA. apply: (injmP injfW); rewrite ?in_setT // morphM ?in_setT //. rewrite defPl defPr defPu defPd -/hW [hW]lock /= -lock. have /(mem_dprod defW)[jR [jC [RjR CjC -> _]]]:= WfW (row j 1). rewrite [hW _]dprodmE // DfUl' DfUr' /= mulg1 mul1g !invmE // -DfW'. by rewrite !fW'K ?(subsetP sRW jR) ?(subsetP sCW). - move=> a Aa; apply/row_matrixP=> j; pose jC := invm injhC (row j 1%:M). rewrite rowE -row1 !mulmxA defPd defPr -/hW [hW]lock /= mul_rV_lin1 /= -lock. have CjC: jC \in 'C_W(Ai1). by rewrite -(im_invm injhC) mem_morphim /= ?im_hC ?inE. have [[/fW'K id_jC /centP cA1jC] A1a] := (setIP CjC, AfG' a Aa). rewrite -DfW' id_jC subgK ?(subsetP sAiG1) // /conjg cA1jC // mulKg id_jC. by rewrite [hW _]dprodmEr ?DfUr' //= invmK ?im_hC ?inE. apply/row_matrixP=> j; pose jR := invm injhR (row j 1%:M). have RjR: jR \in [~: W, Ai1]. by rewrite -(im_invm injhR) mem_morphim /= ?im_hR ?inE. rewrite rowE -row1 mulmx_sumr raddf0 -/jR. have /subsetP nRA1: Ai1 \subset 'N([~: W, Ai1]) by rewrite commg_normr. transitivity (\sum_(a1 in Ai1) hR (jR ^ a1)). rewrite {1}[Ai1 in rhs in _ = rhs]morphimEsub /= ?im_restrm ?imfG1 //. rewrite big_imset /=; last first. apply: sub_in2 (injmP (injm_invm injfG)); apply/subsetP. by rewrite /= im_restrm imfG1. apply: eq_bigr => a /AfG' A1a. have RjRa: jR ^ fG' a \in [~: W, Ai1] by rewrite memJ_norm ?nRA1. rewrite !mulmxA defPu defPl mul_rV_lin1 -/hW [hW]lock /= -lock. rewrite subgK ?(subsetP sAiG1) // -DfW' !fW'K ?(subsetP sRW) //. by rewrite [hW _]dprodmEl // DfUl'. have [nf [fj Rfj ->]] := gen_prodgP RjR. transitivity (\sum_(a1 in Ai1) (\prod_i1 hR (fj i1 ^ a1))%g). apply: eq_bigr => a1 Aa1; rewrite conjg_prod morph_prod // => i1 _. by rewrite memJ_norm ?mem_gen ?nRA1. rewrite exchange_big big1 //= => i1 _; have /imset2P[w a1 Ww Aa1 ->] := Rfj i1. apply: (addrI (\sum_(a2 in Ai1) hR [~ w, a2])). rewrite addr0 {2}(reindex_inj (mulgI a1)) -big_split /=. apply: eq_big => [a2 | a2 Aa2]; first by rewrite groupMl. by rewrite commgMJ [rhs in _ = rhs]morphM ?memJ_norm ?nRA1 ?mem_commg ?groupM. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action gfunctor commutator) mathcomp(gproduct zmodp cyclic center pgroup gseries nilpotent sylow) mathcomp(finalg finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)