(Joint Center)Library wielandt_fixpoint

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div.
Require Import fintype bigop prime binomial finset ssralg fingroup finalg.
Require Import morphism perm automorphism quotient action commutator gproduct.
Require Import zmodp cyclic center pgroup gseries nilpotent sylow finalg.
Require Import finmodule abelian frobenius maximal extremal hall finmodule.
Require Import matrix mxalgebra mxrepresentation mxabelem BGsection1.

This file provides the proof of the Wielandt fixpoint order formula, which is a prerequisite for B & G, Section 3 and Peterfalvi, Section 9.

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GroupScope GRing.Theory.
Import FinRing.Theory.

Implicit Types (gT wT : finGroupType) (m n p q : nat).

Lemma coprime_act_abelian_pgroup_structure gT p (A X : {group gT}) :
    abelian Ap.-group Ap^'.-group XX \subset 'N(A)
  exists2 s : {set {group gT}},
      \big[dprod/1]_(B in s) B = A
    & {in s, B : {group gT},
       [/\ homocyclic B, X \subset 'N(B)
         & acts_irreducibly X (B / 'Phi(B)) 'Q]}.

CoInductive is_iso_quotient_homocyclic_sdprod gT (V G : {group gT}) m : Prop :=
  IsoQuotientHomocyclicSdprod wT (W D G1 : {group wT}) (f : {morphism D >-> gT})
   of homocyclic W & #|W| = (#|V| ^ m)%N
    & 'ker f = 'Mho^1(W) & f @* W = V & f @* G1 = G & W ><| G1 = D.

Lemma iso_quotient_homocyclic_sdprod gT (V G : {group gT}) p m :
    minnormal V Gcoprime p #|G|p.-abelem Vm > 0 →
  is_iso_quotient_homocyclic_sdprod V G m.

Theorem solvable_Wielandt_fixpoint (I : finType) gT (A : I{group gT})
                                   (n m : Inat) (G V : {group gT}) :
    ( i, m i + n i > 0 → A i \subset G) →
    G \subset 'N(V)coprime #|V| #|G|solvable V
    {in G, 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.