(Joint Center)Library PFsection4

(* (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 fingroup.
Require Import morphism perm automorphism quotient action gfunctor gproduct.
Require Import center commutator zmodp cyclic pgroup nilpotent hall frobenius.
Require Import matrix mxalgebra mxrepresentation vector ssrnum algC classfun.
Require Import character inertia vcharacter PFsection1 PFsection2 PFsection3.

This file covers Peterfalvi, Section 4: The Dade isometry of a certain type of subgroup. Given defW : W1 \x W2 = W, we define here: primeTI_hypothesis L K defW <-> L = K ><| W1, where W1 acts in a prime manner on K (see semiprime in frobenius.v), and both W1 and W2 = 'C_K(W1) are nontrivial and cyclic of odd order; these conditions imply that cyclicTI_hypothesis L defW holds.
  • > This is Peterfalvi, Hypothesis (4.2), or Feit-Thompson (13.2).
prime_Dade_definition L K H A A0 defW <-> A0 = A :|: class_support (cyclicTIset defW) L where A is an L-invariant subset of K^# containing all the elements of K that do not act freely on H <| L; in addition W2 \subset H \subset K. prime_Dade_hypothesis G L K H A A0 defW <-> The four assumptions primeTI_hypothesis L K defW, cyclicTI_hypothesis G defW, Dade_hypothesis G L A0 and prime_Dade_definition L K H A A0 defW hold jointly.
  • > This is Peterfalvi, Hypothesis (4.6), or Feit-Thompson (13.3) (except that H is not required to be nilpotent, and the "supporting groups" assumptions have been replaced by Dade hypothesis).
  • > This hypothesis is one of the alternatives under which Sibley's coherence theorem holds (see PFsection6.v), and is verified by all maximal subgroups of type P in a minimal simple odd group.
  • > prime_Dade_hypothesis coerces to Dade_hypothesis, cyclicTI_hypothesis, primeTI_hypothesis and prime_Dade_definition.
For ptiW : primeTI_hypothesis L K defW we also define: prime_cycTIhyp ptiW :: cyclicTI_hypothesis L defW (though NOT a coercion) primeTIirr ptiW i j == the (unique) irreducible constituent of the image (locally) mu2_ i j in 'CF(L) of w_ i j = cyclicTIirr defW i j under the sigma = cyclicTIiso (prime_cycTIhyp ptiW). primeTI_Iirr ptiW ij == the index of mu2_ ij.1 ij.2; indeed mu2_ i j is just notation for 'chi_(primeTI_Iirr ptiW (i, j)). primeTIsign ptiW j == the sign of mu2_ i j in sigma (w_ i j), which does (locally) delta_ j not depend on i. primeTI_Isign ptiW j == the boolean b such that delta_ j := (-1) ^+ b. primeTIres ptiW j == the restriction to K of mu2_ i j, which is an (locally) chi_ j irreducible character that does not depend on i. primeTI_Ires ptiW j == the index of chi_ j := 'chi_(primeTI_Ires ptiW j). primeTIred ptiW j == the (reducible) character equal to the sum of all (locally) mu_ j the mu2_ i j, and also to 'Ind (chi_ j). uniform_prTIred_seq ptiW k == the sequence of all the mu_ j, j != 0, with the same degree as mu_ k (s.t. mu_ j 1 = mu_ k 1).

Set Implicit Arguments.

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

Section Four_1_to_2.

This is Peterfalvi (4.1).

Variable gT : finGroupType.

Lemma vchar_pairs_orthonormal (X : {group gT}) (a b c d : 'CF(X)) u v :
    {subset (a :: b) 'Z[irr X]} {subset (c :: d) 'Z[irr X]}
    orthonormal (a :: b) && orthonormal (c :: d) →
    [&& u \is Creal, v \is Creal, u != 0 & v != 0]
    [&& '[a - b, u *: c - v *: d] == 0,
         (a - b) 1%g == 0 & (u *: c - v *: d) 1%g == 0]
    orthonormal [:: a; b; c; d].

Corollary orthonormal_vchar_diff_ortho (X : {group gT}) (a b c d : 'CF(X)) :
    {subset a :: b 'Z[irr X]} {subset c :: d 'Z[irr X]}
    orthonormal (a :: b) && orthonormal (c :: d) →
    [&& '[a - b, c - d] == 0, (a - b) 1%g == 0 & (c - d) 1%g == 0]
  '[a, c] = 0.

This is Peterfalvi, Hypothesis (4.2), with explicit parameters.
Definition primeTI_hypothesis (L K W W1 W2 : {set gT}) of W1 \x W2 = W :=
  [/\ (*a*) [/\ K ><| W1 = L, W1 != 1, Hall L W1 & cyclic W1],
      (*b*) [/\ W2 != 1, W2 \subset K & cyclic W2],
            {in W1^#, x, 'C_K[x] = W2}
   & (*c*) odd #|W|]%g.

End Four_1_to_2.


Section Four_3_to_5.

Variables (gT : finGroupType) (L K W W1 W2 : {group gT}) (defW : W1 \x W2 = W).
Hypothesis ptiWL : primeTI_hypothesis L K defW.

Let V := cyclicTIset defW.
Let w1 := #|W1|.
Let w2 := #|W2|.

Let defL : K ><| W1 = L.
Let ntW1 : W1 :!=: 1%g.
Let cycW1 : cyclic W1.
Let hallW1 : Hall L W1.

Let ntW2 : W2 :!=: 1%g.
Let sW2K : W2 \subset K.
Let cycW2 : cyclic W2.
Let prKW1 : {in W1^#, x, 'C_K[x] = W2}.

Let oddW : odd #|W|.

Let nsKL : K <| L.
Let sKL : K \subset L.
Let sW1L : W1 \subset L.
Let sWL : W \subset L.
Let sW1W : W1 \subset W.
Let sW2W : W2 \subset W.

Let coKW1 : coprime #|K| #|W1|.
Let coW12 : coprime #|W1| #|W2|.

Let cycW : cyclic W.
Let cWW : abelian W.
Let oddW1 : odd w1.
Let oddW2 : odd w2.

Let ntV : V != set0.

Let sV_V2 : V \subset W :\: W2.

Lemma primeTIhyp_quotient (M : {group gT}) :
    (W2 / M != 1)%gM \subset KM <| L
  {defWbar : (W1 / M) \x (W2 / M) = W / M
           & primeTI_hypothesis (L / M) (K / M) defWbar}%g.

This is the first part of PeterFalvi, Theorem (4.3)(a).
Second part of PeterFalvi, Theorem (4.3)(a).
Theorem prime_cycTIhyp : cyclicTI_hypothesis L defW.
Local Notation ctiW := prime_cycTIhyp.
Let sigma := cyclicTIiso ctiW.
Let w_ i j := cyclicTIirr defW i j.

Let Wlin k : 'chi[W]_k \is a linear_char.
Let W1lin i : 'chi[W1]_i \is a linear_char.
Let W2lin i : 'chi[W2]_i \is a linear_char.
Let w_lin i j : w_ i j \is a linear_char.

Let nirrW1 : #|Iirr W1| = w1.
Let nirrW2 : #|Iirr W2| = w2.
Let NirrW1 : Nirr W1 = w1.
Let NirrW2 : Nirr W2 = w2.
Let w1gt1 : (1 < w1)%N.

Let cfdot_w i1 j1 i2 j2 : '[w_ i1 j1, w_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.

Witnesses for Theorem (4.3)(b).
Fact primeTIdIirr_key : unit.
Definition primeTIdIirr_def := dirr_dIirr (sigma \o prod_curry w_).
Definition primeTIdIirr := locked_with primeTIdIirr_key primeTIdIirr_def.
Definition primeTI_Iirr ij := (primeTIdIirr ij).2.
Definition primeTI_Isign j := (primeTIdIirr (0, j)).1.
Local Notation Imu2 := primeTI_Iirr.
Local Notation mu2_ i j := 'chi_(primeTI_Iirr (i, j)).
Local Notation delta_ j := (GRing.sign algCring (primeTI_Isign j)).

Let ew_ i j := w_ i j - w_ 0 j.
Let V2ew i j : ew_ i j \in 'CF(W, W :\: W2).

This is Peterfalvi, Theorem (4.3)(b, c).
Theorem primeTIirr_spec :
 [/\ (*b*) injective Imu2,
            i j, 'Ind (ew_ i j) = delta_ j *: (mu2_ i j - mu2_ 0 j),
            i j, sigma (w_ i j) = delta_ j *: mu2_ i j,
     (*c*) i j, {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j}
         & k, k \notin codom Imu2{in W :\: W2, 'chi_k =1 \0}].

These lemmas restate the various parts of Theorem (4.3)(b, c) separately.
Lemma prTIirr_inj : injective Imu2.

Corollary cfdot_prTIirr i1 j1 i2 j2 :
  '[mu2_ i1 j1, mu2_ i2 j2] = ((i1 == i2) && (j1 == j2))%:R.

Lemma cfInd_sub_prTIirr i j :
  'Ind[L] (w_ i j - w_ 0 j) = delta_ j *: (mu2_ i j - mu2_ 0 j).

Lemma cycTIiso_prTIirr i j : sigma (w_ i j) = delta_ j *: mu2_ i j.

Lemma prTIirr_id i j : {in W :\: W2, mu2_ i j =1 delta_ j *: w_ i j}.

Lemma not_prTIirr_vanish k : k \notin codom Imu2{in W :\: W2, 'chi_k =1 \0}.

This is Peterfalvi, Theorem (4.3)(d).
Theorem prTIirr1_mod i j : (mu2_ i j 1%g == delta_ j %[mod w1])%C.

Lemma prTIsign_aut u j : delta_ (aut_Iirr u j) = delta_ j.

Lemma prTIirr_aut u i j :
  mu2_ (aut_Iirr u i) (aut_Iirr u j) = cfAut u (mu2_ i j).

The (reducible) column sums of the prime TI irreducibles.
Definition primeTIred j : 'CF(L) := \sum_i mu2_ i j.
Local Notation mu_ := primeTIred.

Definition uniform_prTIred_seq j0 :=
  image mu_ [pred j | j != 0 & mu_ j 1%g == mu_ j0 1%g].

Lemma prTIred_aut u j : mu_ (aut_Iirr u j) = cfAut u (mu_ j).

Lemma cfdot_prTIirr_red i j k : '[mu2_ i j, mu_ k] = (j == k)%:R.

Lemma cfdot_prTIred j1 j2 : '[mu_ j1, mu_ j2] = ((j1 == j2) × w1)%:R.

Lemma cfnorm_prTIred j : '[mu_ j] = w1%:R.

Lemma prTIred_neq0 j : mu_ j != 0.

Lemma prTIred_char j : mu_ j \is a character.

Lemma prTIred_1_gt0 j : 0 < mu_ j 1%g.

Lemma prTIred_1_neq0 i : mu_ i 1%g != 0.

Lemma prTIred_inj : injective mu_.

Lemma prTIred_not_real j : j != 0 → ~~ cfReal (mu_ j).

Lemma prTIsign0 : delta_ 0 = 1.

Lemma prTIirr00 : mu2_ 0 0 = 1.

This is PeterFalvi (4.4).
Lemma prTIirr0P k :
  reflect ( i, 'chi_k = mu2_ i 0) (K \subset cfker 'chi_k).

This is the first part of PeterFalvi, Theorem (4.5)(a).
Theorem cfRes_prTIirr_eq0 i j : 'Res[K] (mu2_ i j) = 'Res (mu2_ 0 j).

Lemma prTIirr_1 i j : mu2_ i j 1%g = mu2_ 0 j 1%g.

Lemma prTIirr0_1 i : mu2_ i 0 1%g = 1.

Lemma prTIirr0_linear i : mu2_ i 0 \is a linear_char.

Lemma prTIred_1 j : mu_ j 1%g = w1%:R × mu2_ 0 j 1%g.

Definition primeTI_Ires j : Iirr K := cfIirr ('Res[K] (mu2_ 0 j)).
Local Notation Ichi := primeTI_Ires.
Local Notation chi_ j := 'chi_(Ichi j).

This is the rest of PeterFalvi, Theorem (4.5)(a).
Theorem prTIres_spec j : chi_ j = 'Res (mu2_ 0 j) mu_ j = 'Ind (chi_ j).

Lemma cfRes_prTIirr i j : 'Res[K] (mu2_ i j) = chi_ j.

Lemma cfInd_prTIres j : 'Ind[L] (chi_ j) = mu_ j.

Lemma cfRes_prTIred j : 'Res[K] (mu_ j) = w1%:R *: chi_ j.

Lemma prTIres_aut u j : chi_ (aut_Iirr u j) = cfAut u (chi_ j).

Lemma prTIres0 : chi_ 0 = 1.

Lemma prTIred0 : mu_ 0 = w1%:R *: '1_K.

Lemma prTIres_inj : injective Ichi.

This is the first assertion of Peterfalvi (4.5)(b).
Theorem prTIres_irr_cases k (theta := 'chi_k) (phi := 'Ind theta) :
  {j | theta = chi_ j} + {phi \in irr L ( i j, phi != mu2_ i j)}.

Implicit elementary converse to the above.
This is the second assertion of Peterfalvi (4.5)(b).
Theorem prTIind_irr_cases ell (phi := 'chi_ell) :
   {i : _ & {j | phi = mu2_ i j}}
     + {k | k \notin codom Ichi & phi = 'Ind 'chi_k}.

End Four_3_to_5.

Notation primeTIsign ptiW j :=
  (GRing.sign algCring (primeTI_Isign ptiW j)) (only parsing).
Notation primeTIirr ptiW i j := 'chi_(primeTI_Iirr ptiW (i, j)) (only parsing).
Notation primeTIres ptiW j := 'chi_(primeTI_Ires ptiW j) (only parsing).

Implicit Arguments prTIirr_inj [gT L K W W1 W2 defW x1 x2].
Implicit Arguments prTIred_inj [gT L K W W1 W2 defW x1 x2].
Implicit Arguments prTIres_inj [gT L K W W1 W2 defW x1 x2].
Implicit Arguments not_prTIirr_vanish [gT L K W W1 W2 defW k].

Section Four_6_t0_10.

Variables (gT : finGroupType) (G L K H : {group gT}) (A A0 : {set gT}).
Variables (W W1 W2 : {group gT}) (defW : W1 \x W2 = W).

Local Notation V := (cyclicTIset defW).

These correspond to Peterfalvi, Hypothesis (4.6).
Definition prime_Dade_definition :=
  [/\ (*c*) [/\ H <| L, W2 \subset H & H \subset K],
      (*d*) [/\ A <| L, \bigcup_(h in H^#) 'C_K[h]^# \subset A & A \subset K^#]
    & (*e*) A0 = A :|: class_support V L].

Record prime_Dade_hypothesis : Prop := PrimeDadeHypothesis {
  prDade_cycTI :> cyclicTI_hypothesis G defW;
  prDade_prTI :> primeTI_hypothesis L K defW;
  prDade_hyp :> Dade_hypothesis G L A0;
  prDade_def :> prime_Dade_definition
}.

Hypothesis prDadeHyp : prime_Dade_hypothesis.

Let ctiWG : cyclicTI_hypothesis G defW := prDadeHyp.
Let ptiWL : primeTI_hypothesis L K defW := prDadeHyp.
Let ctiWL : cyclicTI_hypothesis L defW := prime_cycTIhyp ptiWL.
Let ddA0 : Dade_hypothesis G L A0 := prDadeHyp.
Local Notation ddA0def := (prDade_def prDadeHyp).

Local Notation w_ i j := (cyclicTIirr defW i j).
Local Notation sigma := (cyclicTIiso ctiWG).
Local Notation eta_ i j := (sigma (w_ i j)).
Local Notation mu2_ i j := (primeTIirr ptiWL i j).
Local Notation delta_ j := (primeTIsign ptiWL j).
Local Notation chi_ j := (primeTIres ptiWL j).
Local Notation mu_ := (primeTIred ptiWL).
Local Notation tau := (Dade ddA0).

Let defA0 : A0 = A :|: class_support V L.
Let nsAL : A <| L.
Let sAA0 : A \subset A0.

Let nsHL : H <| L.
Let sHK : H \subset K.
Let defL : K ><| W1 = L.
Let sKL : K \subset L.
Let coKW1 : coprime #|K| #|W1|.

Let sIH_A : \bigcup_(h in H^#) 'C_K[h]^# \subset A.

Let sW2H : W2 \subset H.
Let ntW1 : W1 :!=: 1%g.
Let ntW2 : W2 :!=: 1%g.

Let oddW : odd #|W|.
Let sW1W : W1 \subset W.
Let sW2W : W2 \subset W.
Let tiW12 : W1 :&: W2 = 1%g.

Let cycW : cyclic W.
Let cycW1 : cyclic W1.
Let cycW2 : cyclic W2.
Let sLG : L \subset G.
Let sW2K : W2 \subset K.

Let sWL : W \subset L.
Let sWG : W \subset G.

Let oddW1 : odd #|W1|.
Let oddW2 : odd #|W2|.

Let w1gt1 : (2 < #|W1|)%N.
Let w2gt2 : (2 < #|W2|)%N.

Let nirrW1 : #|Iirr W1| = #|W1|.
Let nirrW2 : #|Iirr W2| = #|W2|.
Let W1lin i : 'chi[W1]_i \is a linear_char.
Let W2lin i : 'chi[W2]_i \is a linear_char.

This is the first part of Peterfalvi (4.7).
Lemma prDade_irr_on k :
   ~~ (H \subset cfker 'chi[K]_k)'chi_k \in 'CF(K, 1%g |: A).

This is the second part of Peterfalvi (4.7).
Third part of Peterfalvi (4.7).
Lemma cfker_prTIres j : j != 0 → ~~ (H \subset cfker (chi_ j)).

Fourth part of Peterfalvi (4.7).
Lemma prDade_TIres_on j : j != 0 → chi_ j \in 'CF(K, 1%g |: A).

Last part of Peterfalvi (4.7).
Lemma prDade_TIred_on j : j != 0 → mu_ j \in 'CF(L, 1%g |: A).

Import ssrint.

Second part of PeterFalvi (4.8).
Lemma prDade_TIsign_eq i j k :
  mu2_ i j 1%g = mu2_ i k 1%gdelta_ j = delta_ k.

First part of PeterFalvi (4.8).
Lemma prDade_sub_TIirr_on i j k :
    j != 0 → k != 0 → mu2_ i j 1%g = mu2_ i k 1%g
  mu2_ i j - mu2_ i k \in 'CF(L, A0).

This is last part of PeterFalvi (4.8).
Lemma prDade_sub_TIirr i j k :
    j != 0 → k != 0 → mu2_ i j 1%g = mu2_ i k 1%g
  tau (mu2_ i j - mu2_ i k) = delta_ j *: (eta_ i j - eta_ i k).

Lemma prDade_supp_disjoint : V \subset ~: K.

This is Peterfalvi (4.9). We have added the "obvious" fact that calT is pairwise orthogonal, since we require this to prove membership in 'Z[calT], we encapsulate the construction of tau1, and state its conformance to tau on the "larger" domain 'Z[calT, L^# ], so that clients can avoid using the domain equation in part (a).
Theorem uniform_prTIred_coherent k (calT := uniform_prTIred_seq ptiWL k) :
    k != 0 →
  (*a*) [/\ pairwise_orthogonal calT, ~~ has cfReal calT, conjC_closed calT,
            'Z[calT, L^#] =i 'Z[calT, A]
          & exists2 psi, psi != 0 & psi \in 'Z[calT, A]]
(*b*) (exists2 tau1 : {linear 'CF(L)'CF(G)},
            j, tau1 (mu_ j) = delta_ k *: (\sum_i sigma (w_ i j))
         & {in 'Z[calT], isometry tau1, to 'Z[irr G]}
         {in 'Z[calT, L^#], tau1 =1 tau}).

This is Peterfalvi (4.10).
Lemma prDade_sub2_TIirr i j :
  tau (delta_ j *: mu2_ i j - delta_ j *: mu2_ 0 j - mu2_ i 0 + mu2_ 0 0)
    = eta_ i j - eta_ 0 j - eta_ i 0 + eta_ 0 0.

End Four_6_t0_10.