(Joint Center)Library PFsection8

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq path div choice.
Require Import fintype tuple finfun bigop prime ssralg poly finset center.
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
Require Import gfunctor gproduct cyclic commutator nilpotent pgroup.
Require Import sylow hall abelian maximal frobenius.
Require Import matrix mxalgebra mxrepresentation vector.
Require Import BGsection1 BGsection3 BGsection7 BGsection10.
Require Import BGsection14 BGsection15 BGsection16.
Require ssrnum.
Require Import algC classfun character inertia vcharacter.
Require Import PFsection1 PFsection2 PFsection3 PFsection4 PFsection5.

This file covers Peterfalvi, Section 8: Structure of a Minimal Simple Group of Odd Order. Actually, most Section 8 definitions can be found in BGsection16, which holds the conclusions of the Local Analysis part of the proof, as the B & G text has been adapted to fit the usage in Section 8. Most of the definitions of Peterfalvi Section 8 are covered in BGsection7, BGsection15 and BGsection16; we only give here: FT_Pstructure S T defW <-> the groups W, W1, W2, S, and T satisfy the conclusion of Theorem (8.8)(b), in particular, S and T are of type P, S = S^(1) ><| W1, and T = T^`(1) ><| W2. The assumption defW : W1 \x W2 = W is a parameter. 'R[x] == the "signalizer" group of x \in 'A1(M) for the Dade hypothesis of M (note: this is only extensionally equal to the 'R[x] defined in BGsection14). 'R_M == the signalizer functor for the Dade hypothesis of M. Note that this only maps x to 'R[x] for x in 'A1(M). The casual use of the R(x) in Peterfalvi is improper, as its meaning depends on which maximal group is considered. 'A1~(M) == the support of the image of the restricted Dade isometry on M (when M is maximal). 'A~(M) == the support of the image of the Dade isometry on M. 'A0~(M) == the support of the image of the extended Dade isometry on M. FTsupports M L <-> L supports M in the sense of (8.14) and (8.18). This definition is not used outside this file.

Set Implicit Arguments.

Import GroupScope GRing.Theory.

Local Open Scope ring_scope.

Supercedes the notation in BGsection14.
Notation "''R' [ x ]" := 'C_((gval 'N[x])`_\F)[x]
 (at level 8, format "''R' [ x ]") : group_scope.
Notation "''R' [ x ]" := 'C_('N[x]`_\F)[x]%G : Group_scope.

Section Definitions.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types L M X : {set gT}.

These cover Peterfalvi, Definition (8.14).
Definition FTsignalizer M x := if 'C[x] \subset M then 1%G else 'R[x]%G.

Definition FTsupports M L :=
  [ x in 'A(M), ~~ ('C[x] \subset M) && ('C[x] \subset L)].

Definition FT_Dade_support M X :=
  \bigcup_(x in X) class_support (FTsignalizer M x :* x) G.

End Definitions.

Notation "''R_' M" := (FTsignalizer M)
 (at level 8, M at level 2, format "''R_' M") : group_scope.

Notation "''A1~' ( M )" := (FT_Dade_support M 'A1(M))
  (at level 8, format "''A1~' ( M )").

Notation "''A~' ( M )" := (FT_Dade_support M 'A(M))
  (at level 8, format "''A~' ( M )").

Notation "''A0~' ( M )" := (FT_Dade_support M 'A0(M))
  (at level 8, format "''A0~' ( M )").

Section Eight.

Variable gT : minSimpleOddGroupType.
Local Notation G := (TheMinSimpleOddGroup gT).
Implicit Types (p q : nat) (x y z : gT).
Implicit Types H K L M N P Q R S T U V W : {group gT}.

Peterfalvi, Definition (8.1) is covered by BGsection16.of_typeF.
This is the remark following Definition (8.1).
Remark compl_of_typeF M U V (H := M`_\F) :
  H ><| U = Mof_typeF M Vof_typeF M U.

Lemma Frobenius_of_typeF M U (H := M`_\F) :
  [Frobenius M = H ><| U]of_typeF M U.

This is Peterfalvi (8.2).
Lemma typeF_context M U (H := M`_\F) :
    of_typeF M U
  [/\ (*a*) U0, is_typeF_complement M U U0#|U0| = exponent U,
      (*b*) [Frobenius M = H ><| U] = Zgroup U
    & (*c*) U1 (i : Iirr H),
            is_typeF_inertia M U U1i != 0 → 'I_U['chi_i] \subset U1].

