(Joint Center)Library PFsection12

(* (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 finset center.
Require Import fingroup morphism perm automorphism quotient action finalg zmodp.
Require Import gfunctor gproduct cyclic commutator gseries nilpotent pgroup.
Require Import sylow hall abelian maximal frobenius.
Require Import matrix mxalgebra mxpoly mxrepresentation mxabelem vector.
Require Import falgebra fieldext finfield.
Require Import BGsection1 BGsection2 BGsection3 BGsection4 BGsection7.
Require Import BGsection14 BGsection15 BGsection16.
Require Import ssrnum ssrint algC cyclotomic algnum.
Require Import classfun character inertia vcharacter.
Require Import PFsection1 PFsection2 PFsection3 PFsection4 PFsection5.
Require Import PFsection6 PFsection7 PFsection8 PFsection9 PFsection11.

Set Implicit Arguments.

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

Section PFTwelve.

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}.

Section Twelve2.

Hypothesis 12.1
Variable L : {group gT}.

Hypotheses (maxL : L \in 'M) (Ltype1 : FTtype L == 1%N).

Local Notation "` 'L'" := (gval L) (at level 0, only parsing) : group_scope.
Local Notation H := `L`_\F%G.
Local Notation "` 'H'" := `L`_\F (at level 0) : group_scope.

Let calS := seqIndD H L H 1%G.
Let tau := FT_Dade maxL.
Let S_ (chi : 'CF(L)) := [set i in irr_constt chi].
Let calX := Iirr_kerD L H 1%g.
Let calI := [seq 'chi_i | i in calX].

Let mem_calI i : i \in calX'chi_i \in calI.

Lemma FTtype1_irrP i :
  reflect (exists2 chi, chi \in calS & i \in S_ chi) (i \in calX).

Lemma FTtype1_irr_partition :
  partition [set Si in [seq S_ chi | chi <- calS]] calX.

This is Peterfalvi (12.2)(a), first part
Lemma FTtype1_seqInd_facts chi :
    chi \in calS
  [/\ chi = \sum_(i in S_ chi) 'chi_i,
      constant [seq 'chi_i 1%g | i in S_ chi]
    & {in S_ chi, i, 'chi_i \in 'CF(L, 1%g |: 'A(L))}].

This is Peterfalvi (12.2)(a), second part.
This is Peterfalvi (12.2)(b).
Lemma FPtype1_subcoherent (R1 := sval R1gen) :
  {R : 'CF(L)seq 'CF(G) |
    [/\ subcoherent calS tau R,
        {in Iirr_kerD L H 1%G, i (phi := 'chi_i),
         [/\ orthonormal (R1 phi),
             size (R1 phi) = 2
           & tau (phi - phi^*%CF) = \sum_(mu <- R1 phi) mu]}
    & chi, R chi = flatten [seq R1 'chi_i | i in S_ chi]]}.

End Twelve2.

Local Notation R1gen := FPtype1_irr_subcoherent.
Local Notation Rgen := FPtype1_subcoherent.

This is Peterfalvi (12.3)
Lemma FTtype1_seqInd_ortho L1 L2 (maxL1 : L1 \in 'M) (maxL2 : L2 \in 'M)
  (L1type : FTtype L1 == 1%N) (L2type : FTtype L2 == 1%N)
  (H1 := L1`_\F%G) (H2 := L2`_\F%G)
  (calS1 := seqIndD H1 L1 H1 1) (calS2 := seqIndD H2 L2 H2 1)
  (R1 := sval (Rgen maxL1 L1type)) (R2 := sval (Rgen maxL2 L2type)) :
  (gval L2) \notin L1 :^: G
  {in calS1 & calS2, chi1 chi2, orthogonal (R1 chi1) (R2 chi2)}.

Section Twelve_4_to_6.

Variable L : {group gT}.
Hypothesis maxL : L \in 'M .

Local Notation "` 'L'" := (gval L) (at level 0, only parsing) : group_scope.
Local Notation H := `L`_\F%G.
Local Notation "` 'H'" := `L`_\F (at level 0) : group_scope.
Local Notation H' := H^`(1)%G.
Local Notation "` 'H''" := `H^`(1) (at level 0) : group_scope.

Let calS := seqIndD H L H 1%G.
Let tau := FT_Dade maxL.
Let rho := invDade (FT_Dade_hyp maxL).

Section Twelve_4_5.

Hypothesis Ltype1 : FTtype L == 1%N.

Let R := sval (Rgen maxL Ltype1).
Let S_ (chi : 'CF(L)) := [set i in irr_constt chi].

This is Peterfalvi (12.4).
Lemma FTtype1_ortho_constant (psi : 'CF(G)) x :
    {in calS, phi, orthogonal psi (R phi)}x \in L :\: H
  {in x *: H, y, psi y = psi x}%g.

This is Peterfalvi (12.5)
Lemma FtypeI_invDade_ortho_constant (psi : 'CF(G)) :
    {in calS, phi, orthogonal psi (R phi)}
  {in H :\: H' &, x y, rho psi x = rho psi y}.

End Twelve_4_5.

Hypothesis frobL : [Frobenius L with kernel H].

Lemma FT_Frobenius_type1 : FTtype L == 1%N.
Let Ltype1 := FT_Frobenius_type1.

This is Peterfalvi (12.6).
Equivalent reformultaion of Hypothesis (12.8), avoiding quotients.
Hypothesis IHp :
   q M, (q < p)%NM \in 'MFTtype M == 1%N → ('r_q(M) > 1)%N
  q \in \pi(M`_\F).

Variables M P0 : {group gT}.

Let K := M`_\F%G.
Let K' := K^`(1)%G.

Hypothesis maxM : M \in 'M.
Hypothesis Mtype1 : FTtype M == 1%N.
Hypothesis prankM : ('r_p(M) > 1)%N.
Hypothesis p'K : p^'.-group K.

Hypothesis sylP0 : p.-Sylow(M) P0.

This is Peterfalvi (12.9).
Lemma non_Frobenius_FTtype1_witness :
  [/\ abelian P0, 'r_p(P0) = 2
    & exists2 L, L \in 'M P0 \subset L`_\s
    & exists2 x, x \in 'Ohm_1(P0)^#
    & [/\ ~~ ('C_K[x] \subset K'), 'N(<[x]>) \subset M & ~~ ('C[x] \subset L)]].

Variables (L : {group gT}) (x : gT).
Hypotheses (abP0 : abelian P0) (prankP0 : 'r_p(P0) = 2).
Hypotheses (maxL : L \in 'M) (sP0_Ls : P0 \subset L`_\s).
Hypotheses (P0_1s_x : x \in 'Ohm_1(P0)^#) (not_sCxK' : ~~ ('C_K[x] \subset K')).
Hypotheses (sNxM : 'N(<[x]>) \subset M) (not_sCxL : ~~ ('C[x] \subset L)).

Let H := L`_\F%G.

This is Peterfalvi (12.10).
Let frobL : [Frobenius L with kernel H].

Let Ltype1 : FTtype L == 1%N.

Let sP0H : P0 \subset H.

This is the first part of Peterfalvi (12.11).
Let defM : K ><| (M :&: L) = M.

This is the second part of Peterfalvi (12.11).
Let sML_H : M :&: L \subset H.

Let E := sval (sigW (existsP frobL)).
Let e := #|E|.

Let defL : H ><| E = L.

Let Ecyclic_le_p : cyclic E (e %| p.-1) || (e %| p.+1).

Let calS := seqIndD H L H 1.
Notation tauL := (FT_Dade maxL).
Notation rhoL := (invDade (FT_Dade_hyp maxL)).

Section Twelve_13_to_16.

Variables (tau1 : {additive 'CF(L)'CF(G)}) (chi : 'CF(L)).
Hypothesis cohS : coherent_with calS L^# tauL tau1.
Hypotheses (Schi : chi \in calS) (chi1 : chi 1%g = e%:R).
Let psi := tau1 chi.

Let rhoL_psi : {in K, g, psi (x × g)%g = chi x} rhoL psi x = chi x.

Let rhoM := (invDade (FT_Dade1_hyp maxM)).

Let rhoM_psi :
  [/\ {in K^#, rhoM psi =1 psi},
      {in K :\: K' &, g1 g2, psi g1 = psi g2}
    & {in K :\: K', g, psi g \in Cint}].

This is the main part of Peterfalvi (12.16).
This is Peterfalvi, Theorem (12.7).
Theorem FTtype1_Frobenius M :
  M \in 'MFTtype M == 1%N[Frobenius M with kernel M`_\F].

This is Peterfalvi, Theorem (12.17).