(Joint Center)Library BGappendixC

(* (c) Copyright Microsoft Corporation and Inria. All rights reserved.        *)
Require Import ssreflect ssrbool ssrfun eqtype choice ssrnat seq div fintype.
Require Import tuple finfun bigop ssralg finset prime binomial poly polydiv.
Require Import fingroup morphism quotient automorphism action finalg zmodp.
Require Import gproduct cyclic commutator pgroup abelian frobenius BGsection1.
Require Import matrix mxalgebra mxabelem vector falgebra fieldext galois.
Require Import finfield ssrnum algC classfun character integral_char inertia.

Set Implicit Arguments.

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

Section AppendixC.

Variables (gT : finGroupType) (p q : nat) (H P P0 U Q : {group gT}).
Let nU := ((p ^ q).-1 %/ p.-1)%N.

External statement of the finite field assumption.
CoInductive finFieldImage : Prop :=
  FinFieldImage (F : finFieldType) (sigma : {morphism P >-> F}) of
     isom P [set: F] sigma & sigma @*^-1 <[1 : F]> = P0
   & exists2 sigmaU : {morphism U >-> {unit F}},
     'injm sigmaU & {in P & U, morph_act 'J 'U sigma sigmaU}.

These correspond to hypothesis (A) of B & G, Appendix C, Theorem C.
Hypotheses (pr_p : prime p) (pr_q : prime q) (coUp1 : coprime nU p.-1).
Hypotheses (defH : P ><| U = H) (fieldH : finFieldImage).
Hypotheses (oP : #|P| = (p ^ q)%N) (oU : #|U| = nU).

These correspond to hypothesis (B) of B & G, Appendix C, Theorem C.
Hypotheses (abelQ : q.-abelem Q) (nQP0 : P0 \subset 'N(Q)).
Hypothesis nU_P0Q : exists2 y, y \in Q & P0 :^ y \subset 'N(U).

Section ExpandHypotheses.

Negation of the goal of B & G, Appendix C, Theorem C.
Hypothesis ltqp : (q < p)%N.

From the fieldH assumption.
Variables (fT : finFieldType) (charFp : p \in [char fT]).
Local Notation F := (PrimeCharType charFp).
Local Notation galF := [splittingFieldType 'F_p of F].
Let Fpq : {vspace F} := fullv.
Let Fp : {vspace F} := 1%VS.

Hypothesis oF : #|F| = (p ^ q)%N.
Let oF_p : #|'F_p| = p.
Let oFp : #|Fp| = p.
Let oFpq : #|Fpq| = (p ^ q)%N.
Let dimFpq : \dim Fpq = q.

Variables (sigma : {morphism P >-> F}) (sigmaU : {morphism U >-> {unit F}}).
Hypotheses (inj_sigma : 'injm sigma) (inj_sigmaU : 'injm sigmaU).
Hypothesis im_sigma : sigma @* P = [set: F].
Variable s : gT.
Hypotheses (sP0P : P0 \subset P) (sigma_s : sigma s = 1) (defP0 : <[s]> = P0).

Let psi u : F := val (sigmaU u).
Let inj_psi : {in U &, injective psi}.

Hypothesis sigmaJ : {in P & U, x u, sigma (x ^ u) = sigma x × psi u}.

Let Ps : s \in P.
Let P0s : s \in P0.

Let nz_psi u : psi u != 0.

Let sigma1 : sigma 1%g = 0.
Let sigmaM : {in P &, {morph sigma : x1 x2 / (x1 × x2)%g >-> x1 + x2}}.
Let sigmaV : {in P, {morph sigma : x / x^-1%g >-> - x}}.
Let sigmaX n : {in P, {morph sigma : x / (x ^+ n)%g >-> x *+ n}}.

Let psi1 : psi 1%g = 1.
Let psiM : {in U &, {morph psi : u1 u2 / (u1 × u2)%g >-> u1 × u2}}.
Let psiV : {in U, {morph psi : u / u^-1%g >-> u^-1}}.
Let psiX n : {in U, {morph psi : u / (u ^+ n)%g >-> u ^+ n}}.

Let sigmaE := (sigma1, sigma_s, mulr1, mul1r,
               (sigmaJ, sigmaX, sigmaM, sigmaV), (psi1, psiX, psiM, psiV)).

Let psiE u : u \in Upsi u = sigma (s ^ u).

Let nPU : U \subset 'N(P).
Let memJ_P : {in P & U, x u, x ^ u \in P}.
Let in_PU := (memJ_P, in_group).

Let sigmaP0 : sigma @* P0 =i Fp.

Let nt_s : s != 1%g.

Let p_gt0 : (0 < p)%N.
Let q_gt0 : (0 < q)%N.
Let p1_gt0 : (0 < p.-1)%N.

This is B & G, Appendix C, Remark I.
Let not_dvd_q_p1 : ~~ (q %| p.-1)%N.

This is the first assertion of B & G, Appendix C, Remark V.
Let odd_p : odd p.

This is the second assertion of B & G, Appendix C, Remark V.
Let odd_q : odd q.

Let qgt2 : (2 < q)%N.
Let pgt4 : (4 < p)%N.
Let qgt1 : (1 < q)%N.

Local Notation Nm := (galNorm Fp Fpq).
Local Notation uval := (@FinRing.uval _).

Let cycFU (FU : {group {unit F}}) : cyclic FU.
Let cUU : abelian U.

This is B & G, Appendix C, Remark VII.
Let im_psi (x : F) : (x \in psi @: U) = (Nm x == 1).

This is B & G, Appendix C, Remark VIII.
This is B & G, Appendix C, Remark IX.
From the abelQ assumption of Peterfalvi, Theorem (14.2) to the assumptions of part (B) of the assumptions of Theorem C.
Let p'q : q != p.
Let cQQ : abelian Q.
Let p'Q : p^'.-group Q.

Let pP : p.-group P.
Let coQP : coprime #|Q| #|P|.
Let sQP0Q : [~: Q, P0] \subset Q.

This is B & G, Appendix C, Remark X.
Let defQ : 'C_Q(P0) \x [~: Q, P0] = Q.

This is B & G, Appendix C, Remark XI.
Let nU_P0QP0 : exists2 y, y \in [~: Q, P0] & P0 :^ y \subset 'N(U).

Let E := [set x : galF | Nm x == 1 & Nm (2%:R - x) == 1].

Let E_1 : 1 \in E.

This is B & G, Appendix C, Lemma C.1.
Let Einv_gt1_le_pq : E = [set x^-1 | x in E] → (1 < #|E|)%N → (p q)%N.

This is B & G, Appendix C, Lemma C.2.
Let E_gt1 : (1 < #|E|)%N.

Section AppendixC3.

Import GroupScope.

Variables y : gT.
Hypotheses (QP0y : y \in [~: Q, P0]) (nUP0y : P0 :^ y \subset 'N(U)).
Let Qy : y \in Q.

Let t := s ^ y.
Let P1 := P0 :^ y.

This is B & G, Appendix C, Lemma C.3, Step 1.
Let splitH x :
     x \in H
  exists2 u, u \in U & exists2 v, v \in U & exists2 s1, s1 \in P0
  & x = u × s1 × v.

This is B & G, Appendix C, Lemma C.3, Step 2.
Let not_splitU s1 s2 u :
  s1 \in P0s2 \in P0u \in Us1 × u × s2 \in U
  (s1 == 1) && (s2 == 1) || (u == 1) && (s1 × s2 == 1).

This is B & G, Appendix C, Lemma C.3, Step 3.
Let tiH_P1 t1 : t1 \in P1^#H :&: H :^ t1 = U.

This is B & G, Appendix C, Lemma C.3, Step 4.
This is B & G, Appendix C, Theorem C.
Theorem prime_dim_normed_finField : (p q)%N.

End AppendixC.