(Joint Center)Library BGsection3

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

This file covers the material in B & G, Section 3. Note that in spite of the use of Gorenstein 2.7.6, the material in all of Section 3, and in all likelyhood the whole of B & G, does NOT depend on the general proof of existence of Frobenius kernels, because results on Frobenius groups are only used when the semidirect product decomposition is already known, and (see file frobenius.v) in this case the kernel is equal to the normal complement of the Frobenius complement.

Set Implicit Arguments.

Local Open Scope ring_scope.
Import GroupScope GRing.Theory.

Section BGsection3.

Implicit Type F : fieldType.
Implicit Type gT : finGroupType.
Implicit Type p : nat.

B & G, Lemma 3.1 is covered by frobenius.Frobenius_semiregularP.
This is B & G, Lemma 3.2.
Section FrobeniusQuotient.

Variables (gT : finGroupType) (G K R : {group gT}).
Implicit Type N : {group gT}.

This is a special case of B & G, Lemma 3.2 (b).
Lemma Frobenius_proper_quotient N :
    [Frobenius G = K ><| R]solvable KN <| GN \proper K
  [Frobenius G / N = (K / N) ><| (R / N)].

This is B & G, Lemma 3.2 (a).
Lemma Frobenius_normal_proper_ker N :
    [Frobenius G = K ><| R]solvable KN <| G~~ (K \subset N)
  N \proper K.

This is B & G, Lemma 3.2 (b).
Lemma Frobenius_quotient N :
    [Frobenius G = K ><| R]solvable KN <| G~~ (K \subset N)
  [Frobenius G / N = (K / N) ><| (R / N)].

End FrobeniusQuotient.

This is B & G, Lemma 3.3.
Lemma Frobenius_rfix_compl F gT (G K R : {group gT}) n
                          (rG : mx_representation F G n) :
    [Frobenius G = K ><| R][char F]^'.-group K
  ~~ (K \subset rker rG)rfix_mx rG R != 0.

This is Aschbacher (40.6)(3), or G. (3.14)(iii).
Lemma regular_pq_group_cyclic gT p q (H R : {group gT}) :
    [/\ prime p, prime q & p != q]#|R| = (p × q)%N
    H :!=: 1 → R \subset 'N(H)semiregular H R
  cyclic R.

This is B & G, Theorem 3.4.
Theorem odd_prime_sdprod_rfix0 F gT (G K R : {group gT}) n
                               (rG : mx_representation F G n) :
    K ><| R = Gsolvable Godd #|G|coprime #|K| #|R|prime #|R|
    [char F]^'.-group Grfix_mx rG R = 0 →
  [~: R, K] \subset rker rG.

Internal action version of B & G, Theorem 3.4.
Theorem odd_prime_sdprod_abelem_cent1 k gT (G K R V : {group gT}) :
    solvable Godd #|G|K ><| R = Gcoprime #|K| #|R|prime #|R|
    k.-abelem VG \subset 'N(V)k^'.-group G'C_V(R) = 1 →
  [~: R, K] \subset 'C_K(V).

This is B & G, Theorem 3.5.
Theorem Frobenius_prime_rfix1 F gT (G K R : {group gT}) n
                              (rG : mx_representation F G n) :
    K ><| R = Gsolvable Gprime #|R|'C_K(R) = 1 →
    [char F]^'.-group G\rank (rfix_mx rG R) = 1%N
  K^`(1) \subset rker rG.

Internal action version of B & G, Theorem 3.5.
Theorem Frobenius_prime_cent_prime k gT (G K R V : {group gT}) :
    solvable GK ><| R = Gprime #|R|'C_K(R) = 1 →
    k.-abelem VG \subset 'N(V)k^'.-group G#|'C_V(R)| = k
  K^`(1) \subset 'C_K(V).

Section Theorem_3_6.
Limit the scope of the FiniteModule notations
Import FiniteModule.

This is B & G, Theorem 3.6.
Theorem odd_sdprod_Zgroup_cent_prime_plength1 p gT (G H R R0 : {group gT}) :
    solvable Godd #|G|H ><| R = Gcoprime #|H| #|R|
    R0 \subset Rprime #|R0|Zgroup 'C_H(R0)
  p.-length_1 [~: H, R].

End Theorem_3_6.

This is B & G, Theorem 3.7.
Theorem prime_Frobenius_sol_kernel_nil gT (G K R : {group gT}) :
   K ><| R = Gsolvable Gprime #|R|'C_K(R) = 1 → nilpotent K.

Corollary Frobenius_sol_kernel_nil gT (G K H : {group gT}) :
  [Frobenius G = K ><| H]solvable Gnilpotent K.

This is B & G, Theorem 3.8.
Theorem odd_sdprod_primact_commg_sub_Fitting gT (G K R : {group gT}) :
    K ><| R = Godd #|G|solvable G
  (*1*) coprime #|K| #|R|
  (*2*) semiprime K R
  (*3*) 'C_('F(K))(R) = 1 →
  [~: K, R] \subset 'F(K).

This is B & G, Proposition 3.9 (for external action), with the incorrectly omitted nontriviality assumption reinstated.
Proposition ext_odd_regular_pgroup_cyclic (aT rT : finGroupType) p
              (D R : {group aT}) (K H : {group rT}) (to : groupAction D K) :
    p.-group Rodd #|R|H :!=: 1 →
    {acts R, on group H | to}{in R^#, x, 'C_(H | to)[x] = 1}
  cyclic R.

Internal action version of B & G, Proposition 3.9 (possibly, the only one we should keep).
Proposition odd_regular_pgroup_cyclic gT p (H R : {group gT}) :
    p.-group Rodd #|R|H :!=: 1 → R \subset 'N(H)semiregular H R
  cyclic R.

Another proof of Proposition 3.9, which avoids Frobenius groups entirely.
Proposition simple_odd_regular_pgroup_cyclic gT p (H R : {group gT}) :
    p.-group Rodd #|R|H :!=: 1 → R \subset 'N(H)semiregular H R
  cyclic R.

This is Aschbacher (40.6)(4).
Lemma odd_regular_metacyclic gT (H R : {group gT}) :
    odd #|R|H :!=: 1 → R \subset 'N(H)semiregular H R
  metacyclic R.

This is Huppert, Kapitel V, Satz 18.8 b (used in Peterfalvi, Section 13).
Lemma prime_odd_regular_normal gT (H R P : {group gT}) :
    prime #|P|odd #|R|P \subset R
    H :!=: 1 → R \subset 'N(H)semiregular H R
  P <| R.

Section Wielandt_Frobenius.

Variables (gT : finGroupType) (G K R : {group gT}).
Implicit Type A : {group gT}.

This is Peterfalvi (9.1).
This is B & G, Theorem 3.10.
Theorem Frobenius_primact gT (G K R M : {group gT}) :
    [Frobenius G = K ><| R]solvable G
    G \subset 'N(M)solvable MM :!=: 1 →
  (*1*) coprime #|M| #|G|
  (*2*) semiprime M R
  (*3*) 'C_M(K) = 1 →
  [/\ prime #|R|,
      #|M| = (#|'C_M(R)| ^ #|R|)%N
    & cyclic 'C_M(R)K^`(1) \subset 'C_K(M)].

End BGsection3.