diff options
| author | Enrico Tassi | 2018-04-17 16:57:13 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-04-17 16:57:13 +0200 |
| commit | eaa90cf9520e43d0b05fc6431a479e6b9559ef0e (patch) | |
| tree | 8499953a468a8d8be510dd0d60232cbd8984c1ec /mathcomp/odd_order/PFsection10.v | |
| parent | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (diff) | |
move odd_order to its own repository
Diffstat (limited to 'mathcomp/odd_order/PFsection10.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection10.v | 1230 |
1 files changed, 0 insertions, 1230 deletions
diff --git a/mathcomp/odd_order/PFsection10.v b/mathcomp/odd_order/PFsection10.v deleted file mode 100644 index 03d8898..0000000 --- a/mathcomp/odd_order/PFsection10.v +++ /dev/null @@ -1,1230 +0,0 @@ -(* (c) Copyright 2006-2016 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) -Require Import mathcomp.ssreflect.ssreflect. -From mathcomp -Require Import ssrbool ssrfun eqtype ssrnat seq path div choice. -From mathcomp -Require Import fintype tuple finfun bigop prime ssralg poly finset center. -From mathcomp -Require Import fingroup morphism perm automorphism quotient action finalg zmodp. -From mathcomp -Require Import gfunctor gproduct cyclic commutator gseries nilpotent pgroup. -From mathcomp -Require Import sylow hall abelian maximal frobenius. -From mathcomp -Require Import matrix mxalgebra mxrepresentation mxabelem vector. -From mathcomp -Require Import BGsection1 BGsection3 BGsection7 BGsection15 BGsection16. -From mathcomp -Require Import ssrnum algC classfun character integral_char inertia vcharacter. -From mathcomp -Require Import PFsection1 PFsection2 PFsection3 PFsection4. -From mathcomp -Require Import PFsection5 PFsection6 PFsection7 PFsection8 PFsection9. - -(******************************************************************************) -(* This file covers Peterfalvi, Section 10: Maximal subgroups of Types III, *) -(* IV and V. For defW : W1 \x W2 = W and MtypeP : of_typeP M U defW, and *) -(* setting ptiW := FT_primeTI_hyp MtypeP, mu2_ i j := primeTIirr ptiW i j and *) -(* delta_ j := primeTIsign j, we define here, for M of type III-V: *) -(* FTtype345_TIirr_degree MtypeP == the common degree of the components of *) -(* (locally) d the images of characters of irr W that don't have *) -(* W2 in their kernel by the cyclicTI isometry to M. *) -(* Thus mu2_ i j 1%g = d%:R for all j != 0. *) -(* FTtype345_TIsign MtypeP == the common sign of the images of characters *) -(* (locally) delta of characters of irr W that don't have W2 in *) -(* their kernel by the cyclicTI isometry to M. *) -(* Thus delta_ j = delta for all j != 0. *) -(* FTtype345_ratio MtypeP == the ratio (d - delta) / #|W1|. Even though it *) -(* (locally) n is always a positive integer we take n : algC. *) -(* FTtype345_bridge MtypeP s i j == a virtual character that can be used to *) -(* (locally) alpha_ i j bridge coherence between the mu2_ i j and other *) -(* irreducibles of M; here s should be the index of *) -(* an irreducible character of M induced from M^(1). *) -(* := mu2_ i j - delta *: mu2_ i 0 -n *: 'chi_s. *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import GroupScope GRing.Theory Num.Theory. - -Section Ten. - -Variable gT : minSimpleOddGroupType. -Local Notation G := (TheMinSimpleOddGroup gT). -Implicit Types (p q : nat) (x y z : gT). -Implicit Types H K L N P Q R S T U W : {group gT}. - -Local Notation "#1" := (inord 1) (at level 0). - -Section OneMaximal. - -(* These assumptions correspond to Peterfalvi, Hypothesis (10.1). *) -(* We also declare the group U_M, even though it is not used in this section, *) -(* because it is a parameter to the theorems and definitions of PFsection8 *) -(* and PFsection9. *) -Variables M U_M W W1 W2 : {group gT}. -Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W). -Hypotheses (MtypeP : of_typeP M U_M defW) (notMtype2: FTtype M != 2). - -Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope. -Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope. -Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope. -Local Notation "` 'W'" := (gval W) (at level 0, only parsing) : group_scope. -Local Notation V := (cyclicTIset defW). -Local Notation M' := M^`(1)%G. -Local Notation "` 'M''" := `M^`(1) (at level 0) : group_scope. -Local Notation M'' := M^`(2)%G. -Local Notation "` 'M'''" := `M^`(2) (at level 0) : group_scope. - -Let defM : M' ><| W1 = M. Proof. by have [[]] := MtypeP. Qed. -Let nsM''M' : M'' <| M'. Proof. exact: (der_normal 1 M'). Qed. -Let nsM'M : M' <| M. Proof. exact: (der_normal 1 M). Qed. -Let sM'M : M' \subset M. Proof. exact: der_sub. Qed. -Let nsM''M : M'' <| M. Proof. exact: der_normal 2 M. Qed. - -Let notMtype1 : FTtype M != 1%N. Proof. exact: FTtypeP_neq1 MtypeP. Qed. -Let typeMgt2 : FTtype M > 2. -Proof. by move: (FTtype M) (FTtype_range M) notMtype1 notMtype2=> [|[|[]]]. Qed. - -Let defA1 : 'A1(M) = M'^#. Proof. by rewrite /= -FTcore_eq_der1. Qed. -Let defA : 'A(M) = M'^#. Proof. by rewrite FTsupp_eq1 ?defA1. Qed. -Let defA0 : 'A0(M) = M'^# :|: class_support V M. -Proof. by rewrite -defA (FTtypeP_supp0_def _ MtypeP). Qed. -Let defMs : M`_\s :=: M'. Proof. exact: FTcore_type_gt2. Qed. - -Let pddM := FT_prDade_hyp maxM MtypeP. -Let ptiWM : primeTI_hypothesis M M' defW := FT_primeTI_hyp MtypeP. -Let ctiWG : cyclicTI_hypothesis G defW := pddM. -Let ctiWM : cyclicTI_hypothesis M defW := prime_cycTIhyp ptiWM. - -Let ntW1 : W1 :!=: 1. Proof. by have [[]] := MtypeP. Qed. -Let ntW2 : W2 :!=: 1. Proof. by have [_ _ _ []] := MtypeP. Qed. -Let cycW1 : cyclic W1. Proof. by have [[]] := MtypeP. Qed. -Let cycW2 : cyclic W2. Proof. by have [_ _ _ []] := MtypeP. Qed. - -Let w1 := #|W1|. -Let w2 := #|W2|. -Let nirrW1 : #|Iirr W1| = w1. Proof. by rewrite card_Iirr_cyclic. Qed. -Let nirrW2 : #|Iirr W2| = w2. Proof. by rewrite card_Iirr_cyclic. Qed. -Let NirrW1 : Nirr W1 = w1. Proof. by rewrite -nirrW1 card_ord. Qed. -Let NirrW2 : Nirr W2 = w2. Proof. by rewrite -nirrW2 card_ord. Qed. - -Let w1gt2 : w1 > 2. Proof. by rewrite odd_gt2 ?mFT_odd ?cardG_gt1. Qed. -Let w2gt2 : w2 > 2. Proof. by rewrite odd_gt2 ?mFT_odd ?cardG_gt1. Qed. - -Let coM'w1 : coprime #|M'| w1. -Proof. by rewrite (coprime_sdprod_Hall_r defM); have [[]] := MtypeP. Qed. - -(* This is used both in (10.2) and (10.8). *) -Let frobMbar : [Frobenius M / M'' = (M' / M'') ><| (W1 / M'')]. -Proof. -have [[_ hallW1 _ _] _ _ [_ _ _ sW2M'' regM'W1 ] _] := MtypeP. -apply: Frobenius_coprime_quotient => //. -split=> [|w /regM'W1-> //]; apply: (sol_der1_proper (mmax_sol maxM)) => //. -by apply: subG1_contra ntW2; apply: subset_trans sW2M'' (der_sub 1 M'). -Qed. - -Local Open Scope ring_scope. - -Let sigma := (cyclicTIiso ctiWG). -Let w_ i j := (cyclicTIirr defW i j). -Local Notation eta_ i j := (sigma (w_ i j)). - -Local Notation Imu2 := (primeTI_Iirr ptiWM). -Let mu2_ i j := primeTIirr ptiWM i j. -Let mu_ := primeTIred ptiWM. -Local Notation chi_ j := (primeTIres ptiWM j). - -Local Notation Idelta := (primeTI_Isign ptiWM). -Local Notation delta_ j := (primeTIsign ptiWM j). - -Local Notation tau := (FT_Dade0 maxM). -Local Notation "chi ^\tau" := (tau chi). - -Let calS0 := seqIndD M' M M`_\s 1. -Let rmR := FTtypeP_coh_base maxM MtypeP. -Let scohS0 : subcoherent calS0 tau rmR. -Proof. exact: FTtypeP_subcoherent MtypeP. Qed. - -Let calS := seqIndD M' M M' 1. -Let sSS0 : cfConjC_subset calS calS0. -Proof. by apply: seqInd_conjC_subset1; rewrite /= ?defMs. Qed. - -Let mem_calS s : ('Ind 'chi[M']_s \in calS) = (s != 0). -Proof. -rewrite mem_seqInd ?normal1 ?FTcore_normal //=. -by rewrite !inE sub1G subGcfker andbT. -Qed. - -Let calSmu j : j != 0 -> mu_ j \in calS. -Proof. -move=> nz_j; rewrite -[mu_ j]cfInd_prTIres mem_calS -irr_eq1. -by rewrite -(prTIres0 ptiWM) (inj_eq irr_inj) (inj_eq (prTIres_inj _)). -Qed. - -Let tauM' : {subset 'Z[calS, M'^#] <= 'CF(M, 'A0(M))}. -Proof. by rewrite defA0 => phi /zchar_on/(cfun_onS (subsetUl _ _))->. Qed. - -(* This is Peterfalvi (10.2). *) -(* Note that this result is also valid for type II groups. *) -Lemma FTtypeP_ref_irr : - {zeta | [/\ zeta \in irr M, zeta \in calS & zeta 1%g = w1%:R]}. -Proof. -have [_ /has_nonprincipal_irr[s nz_s] _ _ _] := Frobenius_context frobMbar. -exists ('Ind 'chi_s %% M'')%CF; split. -- by rewrite cfMod_irr ?irr_induced_Frobenius_ker ?(FrobeniusWker frobMbar). -- by rewrite -cfIndMod ?normal_sub // -mod_IirrE // mem_calS mod_Iirr_eq0. -rewrite -cfIndMod ?cfInd1 ?normal_sub // -(index_sdprod defM) cfMod1. -by rewrite lin_char1 ?mulr1 //; apply/char_abelianP/sub_der1_abelian. -Qed. - -(* This is Peterfalvi (10.3), first assertion. *) -Lemma FTtype345_core_prime : prime w2. -Proof. -have [S pairMS [xdefW [U StypeP]]] := FTtypeP_pair_witness maxM MtypeP. -have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _ _. -by have [[]] := compl_of_typeII maxS StypeP Stype2. -Qed. -Let w2_pr := FTtype345_core_prime. - -Definition FTtype345_TIirr_degree := truncC (mu2_ 0 #1 1%g). -Definition FTtype345_TIsign := delta_ #1. -Local Notation d := FTtype345_TIirr_degree. -Local Notation delta := FTtype345_TIsign. -Definition FTtype345_ratio := (d%:R - delta) / w1%:R. -Local Notation n := FTtype345_ratio. - -(* This is the remainder of Peterfalvi (10.3). *) -Lemma FTtype345_constants : - [/\ forall i j, j != 0 -> mu2_ i j 1%g = d%:R, - forall j, j != 0 -> delta_ j = delta, - (d > 1)%N - & n \in Cnat]. -Proof. -have nz_j1 : #1 != 0 :> Iirr W2 by rewrite Iirr1_neq0. -have invj j: j != 0 -> mu2_ 0 j 1%g = d%:R /\ delta_ j = delta. - move=> nz_j; have [k co_k_j1 Dj] := cfExp_prime_transitive w2_pr nz_j1 nz_j. - rewrite -(cforder_dprodr defW) -dprod_IirrEr in co_k_j1. - have{co_k_j1} [[u Dj1u] _] := cycTIiso_aut_exists ctiWM co_k_j1. - rewrite dprod_IirrEr -rmorphX -Dj /= -!dprod_IirrEr -!/(w_ _ _) in Dj1u. - rewrite truncCK ?Cnat_irr1 //. - have: delta_ j *: mu2_ 0 j == cfAut u (delta_ #1 *: mu2_ 0 #1). - by rewrite -!(cycTIiso_prTIirr pddM) -/ctiWM -Dj1u. - rewrite raddfZsign /= -prTIirr_aut eq_scaled_irr signr_eq0 /= /mu2_. - by case/andP=> /eqP-> /eqP->; rewrite prTIirr_aut cfunE aut_Cnat ?Cnat_irr1. -have d_gt1: (d > 1)%N. - rewrite ltn_neqAle andbC -eqC_nat -ltC_nat truncCK ?Cnat_irr1 //. - rewrite irr1_gt0 /= eq_sym; apply: contraNneq nz_j1 => mu2_lin. - have: mu2_ 0 #1 \is a linear_char by rewrite qualifE irr_char /= mu2_lin. - by rewrite lin_irr_der1 => /(prTIirr0P ptiWM)[i /irr_inj/prTIirr_inj[_ ->]]. -split=> // [i j /invj[<- _] | _ /invj[//] | ]; first by rewrite prTIirr_1. -have: (d%:R == delta %[mod w1])%C by rewrite truncCK ?Cnat_irr1 ?prTIirr1_mod. -rewrite /eqCmod unfold_in -/n (negPf (neq0CG W1)) CnatEint => ->. -rewrite divr_ge0 ?ler0n // [delta]signrE opprB addrA -natrD subr_ge0 ler1n. -by rewrite -(subnKC d_gt1). -Qed. - -Let o_mu2_irr zeta i j : - zeta \in calS -> zeta \in irr M -> '[mu2_ i j, zeta] = 0. -Proof. -case/seqIndP=> s _ -> irr_sM; rewrite -cfdot_Res_l cfRes_prTIirr cfdot_irr. -rewrite (negPf (contraNneq _ (prTIred_not_irr ptiWM j))) // => Ds. -by rewrite -cfInd_prTIres Ds. -Qed. - -Let ZmuBzeta zeta j : - zeta \in calS -> zeta 1%g = w1%:R -> j != 0 -> - mu_ j - d%:R *: zeta \in 'Z[calS, M'^#]. -Proof. -move=> Szeta zeta1w1 nz_j; have [mu1 _ _ _] := FTtype345_constants. -rewrite -[d%:R](mulKf (neq0CiG M M')) mulrC -(mu1 0 j nz_j). -rewrite -(cfResE _ sM'M) // cfRes_prTIirr -cfInd1 // cfInd_prTIres. -by rewrite (seqInd_sub_lin_vchar _ Szeta) ?calSmu // -(index_sdprod defM). -Qed. - -Let mu0Bzeta_on zeta : - zeta \in calS -> zeta 1%g = w1%:R -> mu_ 0 - zeta \in 'CF(M, 'A(M)). -Proof. -move/seqInd_on=> M'zeta zeta1w1; rewrite [mu_ 0]prTIred0 defA cfun_onD1. -rewrite !cfunE zeta1w1 cfuniE // group1 mulr1 subrr rpredB ?M'zeta //=. -by rewrite rpredZ ?cfuni_on. -Qed. - -(* We need to prove (10.5) - (10.7) for an arbitrary choice of zeta, to allow *) -(* part of the proof of (10.5) to be reused in that of (11.8). *) -Variable zeta : 'CF(M). -Hypotheses (irr_zeta : zeta \in irr M) (Szeta : zeta \in calS). -Hypothesis (zeta1w1 : zeta 1%g = w1%:R). - -Let o_mu2_zeta i j : '[mu2_ i j, zeta] = 0. Proof. exact: o_mu2_irr. Qed. - -Let o_mu_zeta j : '[mu_ j, zeta] = 0. -Proof. by rewrite cfdot_suml big1 // => i _; apply: o_mu2_zeta. Qed. - -Definition FTtype345_bridge i j := mu2_ i j - delta *: mu2_ i 0 - n *: zeta. -Local Notation alpha_ := FTtype345_bridge. - -(* This is the first part of Peterfalvi (10.5), which does not depend on the *) -(* coherence assumption that will ultimately be refuted by (10.8). *) -Lemma supp_FTtype345_bridge i j : j != 0 -> alpha_ i j \in 'CF(M, 'A0(M)). -Proof. -move=> nz_j; have [Dd Ddelta _ _] := FTtype345_constants. -have Dmu2 := prTIirr_id pddM. -have W1a0 x: x \in W1 -> alpha_ i j x = 0. - move=> W1x; rewrite !cfunE; have [-> | ntx] := eqVneq x 1%g. - by rewrite Dd // prTIirr0_1 mulr1 zeta1w1 divfK ?neq0CG ?subrr. - have notM'x: x \notin M'. - apply: contra ntx => M'x; have: x \in M' :&: W1 by apply/setIP. - by rewrite coprime_TIg ?inE. - have /sdprod_context[_ sW1W _ _ tiW21] := dprodWsdC defW. - have abW2: abelian W2 := cyclic_abelian cycW2. - have Wx: x \in W :\: W2. - rewrite inE (contra _ ntx) ?(subsetP sW1W) // => W2x. - by rewrite -in_set1 -set1gE -tiW21 inE W2x. - rewrite !Dmu2 {Wx}// Ddelta // prTIsign0 scale1r !dprod_IirrE cfunE. - rewrite -!(cfResE _ sW1W) ?cfDprodKl_abelian // subrr. - have [s _ ->] := seqIndP Szeta. - by rewrite (cfun_on0 (cfInd_normal _ _)) ?mulr0 ?subrr. -apply/cfun_onP=> x; rewrite !inE defA notMtype1 /= => /norP[notM'x]. -set pi := \pi(M'); have [Mx /= pi_x | /cfun0->//] := boolP (x \in M). -have hallM': pi.-Hall(M) M' by rewrite Hall_pi -?(coprime_sdprod_Hall_l defM). -have hallW1: pi^'.-Hall(M) W1 by rewrite -(compl_pHall _ hallM') sdprod_compl. -have{pi_x} pi'x: pi^'.-elt x. - apply: contraR notM'x => not_pi'x; rewrite !inE (mem_normal_Hall hallM') //. - rewrite not_pi'x andbT negbK in pi_x. - by rewrite (contraNneq _ not_pi'x) // => ->; apply: p_elt1. -have [|y My] := Hall_subJ (mmax_sol maxM) hallW1 _ pi'x; rewrite cycle_subG //. -by case/imsetP=> z Wz ->; rewrite cfunJ ?W1a0. -Qed. -Local Notation alpha_on := supp_FTtype345_bridge. - -Lemma vchar_FTtype345_bridge i j : alpha_ i j \in 'Z[irr M]. -Proof. -have [_ _ _ Nn] := FTtype345_constants. -by rewrite !rpredB ?rpredZsign ?rpredZ_Cnat ?irr_vchar ?mem_zchar. -Qed. -Local Notation Zalpha := vchar_FTtype345_bridge. -Local Hint Resolve Zalpha. - -Lemma vchar_Dade_FTtype345_bridge i j : - j != 0 -> (alpha_ i j)^\tau \in 'Z[irr G]. -Proof. by move=> nz_j; rewrite Dade_vchar // zchar_split Zalpha alpha_on. Qed. -Local Notation Zalpha_tau := vchar_Dade_FTtype345_bridge. - -(* This covers the last paragraph in the proof of (10.5); it's isolated here *) -(* because it is reused in the proof of (10.10) and (11.8). *) - -Lemma norm_FTtype345_bridge i j : - j != 0 -> '[(alpha_ i j)^\tau] = 2%:R + n ^+ 2. -Proof. -move=> nz_j; rewrite Dade_isometry ?alpha_on // cfnormBd ?cfnormZ; last first. - by rewrite cfdotZr cfdotBl cfdotZl !o_mu2_zeta !(mulr0, subr0). -have [_ _ _ /Cnat_ge0 n_ge0] := FTtype345_constants. -rewrite ger0_norm // cfnormBd ?cfnorm_sign ?cfnorm_irr ?irrWnorm ?mulr1 //. -by rewrite cfdotZr (cfdot_prTIirr pddM) (negPf nz_j) andbF ?mulr0. -Qed. -Local Notation norm_alpha := norm_FTtype345_bridge. - -Implicit Type tau : {additive 'CF(M) -> 'CF(G)}. - -(* This exported version is adapted to its use in (11.8). *) -Lemma FTtype345_bridge_coherence calS1 tau1 i j X Y : - coherent_with calS1 M^# tau tau1 -> (alpha_ i j)^\tau = X + Y -> - cfConjC_subset calS1 calS0 -> {subset calS1 <= irr M} -> - j != 0 -> Y \in 'Z[map tau1 calS1] -> '[Y, X] = 0 -> '[Y] = n ^+ 2 -> - X = delta *: (eta_ i j - eta_ i 0). -Proof. -move=> cohS1 Dalpha sS10 irrS1 nz_j S1_Y oYX nY_n2. -have [[_ Ddelta _ Nn] [[Itau1 Ztau1] _]] := (FTtype345_constants, cohS1). -have [|z Zz defY] := zchar_expansion _ S1_Y. - rewrite map_inj_in_uniq; first by case: sS10. - by apply: sub_in2 (Zisometry_inj Itau1); apply: mem_zchar. -have nX_2: '[X] = 2%:R. - apply: (addrI '[Y]); rewrite -cfnormDd // addrC -Dalpha norm_alpha //. - by rewrite addrC nY_n2. -have Z_X: X \in 'Z[irr G]. - rewrite -[X](addrK Y) -Dalpha rpredB ?Zalpha_tau // defY big_map big_seq. - by apply: rpred_sum => psi S1psi; rewrite rpredZ_Cint // Ztau1 ?mem_zchar. -apply: eq_signed_sub_cTIiso => // y Vy; rewrite -[X](addrK Y) -Dalpha -/delta. -rewrite !cfunE !cycTIiso_restrict //; set rhs := delta * _. -rewrite Dade_id ?defA0 //; last by rewrite setUC inE mem_class_support. -have notM'y: y \notin M'. - by have:= subsetP (prDade_supp_disjoint pddM) y Vy; rewrite inE. -have Wy: y \in W :\: W2 by move: Vy; rewrite !inE => /andP[/norP[_ ->]]. -rewrite !cfunE 2?{1}prTIirr_id // prTIsign0 scale1r Ddelta // cfunE -mulrBr. -rewrite -/rhs (cfun_on0 (seqInd_on _ Szeta)) // mulr0 subr0. -rewrite (ortho_cycTIiso_vanish ctiWG) ?subr0 // -/sigma. -apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i1 [j1 ->]] ->]. -rewrite defY cfdot_suml big_map big1_seq //= => psi S1psi. -by rewrite cfdotZl (coherent_ortho_cycTIiso MtypeP sS10) ?irrS1 ?mulr0. -Qed. - -(* This is a specialization of the above, used in (10.5) and (10.10). *) -Let def_tau_alpha calS1 tau1 i j : - coherent_with calS1 M^# tau tau1 -> cfConjC_subset calS1 calS0 -> - j != 0 -> zeta \in calS1 -> '[(alpha_ i j)^\tau, tau1 zeta] = - n -> - (alpha_ i j)^\tau = delta *: (eta_ i j - eta_ i 0) - n *: tau1 zeta. -Proof. -move=> cohS1 [_ sS10 ccS1] nz_j S1zeta alpha_zeta_n. -have [[_ _ _ Nn] [[Itau1 _] _]] := (FTtype345_constants, cohS1). -set Y := - (n *: _); apply: canRL (addrK _) _; set X := _ + _. -have Dalpha: (alpha_ i j)^\tau = X + Y by rewrite addrK. -have nY_n2: '[Y] = n ^+ 2. - by rewrite cfnormN cfnormZ norm_Cnat // Itau1 ?mem_zchar // irrWnorm ?mulr1. -pose S2 := zeta :: zeta^*%CF; pose S2tau1 := map tau1 S2. -have S2_Y: Y \in 'Z[S2tau1] by rewrite rpredN rpredZ_Cnat ?mem_zchar ?mem_head. -have sS21: {subset S2 <= calS1} by apply/allP; rewrite /= ccS1 ?S1zeta. -have cohS2 : coherent_with S2 M^# tau tau1 := subset_coherent_with sS21 cohS1. -have irrS2: {subset S2 <= irr M} by apply/allP; rewrite /= cfAut_irr irr_zeta. -rewrite (FTtype345_bridge_coherence cohS2 Dalpha) //; last first. - rewrite -[X]opprK cfdotNr opprD cfdotDr nY_n2 cfdotNl cfdotNr opprK cfdotZl. - by rewrite cfdotC alpha_zeta_n rmorphN conj_Cnat // mulrN addNr oppr0. -split=> [|_ /sS21/sS10//|]; last first. - by apply/allP; rewrite /= !inE cfConjCK !eqxx orbT. -by rewrite /= inE eq_sym; have [[_ /hasPn-> //]] := scohS0; apply: sS10. -Qed. - -Section NonCoherence. - -(* We will ultimately contradict these assumptions. *) -(* Note that we do not need to export any lemma save the final contradiction. *) -Variable tau1 : {additive 'CF(M) -> 'CF(G)}. -Hypothesis cohS : coherent_with calS M^# tau tau1. - -Local Notation "mu ^\tau1" := (tau1 mu%CF) - (at level 2, format "mu ^\tau1") : ring_scope. - -Let Dtau1 : {in 'Z[calS, M'^#], tau1 =1 tau}. -Proof. by case: cohS => _; apply: sub_in1; apply: zchar_onS; apply: setSD. Qed. - -Let o_zeta_s: '[zeta, zeta^*] = 0. -Proof. by rewrite (seqInd_conjC_ortho _ _ _ Szeta) ?mFT_odd /= ?defMs. Qed. - -Import ssrint rat. - -(* This is the second part of Peterfalvi (10.5). *) -Let tau_alpha i j : j != 0 -> - (alpha_ i j)^\tau = delta *: (eta_ i j - eta_ i 0) - n *: zeta^\tau1. -Proof. -move=> nz_j; set al_ij := alpha_ i j; have [[Itau1 Ztau1] _] := cohS. -have [mu1 Ddelta d_gt1 Nn] := FTtype345_constants. -pose a := '[al_ij^\tau, zeta^\tau1] + n. -have al_ij_zeta_s: '[al_ij^\tau, zeta^*^\tau1] = a. - apply: canRL (addNKr _) _; rewrite addrC -opprB -cfdotBr -raddfB. - have M'dz: zeta - zeta^*%CF \in 'Z[calS, M'^#] by apply: seqInd_sub_aut_zchar. - rewrite Dtau1 // Dade_isometry ?alpha_on ?tauM' //. - rewrite cfdotBr opprB cfdotBl cfdot_conjCr rmorphB linearZ /=. - rewrite -!prTIirr_aut !cfdotBl !cfdotZl !o_mu2_zeta o_zeta_s !mulr0. - by rewrite opprB !(subr0, rmorph0) add0r irrWnorm ?mulr1. -have Zal_ij: al_ij^\tau \in 'Z[irr G] by apply: Zalpha_tau. -have Za: a \in Cint. - by rewrite rpredD ?(Cint_Cnat Nn) ?Cint_cfdot_vchar ?Ztau1 ?(mem_zchar Szeta). -have{al_ij_zeta_s} ub_da2: (d ^ 2)%:R * a ^+ 2 <= (2%:R + n ^+ 2) * w1%:R. - have [k nz_k j'k]: exists2 k, k != 0 & k != j. - have:= w2gt2; rewrite -nirrW2 (cardD1 0) (cardD1 j) !inE nz_j !ltnS lt0n. - by case/pred0Pn=> k /and3P[]; exists k. - have muk_1: mu_ k 1%g = (d * w1)%:R. - by rewrite (prTIred_1 pddM) mu1 // mulrC -natrM. - rewrite natrX -exprMn; have <-: '[al_ij^\tau, (mu_ k)^\tau1] = d%:R * a. - rewrite mulrDr mulr_natl -raddfMn /=; apply: canRL (addNKr _) _. - rewrite addrC -cfdotBr -raddfMn -raddfB -scaler_nat. - rewrite Dtau1 ?Dade_isometry ?alpha_on ?tauM' ?ZmuBzeta // cfdotBr cfdotZr. - rewrite rmorph_nat !cfdotBl !cfdotZl !o_mu2_zeta irrWnorm //. - rewrite !(cfdot_prTIirr_red pddM) cfdotC o_mu_zeta conjC0 !mulr0 mulr1. - by rewrite 2 1?eq_sym // mulr0 -mulrN opprB !subr0 add0r. - have ZSmuk: mu_ k \in 'Z[calS] by rewrite mem_zchar ?calSmu. - have <-: '[al_ij^\tau] * '[(mu_ k)^\tau1] = (2%:R + n ^+ 2) * w1%:R. - by rewrite Itau1 // cfdot_prTIred eqxx mul1n norm_alpha. - by rewrite -Cint_normK ?cfCauchySchwarz // Cint_cfdot_vchar // Ztau1. -suffices a0 : a = 0. - by apply: (def_tau_alpha _ sSS0); rewrite // -sub0r -a0 addrK. -apply: contraTeq (d_gt1) => /(sqr_Cint_ge1 Za) a2_ge1. -suffices: n == 0. - rewrite mulf_eq0 invr_eq0 orbC -implyNb neq0CG /= subr_eq0 => /eqP Dd. - by rewrite -ltC_nat -(normr_nat _ d) Dd normr_sign ltrr. -suffices: n ^+ 2 < n + 1. - have d_dv_M: (d%:R %| #|M|)%C by rewrite -(mu1 0 j) // ?dvd_irr1_cardG. - have{d_dv_M} d_odd: odd d by apply: dvdn_odd (mFT_odd M); rewrite -dvdC_nat. - have: (2 %| n * w1%:R)%C. - rewrite divfK ?neq0CG // -signrN signrE addrA -(natrD _ d 1). - by rewrite rpredB // dvdC_nat dvdn2 ?odd_double // odd_add d_odd. - rewrite -(truncCK Nn) -mulrSr -natrM -natrX ltC_nat (dvdC_nat 2) pnatr_eq0. - rewrite dvdn2 odd_mul mFT_odd; case: (truncC n) => [|[|n1]] // _ /idPn[]. - by rewrite -leqNgt (ltn_exp2l 1). -apply: ltr_le_trans (_ : n * - delta + 1 <= _); last first. - have ->: n + 1 = n * `|- delta| + 1 by rewrite normrN normr_sign mulr1. - rewrite ler_add2r ler_wpmul2l ?Cnat_ge0 ?real_ler_norm //. - by rewrite rpredN ?rpred_sign. -rewrite -(ltr_pmul2r (ltC_nat 0 2)) mulrDl mul1r -[rhs in rhs + _]mulrA. -apply: ler_lt_trans (_ : n ^+ 2 * (w1%:R - 1) < _). - rewrite -(subnKC w1gt2) -(@natrB _ _ 1) // ler_wpmul2l ?leC_nat //. - by rewrite Cnat_ge0 ?rpredX. -rewrite -(ltr_pmul2l (gt0CG W1)) -/w1 2!mulrBr mulr1 mulrCA -exprMn. -rewrite mulrDr ltr_subl_addl addrCA -mulrDr mulrCA mulrA -ltr_subl_addl. -rewrite -mulrBr mulNr opprK divfK ?neq0CG // mulr_natr addrA subrK -subr_sqr. -rewrite sqrr_sign mulrC [_ + 2%:R]addrC (ltr_le_trans _ ub_da2) //. -apply: ltr_le_trans (ler_wpmul2l (ler0n _ _) a2_ge1). -by rewrite mulr1 ltr_subl_addl -mulrS -natrX ltC_nat. -Qed. - -(* This is the first part of Peterfalvi (10.6)(a). *) -Let tau1mu j : j != 0 -> (mu_ j)^\tau1 = delta *: \sum_i eta_ i j. -Proof. -move=> nz_j; have [[[Itau1 _] _] Smu_j] := (cohS, calSmu nz_j). -have eta_mu i: '[delta *: (eta_ i j - eta_ i 0), (mu_ j)^\tau1] = 1. - have Szeta_s: zeta^*%CF \in calS by rewrite cfAut_seqInd. - have o_zeta_s_w k: '[eta_ i k, d%:R *: zeta^*^\tau1] = 0. - have o_S_eta_ := coherent_ortho_cycTIiso MtypeP sSS0 cohS. - by rewrite cfdotZr cfdotC o_S_eta_ ?conjC0 ?mulr0 // cfAut_irr. - pose psi := mu_ j - d%:R *: zeta^*%CF; rewrite (canRL (subrK _) (erefl psi)). - rewrite (raddfD tau1) raddfZnat cfdotDr addrC cfdotZl cfdotBl !{}o_zeta_s_w. - rewrite subr0 mulr0 add0r -(canLR (subrK _) (tau_alpha i nz_j)). - have Zpsi: psi \in 'Z[calS, M'^#]. - by rewrite ZmuBzeta // cfunE zeta1w1 rmorph_nat. - rewrite cfdotDl cfdotZl Itau1 ?(zcharW Zpsi) ?mem_zchar // -cfdotZl Dtau1 //. - rewrite Dade_isometry ?alpha_on ?tauM' {Zpsi}// -cfdotDl cfdotBr cfdotZr. - rewrite subrK !cfdotBl !cfdotZl !cfdot_prTIirr_red eq_sym (negPf nz_j). - by rewrite !o_mu2_irr ?cfAut_irr // !(mulr0, subr0) eqxx. -have [_ Ddel _ _] := FTtype345_constants. -have [[d1 k] Dtau1mu] := FTtypeP_coherent_TIred sSS0 cohS irr_zeta Szeta Smu_j. -case=> [[Dd1 Dk] | [_ Dk _]]; first by rewrite Dtau1mu Dd1 Dk [_ ^+ _]Ddel. -have /esym/eqP/idPn[] := eta_mu 0; rewrite Dtau1mu Dk /= cfdotZl cfdotZr. -rewrite cfdot_sumr big1 ?mulr0 ?oner_eq0 // => i _; rewrite -/sigma -/(w_ i _). -rewrite cfdotBl !(cfdot_cycTIiso pddM) !(eq_sym 0) conjC_Iirr_eq0 -!irr_eq1. -rewrite (eq_sym j) -(inj_eq irr_inj) conjC_IirrE. -by rewrite odd_eq_conj_irr1 ?mFT_odd ?subrr. -Qed. - -(* This is the second part of Peterfalvi (10.6)(a). *) -Let tau1mu0 : (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - zeta^\tau1. -Proof. -have [j nz_j] := has_nonprincipal_irr ntW2. -have sum_al: \sum_i alpha_ i j = mu_ j - d%:R *: zeta - delta *: (mu_ 0 - zeta). - rewrite scalerBr opprD addrACA scaler_sumr !sumrB sumr_const; congr (_ + _). - by rewrite -opprD -scalerBl nirrW1 -scaler_nat scalerA mulrC divfK ?neq0CG. -have ->: mu_ 0 - zeta = delta *: (mu_ j - d%:R *: zeta - \sum_i alpha_ i j). - by rewrite sum_al opprD addNKr opprK signrZK. -rewrite linearZ linearB; apply: canLR (signrZK _) _; rewrite -/delta /=. -rewrite linear_sum -Dtau1 ?ZmuBzeta //= raddfB raddfZnat addrAC scalerBr. -rewrite (eq_bigr _ (fun i _ => tau_alpha i nz_j)) sumrB sumr_const nirrW1 opprD. -rewrite -scaler_sumr sumrB scalerBr -tau1mu // opprD !opprK -!addrA addNKr. -congr (_ + _); rewrite -scaler_nat scalerA mulrC divfK ?neq0CG //. -by rewrite addrC -!scaleNr -scalerDl addKr. -Qed. - -(* This is Peterfalvi (10.6)(b). *) -Let zeta_tau1_coprime g : - g \notin 'A~(M) -> coprime #[g] w1 -> `|zeta^\tau1 g| >= 1. -Proof. -move=> notAg co_g_w1; have Amu0zeta := mu0Bzeta_on Szeta zeta1w1. -have mu0_zeta_g: (mu_ 0 - zeta)^\tau g = 0. - have [ | ] := boolP (g \in 'A0~(M)); rewrite -FT_Dade0_supportE; last first. - by apply: cfun_on0; apply: Dade_cfunS. - case/bigcupP=> x A0x xRg; rewrite (DadeE _ A0x) // (cfun_on0 Amu0zeta) //. - apply: contra notAg => Ax; apply/bigcupP; exists x => //. - by rewrite -def_FTsignalizer0. -have{mu0_zeta_g} zeta_g: zeta^\tau1 g = \sum_i eta_ i 0 g. - by apply/esym/eqP; rewrite -subr_eq0 -{2}mu0_zeta_g tau1mu0 !cfunE sum_cfunE. -have Zwg i: eta_ i 0 g \in Cint. - have Lchi: 'chi_i \is a linear_char by apply: irr_cyclic_lin. - rewrite Cint_cycTIiso_coprime // dprod_IirrE irr0 cfDprod_cfun1r. - rewrite (coprime_dvdr _ co_g_w1) // dvdn_cforder. - rewrite -rmorphX cfDprodl_eq1 -dvdn_cforder; apply/dvdn_cforderP=> x W1x. - by rewrite -lin_charX // -expg_mod_order (eqnP (order_dvdG W1x)) lin_char1. -have odd_zeta_g: (zeta^\tau1 g == 1 %[mod 2])%C. - rewrite zeta_g (bigD1 0) //= [w_ 0 0]cycTIirr00 cycTIiso1 cfun1E inE. - pose eW1 := [pred i : Iirr W1 | conjC_Iirr i < i]%N. - rewrite (bigID eW1) (reindex_inj (can_inj (@conjC_IirrK _ _))) /=. - set s1 := \sum_(i | _) _; set s2 := \sum_(i | _) _; suffices ->: s1 = s2. - by rewrite -mulr2n addrC -(mulr_natr _ 2) eqCmod_addl_mul ?rpred_sum. - apply/eq_big=> [i | i _]. - rewrite (canF_eq (@conjC_IirrK _ _)) conjC_Iirr0 conjC_IirrK -leqNgt. - rewrite ltn_neqAle val_eqE -irr_eq1 (eq_sym i) -(inj_eq irr_inj) andbA. - by rewrite aut_IirrE odd_eq_conj_irr1 ?mFT_odd ?andbb. - rewrite -{1}conjC_Iirr0 [w_ _ _]cycTIirr_aut -cfAut_cycTIiso. - by rewrite cfunE conj_Cint ?Zwg. -rewrite norm_Cint_ge1 //; first by rewrite zeta_g rpred_sum. -apply: contraTneq odd_zeta_g => ->. -by rewrite eqCmod_sym /eqCmod subr0 /= (dvdC_nat 2 1). -Qed. - -(* This is Peterfalvi (10.7). *) -Let Frob_der1_type2 S : - S \in 'M -> FTtype S == 2 -> [Frobenius S^`(1) with kernel S`_\F]. -Proof. -move: S => L maxL /eqP Ltype2. -have [S pairMS [xdefW [U StypeP]]] := FTtypeP_pair_witness maxM MtypeP. -have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _. -move/(_ L maxL)/implyP; rewrite Ltype2 /= => /setUP[] /imsetP[x0 _ defL]. - by case/eqP/idPn: Ltype2; rewrite defL FTtypeJ. -pose H := (S`_\F)%G; pose HU := (S^`(1))%G. -suffices{L Ltype2 maxL x0 defL}: [Frobenius HU = H ><| U]. - by rewrite defL derJ FcoreJ FrobeniusJker; apply: FrobeniusWker. -have sHHU: H \subset HU by have [_ [_ _ _ /sdprodW/mulG_sub[]]] := StypeP. -pose calT := seqIndD HU S H 1; pose tauS := FT_Dade0 maxS. -have DcalTs: calT = seqIndD HU S S`_\s 1. - by congr (seqIndD _ _ _ _); apply: val_inj; rewrite /= FTcore_type2. -have notFrobM: ~~ [Frobenius M with kernel M`_\F]. - by apply/existsP=> [[U1 /Frobenius_of_typeF/(typePF_exclusion MtypeP)]]. -have{notFrobM} notSsupportM: ~~ [exists x, FTsupports M (S :^ x)]. - apply: contra notFrobM => /'exists_existsP[x [y /and3P[Ay not_sCyM sCySx]]]. - have [_ [_ /(_ y)uMS] /(_ y)] := FTsupport_facts maxM. - rewrite inE (subsetP (FTsupp_sub0 _)) //= in uMS *. - rewrite -(eq_uniq_mmax (uMS not_sCyM) _ sCySx) ?mmaxJ // FTtypeJ. - by case=> // _ _ _ [_ ->]. -have{notSsupportM} tiA1M_AS: [disjoint 'A1~(M) & 'A~(S)]. - have notMG_S: gval S \notin M :^: G. - by apply: contraL Stype2 => /imsetP[x _ ->]; rewrite FTtypeJ. - by apply: negbNE; have [_ <- _] := FT_Dade_support_disjoint maxM maxS notMG_S. -pose pddS := FT_prDade_hypF maxS StypeP; pose nu := primeTIred pddS. -have{tiA1M_AS} oST phi psi: - phi \in 'Z[calS, M^#] -> psi \in 'Z[calT, S^#] -> '[phi^\tau, tauS psi] = 0. -- rewrite zcharD1_seqInd // -[seqInd _ _]/calS => Sphi. - rewrite zcharD1E => /andP[Tpsi psi1_0]. - rewrite -FT_Dade1E ?defA1 ?(zchar_on Sphi) //. - apply: cfdot_complement (Dade_cfunS _ _) _; rewrite FT_Dade1_supportE setTD. - rewrite -[tauS _]FT_DadeE ?(cfun_onS _ (Dade_cfunS _ _)) ?FT_Dade_supportE //. - by rewrite -disjoints_subset disjoint_sym. - have /subsetD1P[_ /setU1K <-] := FTsupp_sub S; rewrite cfun_onD1 {}psi1_0. - rewrite -Tpsi andbC -zchar_split {psi Tpsi}(zchar_trans_on _ Tpsi) //. - move=> psi Tpsi; rewrite zchar_split mem_zchar //=. - have [s /setDP[_ kerH's] ->] := seqIndP Tpsi. - by rewrite inE in kerH's; rewrite (prDade_Ind_irr_on pddS). -have notStype5: FTtype S != 5 by rewrite (eqP Stype2). -have [|[_ _ _ _ -> //]] := typeP_reducible_core_cases maxS StypeP notStype5. -case=> t []; set lambda := 'chi_t => T0C'lam lam_1 _. -have{T0C'lam} Tlam: lambda \in calT. - by apply: seqIndS T0C'lam; rewrite Iirr_kerDS ?sub1G. -have{lam_1} [r [nz_r Tnu_r nu_r_1]]: - exists r, [/\ r != 0, nu r \in calT & nu r 1%g = lambda 1%g]. -- have [_] := typeP_reducible_core_Ind maxS StypeP notStype5. - set H0 := Ptype_Fcore_kernel _; set nuT := filter _ _; rewrite -/nu. - case/hasP=> nu_r nuTr _ /(_ _ nuTr)/imageP[r nz_r Dr] /(_ _ nuTr)[nu_r1 _ _]. - have{nuTr} Tnu_r := mem_subseq (filter_subseq _ _) nuTr. - by exists r; rewrite -Dr nu_r1 (seqIndS _ Tnu_r) // Iirr_kerDS ?sub1G. -pose T2 := [:: lambda; lambda^*; nu r; (nu r)^*]%CF. -have [rmRS scohT]: exists rmRS, subcoherent calT tauS rmRS. - move: (FTtypeP_coh_base _ _) (FTtypeP_subcoherent maxS StypeP) => RS scohT. - by rewrite DcalTs; exists RS. -have [lam_irr nu_red]: lambda \in irr S /\ nu r \notin irr S. - by rewrite mem_irr prTIred_not_irr. -have [lam'nu lams'nu]: lambda != nu r /\ lambda^*%CF != nu r. - by rewrite -conjC_IirrE !(contraNneq _ nu_red) // => <-; apply: mem_irr. -have [[_ nRT ccT] _ _ _ _] := scohT. -have{ccT} sT2T: {subset T2 <= calT} by apply/allP; rewrite /= ?Tlam ?Tnu_r ?ccT. -have{nRT} uccT2: cfConjC_subset T2 calT. - split; last 1 [by [] | by apply/allP; rewrite /= !inE !cfConjCK !eqxx !orbT]. - rewrite /uniq /T2 !inE !negb_or -!(inv_eq (@cfConjCK _ S)) !cfConjCK. - by rewrite lam'nu lams'nu !(hasPn nRT). -have scohT2 := subset_subcoherent scohT uccT2. -have [tau2 cohT2]: coherent T2 S^# tauS. - apply: (uniform_degree_coherence scohT2); rewrite /= !cfunE nu_r_1 eqxx. - by rewrite conj_Cnat ?Cnat_irr1 ?eqxx. -have [s nz_s] := has_nonprincipal_irr ntW2; have Smu_s := calSmu nz_s. -pose alpha := mu_ s - d%:R *: zeta; pose beta := nu r - lambda. -have Salpha: alpha \in 'Z[calS, M^#] by rewrite zcharD1_seqInd ?ZmuBzeta. -have [T2lam T2nu_r]: lambda \in T2 /\ nu r \in T2 by rewrite !inE !eqxx !orbT. -have Tbeta: beta \in 'Z[T2, S^#]. - by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE nu_r_1 subrr. -have /eqP/idPn[] := oST _ _ Salpha (zchar_subset sT2T Tbeta). -have [[_ <- //] [_ <- //]] := (cohS, cohT2). -rewrite !raddfB raddfZnat /= subr_eq0 !cfdotBl !cfdotZl. -have [|[dr r'] -> _] := FTtypeP_coherent_TIred _ cohT2 lam_irr T2lam T2nu_r. - by rewrite -DcalTs. -set sigS := cyclicTIiso _ => /=. -have etaC i j: sigS (cyclicTIirr xdefW j i) = eta_ i j by apply: cycTIisoC. -rewrite !cfdotZr addrC cfdot_sumr big1 => [|j _]; last first. - by rewrite etaC (coherent_ortho_cycTIiso _ sSS0) ?mem_irr. -rewrite !mulr0 oppr0 add0r rmorph_sign. -have ->: '[zeta^\tau1, tau2 lambda] = 0. - pose X1 := (zeta :: zeta^*)%CF; pose X2 := (lambda :: lambda^*)%CF. - pose Y1 := map tau1 X1; pose Y2 := map tau2 X2; have [_ _ ccS] := sSS0. - have [sX1S sX2T]: {subset X1 <= calS} /\ {subset X2 <= T2}. - by split; apply/allP; rewrite /= ?inE ?eqxx ?orbT // Szeta ccS. - have [/(sub_iso_to (zchar_subset sX1S) sub_refl)[Itau1 Ztau1] Dtau1L] := cohS. - have [/(sub_iso_to (zchar_subset sX2T) sub_refl)[Itau2 Ztau2] Dtau2] := cohT2. - have Z_Y12: {subset Y1 <= 'Z[irr G]} /\ {subset Y2 <= 'Z[irr G]}. - by rewrite /Y1 /Y2; split=> ? /mapP[xi /mem_zchar] => [/Ztau1|/Ztau2] ? ->. - have o1Y12: orthonormal Y1 && orthonormal Y2. - rewrite !map_orthonormal //. - by apply: seqInd_conjC_ortho2 Tlam; rewrite ?gFnormal ?mFT_odd. - by apply: seqInd_conjC_ortho2 Szeta; rewrite ?gFnormal ?mFT_odd ?mem_irr. - apply: orthonormal_vchar_diff_ortho Z_Y12 o1Y12 _; rewrite -2!raddfB. - have SzetaBs: zeta - zeta^*%CF \in 'Z[calS, M^#]. - by rewrite zcharD1_seqInd // seqInd_sub_aut_zchar. - have T2lamBs: lambda - lambda^*%CF \in 'Z[T2, S^#]. - rewrite sub_aut_zchar ?zchar_onG ?mem_zchar ?inE ?eqxx ?orbT //. - by move=> xi /sT2T/seqInd_vcharW. - by rewrite Dtau1L // Dtau2 // !Dade1 oST ?(zchar_subset sT2T) ?eqxx. -have [[ds s'] /= -> _] := FTtypeP_coherent_TIred sSS0 cohS irr_zeta Szeta Smu_s. -rewrite mulr0 subr0 !cfdotZl mulrA -signr_addb !cfdot_suml. -rewrite (bigD1 r') //= cfdot_sumr (bigD1 s') //=. -rewrite etaC cfdot_cycTIiso !eqxx big1 => [|j ne_s'_j]; last first. - by rewrite etaC cfdot_cycTIiso andbC eq_sym (negPf ne_s'_j). -rewrite big1 => [|i ne_i_r']; last first. - rewrite cfdot_sumr big1 // => j _. - by rewrite etaC cfdot_cycTIiso (negPf ne_i_r'). -rewrite !addr0 mulr1 big1 ?mulr0 ?signr_eq0 // => i _. -by rewrite -etaC cfdotC (coherent_ortho_cycTIiso _ _ cohT2) ?conjC0 -?DcalTs. -Qed. - -(* This is the bulk of the proof of Peterfalvi (10.8); however the result *) -(* will be restated below to avoid the quantification on zeta and tau1. *) -Lemma FTtype345_noncoherence_main : False. -Proof. -have [S pairMS [xdefW [U StypeP]]] := FTtypeP_pair_witness maxM MtypeP. -have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _ _. -pose H := (S`_\F)%G; pose HU := (S^`(1))%G. -have [[_ hallW2 _ defS] [_ _ nUW2 defHU] _ [_ _ sW1H _ _] _] := StypeP. -have ntU: U :!=: 1%g by have [[]] := compl_of_typeII maxS StypeP Stype2. -pose G01 := [set g : gT | coprime #[g] w1]. -pose G0 := ~: 'A~(M) :&: G01; pose G1 := ~: 'A~(M) :\: G01. -pose chi := zeta^\tau1; pose ddAM := FT_Dade_hyp maxM; pose rho := invDade ddAM. -have Suzuki: - #|G|%:R^-1 * (\sum_(g in ~: 'A~(M)) `|chi g| ^+ 2 - #|~: 'A~(M)|%:R) - + '[rho chi] - #|'A(M)|%:R / #|M|%:R <= 0. -- pose A_ (_ : 'I_1) := ddAM; pose Atau i := Dade_support (A_ i). - have tiA i j : i != j -> [disjoint Atau i & Atau j] by rewrite !ord1. - have Nchi1: '[chi] = 1 by have [[->]] := cohS; rewrite ?mem_zchar ?irrWnorm. - have:= Dade_cover_inequality tiA Nchi1; rewrite /= !big_ord1 -/rho -addrA. - by congr (_ * _ + _ <= 0); rewrite FT_Dade_supportE setTD. -have{Suzuki} ub_rho: '[rho chi] <= #|'A(M)|%:R / #|M|%:R + #|G1|%:R / #|G|%:R. - rewrite addrC -subr_le0 opprD addrCA (ler_trans _ Suzuki) // -addrA. - rewrite ler_add2r -(cardsID G01 (~: _)) (big_setID G01) -/G0 -/G1 /=. - rewrite mulrC mulrBr ler_subr_addl -mulrBr natrD addrK. - rewrite ler_wpmul2l ?invr_ge0 ?ler0n // -sumr_const ler_paddr //. - by apply: sumr_ge0 => g; rewrite exprn_ge0 ?normr_ge0. - apply: ler_sum => g; rewrite !inE => /andP[notAg] /(zeta_tau1_coprime notAg). - by rewrite expr_ge1 ?normr_ge0. -have lb_M'bar: (w1 * 2 <= #|M' / M''|%g.-1)%N. - suffices ->: w1 = #|W1 / M''|%g. - rewrite muln2 -ltnS prednK ?cardG_gt0 //. - by rewrite (ltn_odd_Frobenius_ker frobMbar) ?quotient_odd ?mFT_odd. - have [_ sW1M _ _ tiM'W1] := sdprod_context defM. - apply/card_isog/quotient_isog; first exact: subset_trans (der_norm 2 M). - by apply/trivgP; rewrite -tiM'W1 setSI ?normal_sub. -have lb_rho: 1 - w1%:R / #|M'|%:R <= '[rho chi]. - have cohS_A: coherent_with calS M^# (Dade ddAM) tau1. - have [Itau1 _] := cohS; split=> // phi; rewrite zcharD1_seqInd // => Sphi. - by rewrite Dtau1 // FT_DadeE // defA (zchar_on Sphi). - rewrite {ub_rho}/rho [w1](index_sdprod defM); rewrite defA in (ddAM) cohS_A *. - have [||_ [_ _ [] //]] := Dade_Ind1_sub_lin cohS_A _ irr_zeta Szeta. - - by apply: seqInd_nontrivial Szeta; rewrite ?mem_irr ?mFT_odd. - - by rewrite -(index_sdprod defM). - rewrite -(index_sdprod defM) ler_pdivl_mulr ?ltr0n // -natrM. - rewrite -leC_nat in lb_M'bar; apply: ler_trans lb_M'bar _. - rewrite ler_subr_addl -mulrS prednK ?cardG_gt0 // leC_nat. - by rewrite dvdn_leq ?dvdn_quotient. -have{lb_rho ub_rho}: - 1 - #|G1|%:R / #|G|%:R - w1%:R^-1 < w1%:R / #|M'|%:R :> algC. -- rewrite -addrA -opprD ltr_subl_addr -ltr_subl_addl. - apply: ler_lt_trans (ler_trans lb_rho ub_rho) _; rewrite addrC ltr_add2l. - rewrite ltr_pdivr_mulr ?gt0CG // mulrC -(sdprod_card defM) natrM. - by rewrite mulfK ?neq0CG // defA ltC_nat (cardsD1 1%g M') group1. -have frobHU: [Frobenius HU with kernel H] by apply: Frob_der1_type2. -have tiH: normedTI H^# G S. - by have [_ _] := FTtypeII_ker_TI maxS Stype2; rewrite FTsupp1_type2. -have sG1_HVG: G1 \subset class_support H^# G :|: class_support V G. - apply/subsetP=> x; rewrite !inE coprime_has_primes ?cardG_gt0 // negbK. - case/andP=> /hasP[p W1p]; rewrite /= mem_primes => /and3P[p_pr _ p_dv_x] _. - have [a x_a a_p] := Cauchy p_pr p_dv_x. - have nta: a != 1%g by rewrite -order_gt1 a_p prime_gt1. - have ntx: x != 1%g by apply: contraTneq x_a => ->; rewrite /= cycle1 inE. - have cxa: a \in 'C[x] by rewrite -cent_cycle (subsetP (cycle_abelian x)). - have hallH: \pi(H).-Hall(G) H by apply: Hall_pi; have [] := FTcore_facts maxS. - have{a_p} p_a: p.-elt a by rewrite /p_elt a_p pnat_id. - have piHp: p \in \pi(H) by rewrite (piSg _ W1p). - have [y _ Hay] := Hall_pJsub hallH piHp (subsetT _) p_a. - do [rewrite -cycleJ cycle_subG; set ay := (a ^ y)%g] in Hay. - rewrite -[x](conjgK y); set xy := (x ^ y)%g. - have caxy: xy \in 'C[ay] by rewrite cent1J memJ_conjg cent1C. - have [ntxy ntay]: xy != 1%g /\ ay != 1%g by rewrite !conjg_eq1. - have Sxy: xy \in S. - have H1ay: ay \in H^# by apply/setD1P. - by rewrite (subsetP (cent1_normedTI tiH H1ay)) ?setTI. - have [HUxy | notHUxy] := boolP (xy \in HU). - rewrite memJ_class_support ?inE ?ntxy //=. - have [_ _ _ regHUH] := Frobenius_kerP frobHU. - by rewrite (subsetP (regHUH ay _)) // inE ?HUxy // inE ntay. - suffices /imset2P[xyz z Vxzy _ ->]: xy \in class_support V S. - by rewrite -conjgM orbC memJ_class_support. - rewrite /V setUC -(FTsupp0_typeP maxS StypeP) !inE Sxy. - rewrite andb_orr andNb (contra (subsetP _ _) notHUxy) /=; last first. - by apply/bigcupsP=> z _; rewrite (eqP Stype2) setDE -setIA subsetIl. - have /Hall_pi hallHU: Hall S HU by rewrite (sdprod_Hall defS). - rewrite (eqP Stype2) -(mem_normal_Hall hallHU) ?gFnormal // notHUxy. - have /mulG_sub[sHHU _] := sdprodW defHU. - rewrite (contra (fun p'xy => pi'_p'group p'xy (piSg sHHU piHp))) //. - by rewrite pgroupE p'natE // cycleJ cardJg p_dv_x. -have ub_G1: #|G1|%:R / #|G|%:R <= #|H|%:R / #|S|%:R + #|V|%:R / #|W|%:R :> algC. - rewrite ler_pdivr_mulr ?ltr0n ?cardG_gt0 // mulrC mulrDr !mulrA. - rewrite ![_ * _ / _]mulrAC -!natf_indexg ?subsetT //= -!natrM -natrD ler_nat. - apply: leq_trans (subset_leq_card sG1_HVG) _. - rewrite cardsU (leq_trans (leq_subr _ _)) //. - have unifJG B C: C \in B :^: G -> #|C| = #|B|. - by case/imsetP=> z _ ->; rewrite cardJg. - have oTI := card_uniform_partition (unifJG _) (partition_class_support _ _). - have{tiH} [ntH tiH /eqP defNH] := and3P tiH. - have [_ _ /and3P[ntV tiV /eqP defNV]] := ctiWG. - rewrite !oTI // !card_conjugates defNH defNV /= leq_add2r ?leq_mul //. - by rewrite subset_leq_card ?subsetDl. -rewrite ler_gtF // addrAC ler_subr_addl -ler_subr_addr (ler_trans ub_G1) //. -rewrite -(sdprod_card defS) -(sdprod_card defHU) addrC. -rewrite -mulnA !natrM invfM mulVKf ?natrG_neq0 // -/w1 -/w2. -have sW12_W: W1 :|: W2 \subset W by rewrite -(dprodWY defW) sub_gen. -rewrite cardsD (setIidPr sW12_W) natrB ?subset_leq_card // mulrBl. -rewrite divff ?natrG_neq0 // -!addrA ler_add2l. -rewrite cardsU -(dprod_card defW) -/w1 -/w2; have [_ _ _ ->] := dprodP defW. -rewrite cards1 natrB ?addn_gt0 ?cardG_gt0 // addnC natrD -addrA mulrDl mulrBl. -rewrite {1}mulnC !natrM !invfM !mulVKf ?natrG_neq0 // opprD -addrA ler_add2l. -rewrite mul1r -{1}[_^-1]mul1r addrC ler_oppr [- _]opprB -!mulrBl. -rewrite -addrA -opprD ler_pdivl_mulr; last by rewrite natrG_gt0. -apply: ler_trans (_ : 1 - (3%:R^-1 + 7%:R^-1) <= _); last first. - rewrite ler_add2l ler_opp2. - rewrite ler_add // lef_pinv ?qualifE ?gt0CG ?ltr0n ?ler_nat //. - have notStype5: FTtype S != 5 by rewrite (eqP Stype2). - have frobUW2 := Ptype_compl_Frobenius maxS StypeP notStype5. - apply: leq_ltn_trans (ltn_odd_Frobenius_ker frobUW2 (mFT_odd _)). - by rewrite (leq_double 3). -apply: ler_trans (_ : 2%:R^-1 <= _); last by rewrite -!CratrE; compute. -rewrite mulrAC ler_pdivr_mulr 1?gt0CG // ler_pdivl_mull ?ltr0n //. -rewrite -!natrM ler_nat mulnA -(Lagrange (normal_sub nsM''M')) mulnC leq_mul //. - by rewrite subset_leq_card //; have [_ _ _ []] := MtypeP. -by rewrite -card_quotient ?normal_norm // mulnC -(prednK (cardG_gt0 _)) leqW. -Qed. - -End NonCoherence. - -(* This is Peterfalvi (10.9). *) -Lemma FTtype345_Dade_bridge0 : - (w1 < w2)%N -> - {chi | [/\ (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - chi, - chi \in 'Z[irr G], '[chi] = 1 - & forall i j, '[chi, eta_ i j] = 0]}. -Proof. -move=> w1_lt_w2; set psi := mu_ 0 - zeta; pose Wsig := map sigma (irr W). -have [X wsigX [chi [DpsiG _ o_chiW]]] := orthogonal_split Wsig psi^\tau. -exists (- chi); rewrite opprK rpredN cfnormN. -have o_chi_w i j: '[chi, eta_ i j] = 0. - by rewrite (orthoPl o_chiW) ?map_f ?mem_irr. -have [Isigma Zsigma] := cycTI_Zisometry ctiWG. -have o1Wsig: orthonormal Wsig by rewrite map_orthonormal ?irr_orthonormal. -have [a_ Da defX] := orthonormal_span o1Wsig wsigX. -have{Da} Da i j: a_ (eta_ i j) = '[psi^\tau, eta_ i j]. - by rewrite DpsiG cfdotDl o_chi_w addr0 Da. -have sumX: X = \sum_i \sum_j a_ (eta_ i j) *: eta_ i j. - rewrite pair_bigA defX big_map (big_nth 0) size_tuple big_mkord /=. - rewrite (reindex (dprod_Iirr defW)) /=. - by apply: eq_bigr => [[i j] /= _]; rewrite -tnth_nth. - by exists (inv_dprod_Iirr defW) => ij; rewrite (inv_dprod_IirrK, dprod_IirrK). -have Zpsi: psi \in 'Z[irr M]. - by rewrite rpredB ?irr_vchar ?(mem_zchar irr_zeta) ?char_vchar ?prTIred_char. -have{Zpsi} M'psi: psi \in 'Z[irr M, M'^#]. - by rewrite -defA zchar_split Zpsi mu0Bzeta_on. -have A0psi: psi \in 'CF(M, 'A0(M)). - by apply: cfun_onS (zchar_on M'psi); rewrite defA0 subsetUl. -have a_00: a_ (eta_ 0 0) = 1. - rewrite Da [w_ 0 0](cycTIirr00 defW) [sigma 1]cycTIiso1. - rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE. - rewrite rmorph1 /= -(prTIirr00 ptiWM) -/(mu2_ 0 0) cfdotC. - by rewrite cfdotBr o_mu2_zeta subr0 cfdot_prTIirr_red rmorph1. -have n2psiG: '[psi^\tau] = w1.+1%:R. - rewrite Dade_isometry // cfnormBd ?o_mu_zeta //. - by rewrite cfnorm_prTIred irrWnorm // -/w1 mulrSr. -have psiG_V0 x: x \in V -> psi^\tau x = 0. - move=> Vx; rewrite Dade_id ?defA0; last first. - by rewrite inE orbC mem_class_support. - rewrite (cfun_on0 (zchar_on M'psi)) // -defA. - suffices /setDP[]: x \in 'A0(M) :\: 'A(M) by []. - by rewrite (FTsupp0_typeP maxM MtypeP) // mem_class_support. -have ZpsiG: psi^\tau \in 'Z[irr G]. - by rewrite Dade_vchar // zchar_split (zcharW M'psi). -have n2psiGsum: '[psi^\tau] = \sum_i \sum_j `|a_ (eta_ i j)| ^+ 2 + '[chi]. - rewrite DpsiG addrC cfnormDd; last first. - by rewrite (span_orthogonal o_chiW) ?memv_span1. - rewrite addrC defX cfnorm_sum_orthonormal // big_map pair_bigA; congr (_ + _). - rewrite big_tuple /= (reindex (dprod_Iirr defW)) //. - by exists (inv_dprod_Iirr defW) => ij; rewrite (inv_dprod_IirrK, dprod_IirrK). -have NCpsiG: (cyclicTI_NC ctiWG psi^\tau < 2 * minn w1 w2)%N. - apply: (@leq_ltn_trans w1.+1); last first. - by rewrite /minn w1_lt_w2 mul2n -addnn (leq_add2r w1 2) cardG_gt1. - pose z_a := [pred ij | a_ (eta_ ij.1 ij.2) == 0]. - have ->: cyclicTI_NC ctiWG psi^\tau = #|[predC z_a]|. - by apply: eq_card => ij; rewrite !inE -Da. - rewrite -leC_nat -n2psiG n2psiGsum ler_paddr ?cfnorm_ge0 // pair_bigA. - rewrite (bigID z_a) big1 /= => [|ij /eqP->]; last by rewrite normCK mul0r. - rewrite add0r -sumr_const ler_sum // => [[i j] nz_ij]. - by rewrite expr_ge1 ?norm_Cint_ge1 // Da Cint_cfdot_vchar ?Zsigma ?irr_vchar. -have nz_psiG00: '[psi^\tau, eta_ 0 0] != 0 by rewrite -Da a_00 oner_eq0. -have [a_i|a_j] := small_cycTI_NC psiG_V0 NCpsiG nz_psiG00. - have psiGi: psi^\tau = \sum_i eta_ i 0 + chi. - rewrite DpsiG sumX; congr (_ + _); apply: eq_bigr => i _. - rewrite big_ord_recl /= Da a_i -Da a_00 mul1r scale1r. - by rewrite big1 ?addr0 // => j1 _; rewrite Da a_i mul0r scale0r. - split=> // [||i j]; last by rewrite cfdotNl o_chi_w oppr0. - rewrite -(canLR (addKr _) psiGi) rpredD // rpredN rpred_sum // => j _. - by rewrite Zsigma ?irr_vchar. - apply: (addrI w1%:R); rewrite -mulrSr -n2psiG n2psiGsum; congr (_ + _). - rewrite -nirrW1 // -sumr_const; apply: eq_bigr => i _. - rewrite big_ord_recl /= Da a_i -Da a_00 mul1r normr1. - by rewrite expr1n big1 ?addr0 // => j1 _; rewrite Da a_i normCK !mul0r. -suffices /idPn[]: '[psi^\tau] >= w2%:R. - rewrite odd_geq /= ?uphalf_half mFT_odd //= in w1_lt_w2. - by rewrite n2psiG leC_nat -ltnNge odd_geq ?mFT_odd. -rewrite n2psiGsum exchange_big /= ler_paddr ?cfnorm_ge0 //. -rewrite -nirrW2 -sumr_const; apply: ler_sum => i _. -rewrite big_ord_recl /= Da a_j -Da a_00 mul1r normr1. -by rewrite expr1n big1 ?addr0 // => j1 _; rewrite Da a_j normCK !mul0r. -Qed. - -Local Notation H := M'. -Local Notation "` 'H'" := `M' (at level 0) : group_scope. -Local Notation H' := M''. -Local Notation "` 'H''" := `M'' (at level 0) : group_scope. - -(* This is the bulk of the proof of Peterfalvi, Theorem (10.10); as with *) -(* (10.8), it will be restated below in order to remove dependencies on zeta, *) -(* U_M and W1. *) -Lemma FTtype5_exclusion_main : FTtype M != 5. -Proof. -apply/negP=> Mtype5. -suffices [tau1]: coherent calS M^# tau by case/FTtype345_noncoherence_main. -have [[_ U_M_1] MtypeV] := compl_of_typeV maxM MtypeP Mtype5. -have [_ [_ _ _ defH] _ [_ _ _ sW2H' _] _] := MtypeP. -have{U_M_1 defH} defMF: M`_\F = H by rewrite /= -defH U_M_1 sdprodg1. -have nilH := Fcore_nil M; rewrite defMF -/w1 in MtypeV nilH. -without loss [p [pH not_cHH ubHbar not_w1_dv_p1]]: / exists p : nat, - [/\ p.-group H, ~~ abelian H, #|H : H'| <= 4 * w1 ^ 2 + 1 & ~ w1 %| p.-1]%N. -- have [isoH1 solH] := (quotient1_isog H, nilpotent_sol nilH). - have /non_coherent_chief-IHcoh := subset_subcoherent scohS0 sSS0. - apply: IHcoh (fun coh _ => coh) _ => // [|[[_ ubH] [p [pH ab'H] /negP-dv'p]]]. - split; rewrite ?mFT_odd ?normal1 ?sub1G ?quotient_nil //. - by rewrite joingG1 (FrobeniusWker frobMbar). - apply; exists p; rewrite (isog_abelian isoH1) (isog_pgroup p isoH1) -subn1. - by rewrite /= joingG1 -(index_sdprod defM) in ubH dv'p. -have ntH: H :!=: 1%g by apply: contraNneq not_cHH => ->; apply: abelian1. -have [sH'H nH'H] := andP nsM''M'; have sW2H := subset_trans sW2H' sH'H. -have def_w2: w2 = p by apply/eqP; have:= pgroupS sW2H pH; rewrite pgroupE pnatE. -have piHp q: q \in \pi(H) -> q = p. - by rewrite /= -(part_pnat_id pH) pi_of_part // => /andP[_ /eqnP]. -have [tiHG | [_ /piHp-> []//] | [_ /piHp-> [oH w1_dv_p1 _]]] := MtypeV. - suffices [tau1 [Itau1 Dtau1]]: coherent (seqIndD H M H 1) M^# 'Ind[G]. - exists tau1; split=> // phi Sphi; rewrite {}Dtau1 //. - rewrite zcharD1_seqInd // -subG1 -setD_eq0 -defA in Sphi tiHG ntH. - by have Aphi := zchar_on Sphi; rewrite -FT_DadeE // Dade_Ind. - apply: (@Sibley_coherence _ [set:_] M H W1); first by rewrite mFT_odd. - right; exists W2 => //; exists 'A0(M), W, defW. - by rewrite -defA -{2}(group_inj defMs). -have [p_pr _ _] := pgroup_pdiv pH ntH; rewrite (pcore_pgroup_id pH) in oH. -have{not_cHH} esH: extraspecial H. - by apply: (p3group_extraspecial pH); rewrite // oH pfactorK. -have oH': #|H'| = p. - by rewrite -(card_center_extraspecial pH esH); have [[_ <-]] := esH. -have defW2: W2 :=: H' by apply/eqP; rewrite eqEcard sW2H' oH' -def_w2 /=. -have iH'H: #|H : H'|%g = (p ^ 2)%N by rewrite -divgS // oH oH' mulKn ?prime_gt0. -have w1_gt0: (0 < w1)%N by apply: cardG_gt0. -(* This is step (10.10.1). *) -have{ubHbar} [def_p_w1 w1_lt_w2]: (p = 2 * w1 - 1 /\ w1 < w2)%N. - have /dvdnP[k def_p]: 2 * w1 %| p.+1. - by rewrite Gauss_dvd ?coprime2n ?mFT_odd ?dvdn2 //= -{1}def_w2 mFT_odd. - suffices k1: k = 1%N. - rewrite k1 mul1n in def_p; rewrite -ltn_double -mul2n -def_p -addn1 addnK. - by rewrite -addnS -addnn def_w2 leq_add2l prime_gt1. - have [k0 | k_gt0] := posnP k; first by rewrite k0 in def_p. - apply/eqP; rewrite eqn_leq k_gt0 andbT -ltnS -ltn_double -mul2n. - rewrite -[(2 * k)%N]prednK ?muln_gt0 // ltnS -ltn_sqr 3?leqW //=. - rewrite -subn1 sqrn_sub ?muln_gt0 // expnMn muln1 mulnA ltnS leq_subLR. - rewrite addn1 addnS ltnS -mulnSr leq_pmul2l // -(leq_subLR _ 1). - rewrite (leq_trans (leq_pmulr _ w1_gt0)) // -(leq_pmul2r w1_gt0). - rewrite -mulnA mulnBl mul1n -2!leq_double -!mul2n mulnA mulnBr -!expnMn. - rewrite -(expnMn 2 _ 2) mulnCA -def_p -addn1 leq_subLR sqrnD muln1. - by rewrite (addnC p) mulnDr addnA leq_add2r addn1 addnS -iH'H. -(* This is step (10.10.2). *) -pose S1 := seqIndD H M H H'. -have sS1S: {subset S1 <= calS} by apply: seqIndS; rewrite Iirr_kerDS ?sub1G. -have irrS1: {subset S1 <= irr M}. - move=> _ /seqIndP[s /setDP[kerH' ker'H] ->]; rewrite !inE in kerH' ker'H. - rewrite -(quo_IirrK _ kerH') // mod_IirrE // cfIndMod // cfMod_irr //. - rewrite (irr_induced_Frobenius_ker (FrobeniusWker frobMbar)) //. - by rewrite quo_Iirr_eq0 // -subGcfker. -have S1w1: {in S1, forall xi : 'CF(M), xi 1%g = w1%:R}. - move=> _ /seqIndP[s /setDP[kerH' _] ->]; rewrite !inE in kerH'. - by rewrite cfInd1 // -(index_sdprod defM) lin_char1 ?mulr1 // lin_irr_der1. -have sS10: cfConjC_subset S1 calS0. - by apply: seqInd_conjC_subset1; rewrite /= defMs. -pose S2 := [seq mu_ j | j in predC1 0]. -have szS2: size S2 = p.-1. - by rewrite -def_w2 size_map -cardE cardC1 card_Iirr_abelian ?cyclic_abelian. -have uS2: uniq S2 by apply/dinjectiveP; apply: in2W (prTIred_inj pddM). -have redS2: {subset S2 <= [predC irr M]}. - by move=> _ /imageP[j _ ->]; apply: (prTIred_not_irr pddM). -have sS2S: {subset S2 <= calS} by move=> _ /imageP[j /calSmu Smu_j ->]. -have S1'2: {subset S2 <= [predC S1]}. - by move=> xi /redS2; apply: contra (irrS1 _). -have w1_dv_p21: w1 %| p ^ 2 - 1 by rewrite (subn_sqr p 1) addn1 dvdn_mull. -have [j nz_j] := has_nonprincipal_irr ntW2. -have [Dmu2_1 Ddelta_ lt1d Nn] := FTtype345_constants. -have{lt1d} [defS szS1 Dd Ddel Dn]: - [/\ perm_eq calS (S1 ++ S2), size S1 = (p ^ 2 - 1) %/ w1, - d = p, delta = -1 & n = 2%:R]. -- pose X_ (S0 : seq 'CF(M)) := [set s | 'Ind[M, H] 'chi_s \in S0]. - pose sumX_ cS0 := \sum_(s in X_ cS0) 'chi_s 1%g ^+ 2. - have defX1: X_ S1 = Iirr_kerD H H H'. - by apply/setP=> s; rewrite !inE mem_seqInd // !inE. - have defX: X_ calS = Iirr_kerD H H 1%g. - by apply/setP=> s; rewrite !inE mem_seqInd ?normal1 //= !inE. - have sumX1: sumX_ S1 = (p ^ 2)%:R - 1. - by rewrite /sumX_ defX1 sum_Iirr_kerD_square // iH'H indexgg mul1r. - have ->: size S1 = (p ^ 2 - 1) %/ w1. - apply/eqP; rewrite eqn_div // -eqC_nat mulnC [w1](index_sdprod defM). - rewrite (size_irr_subseq_seqInd _ (subseq_refl S1)) //. - rewrite natrB ?expn_gt0 ?prime_gt0 // -sumr_const -sumX1. - apply/eqP/esym/eq_bigr => s. - by rewrite defX1 !inE -lin_irr_der1 => /and3P[_ _ /eqP->]; rewrite expr1n. - have oX2: #|X_ S2| = p.-1. - by rewrite -(size_red_subseq_seqInd_typeP MtypeP uS2 sS2S). - have sumX2: (p ^ 2 * p.-1)%:R <= sumX_ S2 ?= iff (d == p). - rewrite /sumX_ (eq_bigr (fun _ => d%:R ^+ 2)) => [|s]; last first. - rewrite inE => /imageP[j1 nz_j1 Dj1]; congr (_ ^+ 2). - apply: (mulfI (neq0CiG M H)); rewrite -cfInd1 // -(index_sdprod defM). - by rewrite Dj1 (prTIred_1 pddM) Dmu2_1. - rewrite sumr_const oX2 mulrnA (mono_lerif (ler_pmuln2r _)); last first. - by rewrite -def_w2 -(subnKC w2gt2). - rewrite natrX (mono_in_lerif ler_sqr) ?rpred_nat // eq_sym lerif_nat. - apply/leqif_eq; rewrite dvdn_leq 1?ltnW //. - have: (mu2_ 0 j 1%g %| (p ^ 3)%N)%C. - by rewrite -(cfRes1 H) cfRes_prTIirr -oH dvd_irr1_cardG. - rewrite Dmu2_1 // dvdC_nat => /dvdn_pfactor[//|[_ d1|e _ ->]]. - by rewrite d1 in lt1d. - by rewrite expnS dvdn_mulr. - pose S3 := filter [predC S1 ++ S2] calS. - have sumX3: 0 <= sumX_ S3 ?= iff nilp S3. - rewrite /sumX_; apply/lerifP. - have [-> | ] := altP nilP; first by rewrite big_pred0 // => s; rewrite !inE. - rewrite -lt0n -has_predT => /hasP[xi S3xi _]. - have /seqIndP[s _ Dxi] := mem_subseq (filter_subseq _ _) S3xi. - rewrite (bigD1 s) ?inE -?Dxi //= ltr_spaddl ?sumr_ge0 // => [|s1 _]. - by rewrite exprn_gt0 ?irr1_gt0. - by rewrite ltrW ?exprn_gt0 ?irr1_gt0. - have [_ /esym] := lerif_add sumX2 sumX3. - have /(canLR (addKr _)) <-: sumX_ calS = sumX_ S1 + (sumX_ S2 + sumX_ S3). - rewrite [sumX_ _](big_setID (X_ S1)); congr (_ + _). - by apply: eq_bigl => s; rewrite !inE andb_idl // => /sS1S. - rewrite (big_setID (X_ S2)); congr (_ + _); apply: eq_bigl => s. - by rewrite !inE andb_idl // => S2s; rewrite [~~ _]S1'2 ?sS2S. - by rewrite !inE !mem_filter /= mem_cat orbC negb_or andbA. - rewrite sumX1 /sumX_ defX sum_Iirr_kerD_square ?sub1G ?normal1 // indexgg. - rewrite addr0 mul1r indexg1 oH opprD addrACA addNr addr0 addrC. - rewrite (expnSr p 2) -[p in (_ ^ 2 * p)%:R - _]prednK ?prime_gt0 // mulnSr. - rewrite natrD addrK eqxx => /andP[/eqP Dd /nilP S3nil]. - have uS12: uniq (S1 ++ S2). - by rewrite cat_uniq seqInd_uniq uS2 andbT; apply/hasPn. - rewrite uniq_perm_eq ?seqInd_uniq {uS12}// => [|xi]; last first. - apply/idP/idP; apply: allP xi; last by rewrite all_cat !(introT allP _). - by rewrite -(canLR negbK (has_predC _ _)) has_filter -/S3 S3nil. - have: (w1 %| d%:R - delta)%C. - by rewrite unfold_in pnatr_eq0 eqn0Ngt w1_gt0 rpred_Cnat. - rewrite /n Dd def_p_w1 /delta; case: (Idelta _) => [_|/idPn[] /=]. - by rewrite opprK -(natrD _ _ 1) subnK ?muln_gt0 // natrM mulfK ?neq0CG. - rewrite mul2n -addnn -{1}(subnKC (ltnW w1gt2)) !addSn mulrSr addrK dvdC_nat. - by rewrite add0n dvdn_addl // -(subnKC w1gt2) gtnNdvd // leqW. -have scohS1 := subset_subcoherent scohS0 sS10. -have o1S1: orthonormal S1. - rewrite orthonormalE andbC; have [_ _ -> _ _] := scohS1. - by apply/allP=> xi /irrS1/irrP[t ->]; rewrite /= cfnorm_irr. -have [tau1 cohS1]: coherent S1 M^# tau. - apply: uniform_degree_coherence scohS1 _; apply: all_pred1_constant w1%:R _ _. - by rewrite all_map; apply/allP=> xi /S1w1/= ->. -have [[Itau1 Ztau1] Dtau1] := cohS1. -have o1S1tau: orthonormal (map tau1 S1) by apply: map_orthonormal. -have S1zeta: zeta \in S1. - by have:= Szeta; rewrite (perm_eq_mem defS) mem_cat => /orP[//|/redS2/negP]. -(* This is the main part of step 10.10.3; as the definition of alpha_ remains *) -(* valid we do not need to reprove alpha_on. *) -have Dalpha i (al_ij := alpha_ i j) : - al_ij^\tau = delta *: (eta_ i j - eta_ i 0) - n *: tau1 zeta. -- have [Y S1_Y [X [Dal_ij _ oXY]]] := orthogonal_split (map tau1 S1) al_ij^\tau. - have [a_ Da_ defY] := orthonormal_span o1S1tau S1_Y. - have oXS1 lam : lam \in S1 -> '[X, tau1 lam] = 0. - by move=> S1lam; rewrite (orthoPl oXY) ?map_f. - have{Da_} Da_ lam : lam \in S1 -> a_ (tau1 lam) = '[al_ij^\tau, tau1 lam]. - by move=> S1lam; rewrite Dal_ij cfdotDl oXS1 // addr0 Da_. - pose a := n + a_ (tau1 zeta); have [_ oS1S1] := orthonormalP o1S1. - have Da_z: a_ (tau1 zeta) = - n + a by rewrite addKr. - have Za: a \in Cint. - rewrite rpredD ?Dn ?rpred_nat // Da_ // Cint_cfdot_vchar ?Zalpha_tau //=. - by rewrite Ztau1 ?mem_zchar. - have Da_z' lam: lam \in S1 -> lam != zeta -> a_ (tau1 lam) = a. - move=> S1lam zeta'lam; apply: canRL (subrK _) _. - rewrite !Da_ // -cfdotBr -raddfB. - have S1dlam: lam - zeta \in 'Z[S1, M^#]. - by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE !S1w1 ?subrr. - rewrite Dtau1 // Dade_isometry ?alpha_on ?tauM' //; last first. - by rewrite -zcharD1_seqInd ?(zchar_subset sS1S). - have o_mu2_lam k: '[mu2_ i k, lam] = 0 by rewrite o_mu2_irr ?sS1S ?irrS1. - rewrite !cfdotBl !cfdotZl !cfdotBr !o_mu2_lam !o_mu2_zeta !(subr0, mulr0). - by rewrite irrWnorm ?oS1S1 // eq_sym (negPf zeta'lam) !add0r mulrN1 opprK. - have lb_n2alij: (a - n) ^+ 2 + (size S1 - 1)%:R * a ^+ 2 <= '[al_ij^\tau]. - rewrite Dal_ij cfnormDd; last first. - by rewrite cfdotC (span_orthogonal oXY) ?rmorph0 // memv_span1. - rewrite ler_paddr ?cfnorm_ge0 // defY cfnorm_sum_orthonormal //. - rewrite (big_rem (tau1 zeta)) ?map_f //= ler_eqVlt; apply/predU1P; left. - congr (_ + _). - by rewrite Da_z addrC Cint_normK 1?rpredD // rpredN Dn rpred_nat. - rewrite (eq_big_seq (fun _ => a ^+ 2)) => [|tau1lam]; last first. - rewrite rem_filter ?free_uniq ?orthonormal_free // filter_map. - case/mapP=> lam; rewrite mem_filter /= andbC => /andP[S1lam]. - rewrite (inj_in_eq (Zisometry_inj Itau1)) ?mem_zchar // => zeta'lam ->. - by rewrite Da_z' // Cint_normK. - rewrite big_tnth sumr_const card_ord size_rem ?map_f // size_map. - by rewrite mulr_natl subn1. - have{lb_n2alij} ub_a2: (size S1)%:R * a ^+ 2 <= 2%:R * a * n + 2%:R. - rewrite norm_alpha // addrC sqrrB !addrA ler_add2r in lb_n2alij. - rewrite mulr_natl -mulrSr ler_subl_addl subn1 in lb_n2alij. - by rewrite -mulrA !mulr_natl; case: (S1) => // in S1zeta lb_n2alij *. - have{ub_a2} ub_8a2: 8%:R * a ^+ 2 <= 4%:R * a + 2%:R. - rewrite mulrAC Dn -natrM in ub_a2; apply: ler_trans ub_a2. - rewrite -Cint_normK // ler_wpmul2r ?exprn_ge0 ?normr_ge0 // leC_nat szS1. - rewrite (subn_sqr p 1) def_p_w1 subnK ?muln_gt0 // mulnA mulnK // mulnC. - by rewrite -subnDA -(mulnBr 2 _ 1%N) mulnA (@leq_pmul2l 4 2) ?ltn_subRL. - have Z_4a1: 4%:R * a - 1%:R \in Cint by rewrite rpredB ?rpredM ?rpred_nat. - have{ub_8a2} ub_4a1: `|4%:R * a - 1| < 3%:R. - rewrite -ltr_sqr ?rpred_nat ?qualifE ?normr_ge0 // -natrX Cint_normK //. - rewrite sqrrB1 exprMn -natrX -mulrnAl -mulrnA (natrD _ 8 1) ltr_add2r. - rewrite (natrM _ 2 4) (natrM _ 2 8) -!mulrA -mulrBr ltr_pmul2l ?ltr0n //. - by rewrite ltr_subl_addl (ler_lt_trans ub_8a2) // ltr_add2l ltr_nat. - have{ub_4a1} a0: a = 0. - apply: contraTeq ub_4a1 => a_nz; have:= norm_Cint_ge1 Za a_nz. - rewrite real_ltr_norml ?real_ler_normr ?Creal_Cint //; apply: contraL. - case/andP; rewrite ltr_subl_addr -(natrD _ 3 1) gtr_pmulr ?ltr0n //. - rewrite ltr_oppl opprB -mulrN => /ltr_le_trans/=/(_ _ (leC_nat 3 5)). - by rewrite (natrD _ 1 4) ltr_add2l gtr_pmulr ?ltr0n //; do 2!move/ltr_geF->. - apply: (def_tau_alpha cohS1 sS10 nz_j S1zeta). - by rewrite -Da_ // Da_z a0 addr0. -have o_eta__zeta i j1: '[tau1 zeta, eta_ i j1] = 0. - by rewrite (coherent_ortho_cycTIiso _ sS10 cohS1) ?mem_irr. -(* This is step (10.4), the final one. *) -have Dmu0zeta: (mu_ 0 - zeta)^\tau = \sum_i eta_ i 0 - tau1 zeta. - have A0mu0tau: mu_ 0 - zeta \in 'CF(M, 'A0(M)). - rewrite /'A0(M) defA; apply: (cfun_onS (subsetUl _ _)). - rewrite cfun_onD1 [mu_ 0](prTIred0 pddM) !cfunE zeta1w1 cfuniE // group1. - by rewrite mulr1 subrr rpredB ?rpredZnat ?cfuni_on ?(seqInd_on _ Szeta) /=. - have [chi [Dmu0 Zchi n1chi o_chi_w]] := FTtype345_Dade_bridge0 w1_lt_w2. - have dirr_chi: chi \in dirr G by rewrite dirrE Zchi n1chi /=. - have dirr_zeta: tau1 zeta \in dirr G. - by rewrite dirrE Ztau1 ?Itau1 ?mem_zchar //= irrWnorm. - have: '[(alpha_ 0 j)^\tau, (mu_ 0 - zeta)^\tau] == - delta + n. - rewrite Dade_isometry ?alpha_on // !cfdotBl !cfdotZl !cfdotBr. - rewrite !o_mu2_zeta 2!cfdot_prTIirr_red (negPf nz_j) cfdotC o_mu_zeta. - by rewrite eqxx irrWnorm // conjC0 !(subr0, add0r) mulr1 mulrN1 opprK. - rewrite Dalpha // Dmu0 !{1}(cfdotBl, cfdotZl) !cfdotBr 2!{1}(cfdotC _ chi). - rewrite !o_chi_w conjC0 !cfdot_sumr big1 => [|i]; first last. - by rewrite (cfdot_cycTIiso pddM) (negPf nz_j) andbF. - rewrite (bigD1 0) //= cfdot_cycTIiso big1 => [|i nz_i]; first last. - by rewrite cfdot_cycTIiso eq_sym (negPf nz_i). - rewrite big1 // !subr0 !add0r addr0 mulrN1 mulrN opprK (can_eq (addKr _)). - rewrite {2}Dn -mulr_natl Dn (inj_eq (mulfI _)) ?pnatr_eq0 //. - by rewrite cfdot_dirr_eq1 // => /eqP->. -have [] := uniform_prTIred_coherent pddM nz_j; rewrite -/sigma. -have ->: uniform_prTIred_seq pddM j = S2. - congr (map _ _); apply: eq_enum => k; rewrite !inE -!/(mu_ _). - by rewrite andb_idr // => nz_k; rewrite 2!{1}prTIred_1 2?Dmu2_1. -case=> _ _ ccS2 _ _ [tau2 Dtau2 cohS2]. -have{cohS2} cohS2: coherent_with S2 M^# tau tau2 by apply: cohS2. -have sS20: cfConjC_subset S2 calS0. - by split=> // xi /sS2S Sxi; have [_ ->] := sSS0. -rewrite perm_eq_sym perm_catC in defS; apply: perm_eq_coherent defS _. -suffices: (mu_ j - d%:R *: zeta)^\tau = tau2 (mu_ j) - tau1 (d%:R *: zeta). - apply: (bridge_coherent scohS0 sS20 cohS2 sS10 cohS1) => [phi|]. - by apply: contraL => /S1'2. - rewrite cfunD1E !cfunE zeta1w1 prTIred_1 mulrC Dmu2_1 // subrr. - by rewrite image_f // rpredZnat ?mem_zchar. -have sumA: \sum_i alpha_ i j = mu_ j - delta *: mu_ 0 - (d%:R - delta) *: zeta. - rewrite !sumrB sumr_const /= -scaler_sumr; congr (_ - _ - _). - rewrite card_Iirr_abelian ?cyclic_abelian // -/w1 -scaler_nat. - by rewrite scalerA mulrC divfK ?neq0CG. -rewrite scalerBl opprD opprK addrACA in sumA. -rewrite -{sumA}(canLR (addrK _) sumA) opprD opprK -scalerBr. -rewrite linearD linearZ linear_sum /= Dmu0zeta scalerBr. -rewrite (eq_bigr _ (fun i _ => Dalpha i)) sumrB sumr_const nirrW1. -rewrite -!scaler_sumr sumrB addrAC !addrA scalerBr subrK -addrA -opprD. -rewrite raddfZnat Dtau2 Ddelta_ //; congr (_ - _). -by rewrite addrC -scaler_nat scalerA mulrC divfK ?neq0CG // -scalerDl subrK. -Qed. - -End OneMaximal. - -Implicit Type M : {group gT}. - -(* This is the exported version of Peterfalvi, Theorem (10.8). *) -Theorem FTtype345_noncoherence M (M' := M^`(1)%G) (maxM : M \in 'M) : - (FTtype M > 2)%N -> ~ coherent (seqIndD M' M M' 1) M^# (FT_Dade0 maxM). -Proof. -rewrite ltnNge 2!leq_eqVlt => /norP[notMtype2 /norP[notMtype1 _]] [tau1 cohS]. -have [U W W1 W2 defW MtypeP] := FTtypeP_witness maxM notMtype1. -have [zeta [irr_zeta Szeta zeta1w1]] := FTtypeP_ref_irr maxM MtypeP. -exact: (FTtype345_noncoherence_main MtypeP _ irr_zeta Szeta zeta1w1 cohS). -Qed. - -(* This is the exported version of Peterfalvi, Theorem (10.10). *) -Theorem FTtype5_exclusion M : M \in 'M -> FTtype M != 5. -Proof. -move=> maxM; apply: wlog_neg; rewrite negbK => Mtype5. -have notMtype2: FTtype M != 2 by rewrite (eqP Mtype5). -have [U W W1 W2 defW [[MtypeP _] _]] := FTtypeP 5 maxM Mtype5. -have [zeta [irr_zeta Szeta zeta1w1]] := FTtypeP_ref_irr maxM MtypeP. -exact: (FTtype5_exclusion_main _ MtypeP _ irr_zeta). -Qed. - -(* This the first assertion of Peterfalvi (10.11). *) -Lemma FTtypeP_pair_primes S T W W1 W2 (defW : W1 \x W2 = W) : - typeP_pair S T defW -> prime #|W1| /\ prime #|W2|. -Proof. -move=> pairST; have [[_ maxS maxT] _ _ _ _] := pairST. -have type24 maxM := compl_of_typeII_IV maxM _ (FTtype5_exclusion maxM). -split; first by have [U /type24[]] := typeP_pairW pairST. -have xdefW: W2 \x W1 = W by rewrite dprodC. -by have [U /type24[]] := typeP_pairW (typeP_pair_sym xdefW pairST). -Qed. - -Corollary FTtypeP_primes M U W W1 W2 (defW : W1 \x W2 = W) : - M \in 'M -> of_typeP M U defW -> prime #|W1| /\ prime #|W2|. -Proof. -move=> maxM MtypeP; have [T pairMT _] := FTtypeP_pair_witness maxM MtypeP. -exact: FTtypeP_pair_primes pairMT. -Qed. - -(* This is the remainder of Peterfalvi (10.11). *) -Lemma FTtypeII_prime_facts M U W W1 W2 (defW : W1 \x W2 = W) (maxM : M \in 'M) : - of_typeP M U defW -> FTtype M == 2 -> - let H := M`_\F%G in let HU := M^`(1)%G in - let calS := seqIndD HU M H 1 in let tau := FT_Dade0 maxM in - let p := #|W2| in let q := #|W1| in - [/\ p.-abelem H, (#|H| = p ^ q)%N & coherent calS M^# tau]. -Proof. -move=> MtypeP Mtype2 H HU calS tau p q. -have Mnot5: FTtype M != 5 by rewrite (eqP Mtype2). -have [_ cUU _ _ _] := compl_of_typeII maxM MtypeP Mtype2. -have [q_pr p_pr]: prime q /\ prime p := FTtypeP_primes maxM MtypeP. -have:= typeII_IV_core maxM MtypeP Mnot5; rewrite Mtype2 -/p -/q => [[_ oH]]. -have [] := Ptype_Fcore_kernel_exists maxM MtypeP Mnot5. -have [_ _] := Ptype_Fcore_factor_facts maxM MtypeP Mnot5. -rewrite -/H; set H0 := Ptype_Fcore_kernel _; set Hbar := (H / H0)%G. -rewrite def_Ptype_factor_prime // -/p -/q => oHbar chiefHbar _. -have trivH0: H0 :=: 1%g. - have [/maxgroupp/andP[/andP[sH0H _] nH0M] /andP[sHM _]] := andP chiefHbar. - apply: card1_trivg; rewrite -(setIidPr sH0H) -divg_index. - by rewrite -card_quotient ?(subset_trans sHM) // oHbar -oH divnn cardG_gt0. -have abelHbar: p.-abelem Hbar. - have pHbar: p.-group Hbar by rewrite /pgroup oHbar pnat_exp pnat_id. - by rewrite -is_abelem_pgroup // (sol_chief_abelem _ chiefHbar) ?mmax_sol. -rewrite /= trivH0 -(isog_abelem (quotient1_isog _)) in abelHbar. -have:= Ptype_core_coherence maxM MtypeP Mnot5; rewrite trivH0. -set C := _ MtypeP; have sCU: C \subset U by rewrite [C]unlock subsetIl. -by rewrite (derG1P (abelianS sCU cUU)) [(1 <*> 1)%G]join1G. -Qed. - -End Ten. |