(Joint Center)Library BGsection2

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

This file covers the useful material in B & G, Section 2. This excludes part (c) of Proposition 2.1 and part (b) of Proposition 2.2, which are not actually used in the rest of the proof; also the rest of Proposition 2.1 is already covered by material in file mxrepresentation.v.

Set Implicit Arguments.

Section BGsection2.

Import GroupScope GRing.Theory FinRing.Theory poly.UnityRootTheory ssrint.IntDist.
Local Open Scope ring_scope.

Implicit Types (F : fieldType) (gT : finGroupType) (p : nat).

File mxrepresentation.v covers B & G, Proposition 2.1 as follows:
  • Proposition 2.1 (a) is covered by Lemmas mx_abs_irr_cent_scalar and cent_mx_scalar_abs_irr.
  • Proposition 2.2 (b) is our definition of "absolutely irreducible", and is thus covered by cent_mx_scalar_abs_irr and mx_abs_irrP.
  • Proposition 2.2 (c) is partly covered by the construction in submodule MatrixGenField, which extends the base field with a single element a of K = Hom_FG(M, M), rather than all of K, thus avoiding the use of the Wedderburn theorem on finite division rings (by the primitive element theorem this is actually equivalent). The corresponding representation is built by MatrixGenField.gen_repr. In B & G, Proposition 2.1(c) is only used in case II of the proof of Theorem 3.10, which we greatly simplify by making use of the Wielandt fixpoint formula, following Peterfalvi (Theorem 9.1). In this formalization the limited form of 2.1(c) is used to streamline the proof that groups of odd order are p-stable (B & G, Appendix A.5(c)).
This is B & G, Proposition 2.2(a), using internal isomorphims (mx_iso).
Proposition mx_irr_prime_index F gT (G H : {group gT}) n M (nsHG : H <| G)
    (rG : mx_representation F G n) (rH := subg_repr rG (normal_sub nsHG)) :
    group_closure_field F gTmx_irreducible rGcyclic (G / H)%g
    mxsimple rH M{in G, x, mx_iso rH M (M ×m rG x)}
  mx_irreducible rH.

This is B & G, Lemma 2.3. Note that this is not used in the FT proof.
Lemma rank_abs_irr_dvd_solvable F gT (G : {group gT}) n rG :
  @mx_absolutely_irreducible F _ G n rGsolvable Gn %| #|G|.

This section covers the many parts B & G, Proposition 2.4; only the last part (k) in used in the rest of the proof, and then only for Theorem 2.5.
Section QuasiRegularCyclic.

