(Joint Center)Library BGappendixAB

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div.
Require Import fintype bigop prime finset ssralg fingroup morphism.
Require Import automorphism quotient gfunctor commutator zmodp center pgroup.
Require Import sylow gseries nilpotent abelian maximal.
Require Import matrix mxalgebra mxrepresentation mxabelem.
Require Import BGsection1 BGsection2.

This file contains the useful material in B & G, appendices A and B, i.e., the proof of the p-stability properties and the ZL-Theorem (the Puig replacement for the Glaubermann ZJ-theorem). The relevant definitions are given in BGsection1. Theorem A.4(a) has not been formalised: it is a result on external p-stability, which concerns faithful representations of group with a trivial p-core on a field of characteristic p. It's the historical concept that was studied by Hall and Higman, but it's not used for FT. Note that the finite field case can be recovered from A.4(c) with a semi-direct product.

Set Implicit Arguments.

Open Local Scope ring_scope.
Import GroupScope GRing.Theory.

Section AppendixA.

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

Import MatrixGenField.

This is B & G, Theorem A.4(c) (in Appendix A, not section 16!). We follow both B & G and Gorenstein in using the general form of the p-stable property. We could simplify the property because the conditions under which we prove p-stability are inherited by sections (morphic image in our framework), and restrict to the case where P is normal in G. (Clearly the 'O_p^'(G) * P <| G premise plays no part in the proof.) Theorems A.1-A.3 are essentially inlined in this proof.

Theorem odd_p_stable gT p (G : {group gT}) : odd #|G|p.-stable G.

Section A5.

Variables (gT : finGroupType) (p : nat) (G P X : {group gT}).

Hypotheses (oddG : odd #|G|) (solG : solvable G) (pP : p.-group P).
Hypotheses (nsPG : P <| G) (sXG : X \subset G).
Hypotheses (genX : generated_by (p_norm_abelian p P) X).

Let C := 'C_G(P).
Let defN : 'N_G(P) = G.
Let nsCG : C <| G.
Let nCG := normal_norm nsCG.
Let nCX := subset_trans sXG nCG.

This is B & G, Theorem A.5.1; it does not depend on the solG assumption.
This is B & G, Theorem A.5.2.
Theorem odd_abelian_gen_constrained :
  'O_p^'(G) = 1 → 'C_('O_p(G))(P) \subset PX \subset 'O_p(G).

End A5.

End AppendixA.

Section AppendixB.

Local Notation "X --> Y" := (generated_by (norm_abelian X) Y)
  (at level 70, no associativity) : group_scope.

Variable gT : finGroupType.
Implicit Types G H A : {group gT}.
Implicit Types D E : {set gT}.
Implicit Type p : nat.

Lemma Puig_char G : 'L(G) \char G.

Lemma center_Puig_char G : 'Z('L(G)) \char G.

This is B & G, Lemma B.1(a).
This is part of B & G, Lemma B.1(b) (see also BGsection1.Puig1).
This is part of B & G, Lemma B.1(b).
This is part of B & G, Lemma B.1(b).
This is B & G, Lemma B.1(c).
Lemma Puig_limit G :
   m, k, m k
    'L_{k.*2}(G) = 'L_*(G) 'L_{k.*2.+1}(G) = 'L(G).

This is B & G, Lemma B.1(d), second part; the first part is covered by BGsection1.Puig_inf_sub.
This is B & G, Lemma B.1(e).
Lemma abelian_norm_Puig n G A :
  n > 0 → abelian AA <| GA \subset 'L_{n}(G).

This is B & G, Lemma B.1(f), first inclusion.
This is B & G, Lemma B.1(f), second inclusion.
This is B & G, Lemma B.1(f), third inclusion (the fourth is trivial).
This is B & G, Lemma B.1(f), fifth inclusion (the sixth is trivial).
This is B & G, Lemma B.1(f), final remark (we prove the contrapositive).
Lemma trivg_center_Puig_pgroup p G : p.-group G'Z('L(G)) = 1 → G :=: 1.

This is B & G, Lemma B.1(g), second part; the first part is simply the definition of 'L(G) in terms of 'L_*(G).
This is B & G, Lemma B.2.
Lemma sub_Puig_eq G H : H \subset G'L(G) \subset H'L(H) = 'L(G).

Lemma norm_abgen_pgroup p X G :
  p.-group GX --> Ggenerated_by (p_norm_abelian p X) G.

Variables (p : nat) (G S : {group gT}).
Hypotheses (oddG : odd #|G|) (solG : solvable G) (sylS : p.-Sylow(G) S).
Hypothesis p'G1 : 'O_p^'(G) = 1.

Let T := 'O_p(G).
Let nsTG : T <| G := pcore_normal _ _.
Let pT : p.-group T := pcore_pgroup _ _.
Let pS : p.-group S := pHall_pgroup sylS.
Let sSG := pHall_sub sylS.

This is B & G, Lemma B.3.
This is B & G, Theorem B.4(b).
Theorem Puig_center_normal : 'Z(L) <| G.

End AppendixB.

Section Puig_factorization.

Variables (gT : finGroupType) (p : nat) (G S : {group gT}).
Hypotheses (oddG : odd #|G|) (solG : solvable G) (sylS : p.-Sylow(G) S).

This is B & G, Theorem B.4(a).