Peterfalvi, Definition (8.3) is covered by BGsection16.of_typeI. Peterfalvi, Definition (8.4) is covered by BGsection16.of_typeP.

Section TypeP_Remarks.
These correspond to the remarks following Definition (8.4).

Variables (M U W W1 W2 : {group gT}) (defW : W1 \x W2 = W).
Let H := M`_\F.
Let M' := M^`(1)%g.

Hypothesis MtypeP : of_typeP M U defW.

Remark of_typeP_sol : solvable M.

Remark typeP_cent_compl : 'C_M'(W1) = W2.

Remark typeP_cent_core_compl : 'C_H(W1) = W2.

Lemma typePF_exclusion K : ¬ of_typeF M K.

Remark of_typeP_compl_conj W1x : M' ><| W1x = MW1x \in W1 :^: M.

Remark conj_of_typeP x :
  x \in M{defWx : W1 :^ x \x W2 :^ x = W :^ x | of_typeP M (U :^ x) defWx}.

This is Peterfalvi (8.5), with an extra clause in anticipation of (8.15).
Lemma typeP_context :
  [/\ (*a*) H \x 'C_U(H) = 'F(M),
      (*b*) U^`(1)%g \subset 'C(H) (U :!=: 1%g~~ (U \subset 'C(H))),
      (*c*) normedTI (cyclicTIset defW) G W
    & cyclicTI_hypothesis G defW].

End TypeP_Remarks.

Remark FTtypeP_witness M :
  M \in 'MFTtype M != 1%Nexists_typeP (of_typeP M).

Peterfalvi, Definition (8.6) is covered by BGsection16.of_typeII_IV et al. Peterfalvi, Definition (8.7) is covered by BGsection16.of_typeV.

Section FTypeP_Remarks.
The remarks for Definition (8.4) also apply to (8.6) and (8.7).

Variables (M U W W1 W2 : {group gT}) (defW : W1 \x W2 = W).
Let H := M`_\F.
Let M' := M^`(1)%g.

Hypotheses (maxM : M \in 'M) (MtypeP : of_typeP M U defW).

Remark of_typeP_conj (Ux W1x W2x Wx : {group gT}) (defWx : W1x \x W2x = Wx) :
    of_typeP M Ux defWx
     [/\ x \in M, U :^ x = Ux, W1 :^ x = W1x, W2 :^ x = W2x & W :^ x = Wx].

Lemma FTtypeP_neq1 : FTtype M != 1%N.

Remark compl_of_typeII_IV : FTtype M != 5 → of_typeII_IV M U defW.

Remark compl_of_typeII : FTtype M == 2 → of_typeII M U defW.

Remark compl_of_typeIII : FTtype M == 3 → of_typeIII M U defW.

Remark compl_of_typeIV : FTtype M == 4 → of_typeIV M U defW.

Remark compl_of_typeV : FTtype M == 5 → of_typeV M U defW.

End FTypeP_Remarks.

This is the statement of Peterfalvi, Theorem (8.8)(a).
Definition all_FTtype1 := [ M : {group gT} in 'M, FTtype M == 1%N].

This is the statement of Peterfalvi, Theorem (8.8)(b).
Definition typeP_pair S T (W W1 W2 : {set gT}) (defW : W1 \x W2 = W) :=
 [/\ [/\ cyclicTI_hypothesis G defW, S \in 'M & T \in 'M],
   (*b1*) [/\ S^`(1) ><| W1 = S, T^`(1) ><| W2 = T & S :&: T = W]%g,
   (*b2*) (FTtype S == 2) || (FTtype T == 2),
   (*b3*) (1 < FTtype S 5 1 < FTtype T 5)%N
 & (*b4*) {in 'M, M, FTtype M != 1%Ngval M \in S :^: G :|: T :^: G}].

Lemma typeP_pair_sym S T W W1 W2 (defW : W1 \x W2 = W) (defW21 : W2 \x W1 = W) :
  typeP_pair S T defWtypeP_pair T S defW21.

This is Peterfalvi, Theorem (8.8).
Lemma FTtypeP_pair_cases :
     (*a*) {in 'M, M, FTtype M == 1%N}
   (*b*) S, T, exists_typeP (fun _typeP_pair S T).

This is Peterfalvi (8.9). We state the lemma using the of_typeP predicate, as it is the Skolemised form of Peterfalvi, Definition (8.4).
Lemma typeP_pairW S T W W1 W2 (defW : W1 \x W2 = W) :
  typeP_pair S T defW U : {group gT}, of_typeP S U defW.

Section OneMaximal.

Variable M U W W1 W2 : {group gT}. (* W, W1 and W2 are only used later. *)
Hypothesis maxM : M \in 'M.

Peterfalvi, Definition (8.10) is covered in BGsection16.
This is Peterfalvi (8.11).
Lemma FTcore_facts :
 [/\ Hall G M`_\F, Hall G M`_\s
   & S, Sylow M`_\s SS :!=: 1%g'N(S) \subset M].

This is Peterfalvi (8.12). (b) could be stated for subgroups of U wlog -- usage should be checked.
Lemma FTtypeI_II_facts n (H := M`_\F) :
    FTtype M == nH ><| U = M ^`(n.-1)%g
  if 0 < n 2 then
  [/\ (*a*) p S, p.-Sylow(U) Sabelian S ('r(S) 2)%N,
      (*b*) X, X != set0X \subset U^#'C_H(X) != 1%g
            'M('C(X)) = [set M]
    & (*c*) let B := 'A(M) :\: 'A1(M) in B != set0normedTI B G M
  ] else True.

This is Peterfalvi (8.13). We have substituted the B & G notation for the unique maximal supergroup of 'C[x], and specialized the lemma to X := 'A0(M).
Lemma FTsupport_facts (X := 'A0(M)) (D := [set x in X | ~~('C[x] \subset M)]) :
  [/\ (*a*) {in X &, x, {subset x ^: G x ^: M}},
      (*b*) D \subset 'A1(M) {in D, x, 'M('C[x]) = [set 'N[x]]}
    & (*c*) {in D, x (L := 'N[x]) (H := L`_\F),
        [/\ (*c1*) H ><| (M :&: L) = L 'C_H[x] ><| 'C_M[x] = 'C[x],
            (*c2*) {in X, y, coprime #|H| #|'C_M[y]| },
            (*c3*) x \in 'A(L) :\: 'A1(L)
          & (*c4*) 1 FTtype L 2
                 (FTtype L == 2 → [Frobenius M with kernel M`_\F])]}].

A generic proof of the first assertion of Peterfalvi (8.15).
This is Peterfalvi (8.15), second assertion.
Subcoherence and cyclicTI properties of type II-V subgroups.
Hypotheses (defW : W1 \x W2 = W) (MtypeP : of_typeP M U defW).
Let H := M`_\F%G.
Let K := M^`(1)%G.

Lemma FT_cyclicTI_hyp : cyclicTI_hypothesis G defW.
Let ctiW := FT_cyclicTI_hyp.

This useful combination of Peterfalvi (8.8) and (8.9).
Lemma FTtypeP_pair_witness :
  exists2 T, typeP_pair M T defW
     & defW21 : W2 \x W1 = W, V : {group gT}, of_typeP T V defW21.

Lemma FT_primeTI_hyp : primeTI_hypothesis M K defW.
Let ptiWM := FT_primeTI_hyp.

Lemma FTtypeP_supp0_def :
  'A0(M) = 'A(M) :|: class_support (cyclicTIset defW) M.

Fact FT_Fcore_prime_Dade_def : prime_Dade_definition M K H 'A(M) 'A0(M) defW.

Definition FT_prDade_hypF : prime_Dade_hypothesis _ M K H 'A(M) 'A0(M) defW :=
  PrimeDadeHypothesis ctiW ptiWM FT_Dade0_hyp FT_Fcore_prime_Dade_def.

Fact FT_core_prime_Dade_def : prime_Dade_definition M K M`_\s 'A(M) 'A0(M) defW.

Definition FT_prDade_hyp : prime_Dade_hypothesis _ M K M`_\s 'A(M) 'A0(M) defW
  := PrimeDadeHypothesis ctiW ptiWM FT_Dade0_hyp FT_core_prime_Dade_def.

Let calS := seqIndD K M M`_\s 1.

Fact FTtypeP_cohererence_base_subproof : cfConjC_subset calS calS.

Fact FTtypeP_cohererence_nonreal_subproof : ~~ has cfReal calS.

Definition FTtypeP_coh_base_sig :=
  prDade_subcoherent FT_prDade_hyp
    FTtypeP_cohererence_base_subproof FTtypeP_cohererence_nonreal_subproof.

Definition FTtypeP_coh_base := sval FTtypeP_coh_base_sig.

Local Notation R := FTtypeP_coh_base.

Lemma FTtypeP_subcoherent : subcoherent calS tau R.
Let scohS := FTtypeP_subcoherent.

Let w_ i j := cyclicTIirr defW i j.
Let sigma := cyclicTIiso ctiW.
Let eta_ i j := sigma (w_ i j).
Let mu_ := primeTIred ptiWM.
Let delta_ := fun jprimeTIsign ptiWM j.

Lemma FTtypeP_base_ortho :
  {in [predI calS & irr M] & irr W, phi w, orthogonal (R phi) (sigma w)}.

Lemma FTtypeP_base_TIred :
  let dsw j k := [seq delta_ j *: eta_ i k | i : Iirr W1] in
  let Rmu j := dsw j j ++ map -%R (dsw j (conjC_Iirr j)) in
   j, R (mu_ j) = Rmu j.

Lemma coherent_ortho_cycTIiso calS1 (tau1 : {additive 'CF(M)'CF(G)}) :
    cfConjC_subset calS1 calScoherent_with calS1 M^# tau tau1
   chi i j, chi \in calS1chi \in irr M'[tau1 chi, eta_ i j] = 0.

Import ssrnum Num.Theory.

Lemma FTtypeP_coherent_TIred calS1 (tau1 : {additive 'CF(M)'CF(G)}) t j :
    cfConjC_subset calS1 calScoherent_with calS1 M^# tau tau1
    'chi_t \in calS1mu_ j \in calS1
    let d := primeTI_Isign ptiWM j in let k := conjC_Iirr j in
  {dk : bool × Iirr W2 | tau1 (mu_ j) = (-1) ^+ dk.1 *: (\sum_i eta_ i dk.2)
    & dk.1 = d dk.2 = j
     [/\ dk.1 = ~~ d, dk.2 = k
        & l, mu_ l \in calS1mu_ l 1%g = mu_ j 1%gpred2 j k l]}.

Lemma size_red_subseq_seqInd_typeP (calX : {set Iirr K}) calS1 :
    uniq calS1{subset calS1 seqInd M calX}
    {subset calS1 [predC irr M]}
  size calS1 = #|[set i : Iirr K | 'Ind 'chi_i \in calS1]|.

End OneMaximal.

This is Peterfalvi (8.16).
This is Peterfalvi, Theorem (8.17).
Theorem FT_Dade_support_partition :
  [/\ (*a1*)
           \pi(G) =i [pred p | [ M : {group gT} in 'M, p \in \pi(M`_\s)]],
      (*a2*) {in 'M &, M L,
                gval L \notin M :^: Gcoprime #|M`_\s| #|L`_\s| },
      (*b*) {in 'M, M, #|'A1~(M)| = (#|M`_\s|.-1 × #|G : M|)%N}
    & (*c*) let PG := [set 'A1~(Mi) | Mi : {group gT} in 'M^G] in
       [/\ {in 'M^G &, injective (fun M'A1~(M))},
           all_FTtype1partition PG G^#
         & S T W W1 W2 (defW : W1 \x W2 = W),
             let VG := class_support (cyclicTIset defW) G in
           typeP_pair S T defWpartition (VG |: PG) G^# VG \notin PG]].

This is Peterfalvi (8.18). Note that only part (c) is actually used later.
Lemma FT_Dade_support_disjoint S T :
    S \in 'MT \in 'Mgval T \notin S :^: G
  [/\ (*a*) FTsupports S T = ~~ [disjoint 'A1(S) & 'A(T)]
          {in 'A1(S) :&: 'A(T), x,
               ~~ ('C[x] \subset S) 'C[x] \subset T},
      (*b*) [ x, FTsupports S (T :^ x)] = ~~ [disjoint 'A1~(S) & 'A~(T)]
    & (*c*) [disjoint 'A1~(S) & 'A~(T)] [disjoint 'A1~(T) & 'A~(S)]].

End Eight.

Notation FT_Dade0 maxM := (Dade (FT_Dade0_hyp maxM)).
Notation FT_Dade maxM := (Dade (FT_Dade_hyp maxM)).
Notation FT_Dade1 maxM := (Dade (FT_Dade1_hyp maxM)).