Variables (F : fieldType) (q' h : nat).

Local Notation q := q'.+1.
Local Notation V := 'rV[F]_q.
Local Notation E := 'M[F]_q.

Variables (g : E) (eps : F).

Hypothesis gh1 : g ^+ h = 1.
Hypothesis prim_eps : h.-primitive_root eps.

Let h_gt0 := prim_order_gt0 prim_eps.
Let eps_h := prim_expr_order prim_eps.
Let eps_mod_h m := expr_mod m eps_h.
Let inj_eps : injective (fun i : 'I_heps ^+ i).

Let inhP m : m %% h < h.
Let inh m := Ordinal (inhP m).

Let V_ i := eigenspace g (eps ^+ i).
Let n_ i := \rank (V_ i).
Let E_ i := eigenspace (lin_mx (mulmx g^-1 \o mulmxr g)) (eps ^+ i).
Let E2_ i t :=
  (kermx (lin_mx (mulmxr (cokermx (V_ t)) \o mulmx (V_ i)))
   :&: kermx (lin_mx (mulmx (\sum_(j < h | j != i %[mod h]) V_ j)%MS)))%MS.

Local Notation "''V_' i" := (V_ i) (at level 8, i at level 2, format "''V_' i").
Local Notation "''n_' i" := (n_ i) (at level 8, i at level 2, format "''n_' i").
Local Notation "''E_' i" := (E_ i) (at level 8, i at level 2, format "''E_' i").
Local Notation "'E_ ( i )" := (E_ i) (at level 8, only parsing).
Local Notation "e ^g" := (g^-1 ×m (e ×m g))
  (at level 8, format "e ^g") : ring_scope.
Local Notation "'E_ ( i , t )" := (E2_ i t)
  (at level 8, format "''E_' ( i , t )").

Let inj_g : g \in GRing.unit.

Let Vi_mod i : 'V_(i %% h) = 'V_i.

Let g_mod i := expr_mod i gh1.

Let EiP i e : reflect (e^g = eps ^+ i *: e) (e \in 'E_i)%MS.

Let E2iP i t e :
  reflect ('V_i ×m e 'V_t j, j != i %[mod h]'V_j ×m e = 0)%MS
          (e \in 'E_(i, t))%MS.

Let sumV := (\sum_(i < h) 'V_i)%MS.

This is B & G, Proposition 2.4(a).
This is B & G, Proposition 2.4(b).
Proposition rank_step_eigenspace_cycle i : 'n_ (i + h) = 'n_ i.

Let sumE := (\sum_(it : 'I_h × 'I_h) 'E_(it.1, it.2))%MS.

This is B & G, Proposition 2.4(c).
This is B & G, Proposition 2.4(d).
This is B & G, Proposition 2.4(e).
Proposition proj_eigenspace_cycle_sub_quasi_cent i j :
  ('E_(i, i + j) 'E_j)%MS.

Let diagE m :=
  (\sum_(it : 'I_h × 'I_h | it.1 + m == it.2 %[mod h]) 'E_(it.1, it.2))%MS.

This is B & G, Proposition 2.4(f).
This is B & G, Proposition 2.4(g).
Proposition rank_quasi_cent_cycle m :
  \rank 'E_m = (\sum_(i < h) 'n_i × 'n_(i + m))%N.

This is B & G, Proposition 2.4(h).
Proposition diff_rank_quasi_cent_cycle m :
  (2 × \rank 'E_0 = 2 × \rank 'E_m + \sum_(i < h) `|'n_i - 'n_(i + m)| ^ 2)%N.

Hypothesis rankEm : m, m != 0 %[mod h]\rank 'E_0 = (\rank 'E_m).+1.

This is B & G, Proposition 2.4(j).
Proposition rank_eigenspaces_quasi_homocyclic :
  exists2 n, `|q - h × n| = 1%N &
   i : 'I_h, [/\ `|'n_i - n| = 1%N, (q < h × n) = ('n_i < n)
                     & j, j != i'n_j = n].

This is B & G, Proposition 2.4(k).
Proposition rank_eigenspaces_free_quasi_homocyclic :
  q > 1 → 'n_0 = 0%Nh = q.+1 ( j, j != 0 %[mod h]'n_j = 1%N).

End QuasiRegularCyclic.

This is B & G, Theorem 2.5, used for Theorems 3.4 and 15.7.
Theorem repr_extraspecial_prime_sdprod_cycle p n gT (G P H : {group gT}) :
    p.-group Pextraspecial PP ><| H = Gcyclic H
    let h := #|H| in #|P| = (p ^ n.*2.+1)%Ncoprime p h
    {in H^#, x, 'C_P[x] = 'Z(P)}
  (h %| p ^ n + 1) || (h %| p ^ n - 1)
   ((h != p ^ n + 1)%N F q (rG : mx_representation F G q),
      [char F]^'.-group Gmx_faithful rGrfix_mx rG H != 0).

This is the main part of B & G, Theorem 2.6; it implies 2.6(a) and most of 2.6(b).
Theorem der1_odd_GL2_charf F gT (G : {group gT})
                           (rG : mx_representation F G 2) :
 odd #|G|mx_faithful rG[char F].-group G^`(1)%g.

This is B & G, Theorem 2.6(a)
Theorem charf'_GL2_abelian F gT (G : {group gT})
                           (rG : mx_representation F G 2) :
  odd #|G|mx_faithful rG[char F]^'.-group Gabelian G.

This is B & G, Theorem 2.6(b)
Theorem charf_GL2_der_subS_abelian_Sylow p F gT (G : {group gT})
                                         (rG : mx_representation F G 2) :
    odd #|G|mx_faithful rGp \in [char F]
   P : {group gT}, [/\ p.-Sylow(G) P, abelian P & G^`(1)%g \subset P].

This is B & G, Lemma 2.7.
Lemma regular_abelem2_on_abelem2 p q gT (P Q : {group gT}) :
    p.-abelem Pq.-abelem Q'r_p(P) = 2 →'r_q(Q) = 2 →
    Q \subset 'N(P)'C_Q(P) = 1%g
  (q %| p.-1)%N
   (exists2 a, a \in Q^# & r,
      [/\ {in P, x, x ^ a = x ^+ r}%g,
          r ^ q = 1 %[mod p] & r != 1 %[mod p]]).

End BGsection2.