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/PFsection9.v | |
| parent | c1ec9cd8e7e50f73159613c492aad4c6c40bc3aa (diff) | |
move odd_order to its own repository
Diffstat (limited to 'mathcomp/odd_order/PFsection9.v')
| -rw-r--r-- | mathcomp/odd_order/PFsection9.v | 2211 |
1 files changed, 0 insertions, 2211 deletions
diff --git a/mathcomp/odd_order/PFsection9.v b/mathcomp/odd_order/PFsection9.v deleted file mode 100644 index d8ec417..0000000 --- a/mathcomp/odd_order/PFsection9.v +++ /dev/null @@ -1,2211 +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 binomial ssralg poly finset. -From mathcomp -Require Import fingroup morphism perm automorphism quotient action finalg zmodp. -From mathcomp -Require Import gfunctor gproduct cyclic commutator center gseries nilpotent. -From mathcomp -Require Import pgroup 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 algC classfun character inertia vcharacter. -From mathcomp -Require Import PFsection1 PFsection2 PFsection3 PFsection4. -From mathcomp -Require Import PFsection5 PFsection6 PFsection8. - -(******************************************************************************) -(* This file covers Peterfalvi, Section 9: On the maximal subgroups of Types *) -(* II, III and IV. For defW : W1 \x W2 = W, MtypeP : of_typeP M U defW, and *) -(* H := M`_\F we define : *) -(* Ptype_Fcore_kernel MtypeP == a maximal normal subgroup of M contained *) -(* (locally) H0 in H and containing 'C_H(U), provided M is *) -(* not a maximal subgroup of type V. *) -(* Ptype_Fcore_kernel MtypeP == the stabiliser of Hbar := H / H0 in U; this *) -(* (locally to this file) C is locked for performance reasons. *) -(* typeP_Galois MtypeP <=> U acts irreducibly on Hbar; this implies *) -(* that M / H0C is isomorphic to a Galois group *) -(* acting on the semidirect product of the *) -(* additive group of a finite field with a *) -(* a subgroup of its multiplicative group. *) -(* --> This predicate reflects alternative (b) in Peterfalvi (9.7). *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import GroupScope GRing.Theory FinRing.Theory. - -Section Nine. - -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 V W : {group gT}. - -(* Peterfalvi (9.1) is covered by BGsection3.Frobenius_Wielandt_fixpoint. *) - -(* These assumptions correspond to Peterfalvi, Hypothesis (9.2). *) - -Variables M U W W1 W2 : {group gT}. -Hypotheses (maxM : M \in 'M) (defW : W1 \x W2 = W) (MtypeP: of_typeP M U defW). -Hypothesis notMtype5 : FTtype M != 5. - -Local Notation "` 'M'" := (gval M) (at level 0, only parsing) : group_scope. -Local Notation "` 'U'" := (gval U) (at level 0, only parsing) : group_scope. -Local Notation "` 'W1'" := (gval W1) (at level 0, only parsing) : group_scope. -Local Notation H := `M`_\F%G. -Local Notation "` 'H'" := `M`_\F (at level 0) : group_scope. -Local Notation "` 'W2'" := (gval W2) (at level 0, only parsing) : group_scope. -Local Notation HU := M^`(1)%G. -Local Notation "` 'HU'" := `M^`(1) (at level 0) : group_scope. -Local Notation U' := U^`(1)%G. -Local Notation "` 'U''" := `U^`(1) (at level 0) : group_scope. - -Let q := #|W1|. - -Let defM : HU ><| W1 = M. Proof. by have [[]] := MtypeP. Qed. -Let defHU : H ><| U = HU. Proof. by have [_ []] := MtypeP. Qed. -Let nUW1 : W1 \subset 'N(U). Proof. by have [_ []] := MtypeP. Qed. -Let cHU' : U' \subset 'C(H). Proof. by have [_ []] := typeP_context MtypeP. Qed. - -Let notMtype1 : FTtype M != 1%N. Proof. exact: FTtypeP_neq1 MtypeP. Qed. - -Local Notation Mtype24 := (compl_of_typeII_IV maxM MtypeP notMtype5). -Let ntU : U :!=: 1. Proof. by have [] := Mtype24. Qed. -Let pr_q : prime q. Proof. by have [] := Mtype24. Qed. -Let ntW2 : W2 :!=: 1. Proof. by have [_ _ _ []] := MtypeP. Qed. -Let sW2H : W2 \subset H. Proof. by have [_ _ _ []] := MtypeP. Qed. -Let defW2 : 'C_H(W1) = W2. Proof. exact: typeP_cent_core_compl MtypeP. Qed. - -Lemma Ptype_Fcore_sdprod : H ><| (U <*> W1) = M. -Proof. -have [_ /= sW1M mulHUW1 _ tiHUW1] := sdprod_context defM. -have [/= /andP[sHHU _] sUHU mulHU nHU tiHU] := sdprod_context defHU. -rewrite sdprodE /= norm_joinEr // ?mulgA ?mulHU //. - by rewrite mulG_subG nHU (subset_trans sW1M) ?gFnorm. -rewrite setIC -(setIidPr sHHU) setIA -group_modl //. -by rewrite (setIC W1) tiHUW1 mulg1 setIC tiHU. -Qed. -Local Notation defHUW1 := Ptype_Fcore_sdprod. - -Lemma Ptype_Fcore_coprime : coprime #|H| #|U <*> W1|. -Proof. -by rewrite (coprime_sdprod_Hall_l defHUW1) ?(pHall_Hall (Fcore_Hall M)). -Qed. -Let coH_UW1 := Ptype_Fcore_coprime. -Let coHU : coprime #|H| #|U|. -Proof. exact: coprimegS (joing_subl U W1) coH_UW1. Qed. - -Let not_cHU : ~~ (U \subset 'C(H)). -Proof. by have [_ [_ ->]] := typeP_context MtypeP. Qed. - -Lemma Ptype_compl_Frobenius : [Frobenius U <*> W1 = U ><| W1]. -Proof. -have [[_ _ ntW1 _] _ _ [_ _ _ _ prHU_W1] _] := MtypeP. -have [[_ _ _ tiHUW1] [_ sUHU _ _ tiHU]] := (sdprodP defM, sdprod_context defHU). -apply/Frobenius_semiregularP=> // [|x /prHU_W1 defCx]. - by rewrite sdprodEY //; apply/trivgP; rewrite -tiHUW1 setSI. -by apply/trivgP; rewrite -tiHU /= -{1}(setIidPr sUHU) setIAC defCx setSI. -Qed. -Local Notation frobUW1 := Ptype_compl_Frobenius. - -Let nilH : nilpotent H. Proof. exact: Fcore_nil. Qed. -Let solH : solvable H. Proof. exact: nilpotent_sol. Qed. - -(* This is Peterfalvi (9.3). *) -Lemma typeII_IV_core (p := #|W2|) : - if FTtype M == 2 then 'C_H(U) = 1 /\ #|H| = (#|W2| ^ q)%N - else [/\ prime p, 'C_H(U <*> W1) = 1 & #|H| = (p ^ q * #|'C_H(U)|)%N]. -Proof. -have [_ _ nHUW1 _] := sdprodP defHUW1. -have /= [oH _ oH1] := Frobenius_Wielandt_fixpoint frobUW1 nHUW1 coH_UW1 solH. -have [Mtype2 {oH}| notMtype2 {oH1}] := boolP (FTtype M == 2). - suffices regHU: 'C_H(U) = 1 by rewrite -defW2 oH1. - have [_ _ _ HUtypeF defHUF] := compl_of_typeII maxM MtypeP Mtype2. - have [_ _ [U0 [sU0U _]]] := HUtypeF; rewrite {}defHUF => frobHU0. - have /set0Pn[x U0x]: U0^# != set0. - by rewrite setD_eq0 subG1; case/Frobenius_context: frobHU0. - apply/trivgP; rewrite -(Frobenius_reg_ker frobHU0 U0x) setIS // -cent_cycle. - by rewrite centS // cycle_subG (subsetP sU0U) //; case/setD1P: U0x. -have p_pr: prime p. - have [S pairMS [xdefW [U_S StypeP]]] := FTtypeP_pair_witness maxM MtypeP. - have [[_ _ maxS] _] := pairMS; rewrite {1}(negPf notMtype2) /= => Stype2 _ _. - by have [[]] := compl_of_typeII maxS StypeP Stype2. -rewrite -/q -/p centY setICA defW2 setIC in oH *. -suffices regW2U: 'C_W2(U) = 1 by rewrite -oH regW2U cards1 exp1n mul1n. -apply: prime_TIg => //=; apply: contra not_cHU => /setIidPl cUW2. -rewrite centsC (sameP setIidPl eqP) eqEcard subsetIl. -by rewrite -(@leq_pmul2l (p ^ q)) -?oH ?cUW2 //= expn_gt0 cardG_gt0. -Qed. - -(* Existential witnesses for Peterfalvi (9.4). *) -Definition Ptype_Fcore_kernel of of_typeP M U defW := - odflt 1%G [pick H0 : {group gT} | chief_factor M H0 H & 'C_H(U) \subset H0]. -Let H0 := (Ptype_Fcore_kernel MtypeP). -Local Notation "` 'H0'" := (gval H0) (at level 0, only parsing) : group_scope. -Local Notation Hbar := (H / `H0)%G. -Local Notation "` 'Hbar'" := (`H / `H0)%g (at level 0) : group_scope. -Let p := pdiv #|Hbar|. - -(* This corresponds to Peterfalvi (9.4). *) -Lemma Ptype_Fcore_kernel_exists : chief_factor M H0 H /\ 'C_H(U) \subset H0. -Proof. -pose S := <<class_support 'C_H(U) H>> . -suffices [H1 maxH sCH1]: {H1 : {group gT} | maxnormal H1 H M & S \subset H1}. - apply/andP; rewrite /H0 /Ptype_Fcore_kernel; case: pickP => // /(_ H1)/idP[]. - rewrite /chief_factor maxH Fcore_normal (subset_trans _ sCH1) ?sub_gen //. - exact: sub_class_support. -apply/maxgroup_exists/andP; split. - have snCH: 'C_H(U) <|<| H by rewrite nilpotent_subnormal ?subsetIl. - by have [/setIidPl/idPn[] | // ] := subnormalEsupport snCH; rewrite centsC. -have [_ {3}<- nHUW1 _] := (sdprodP defHUW1). -rewrite norms_gen // mulG_subG class_support_norm norms_class_support //. -by rewrite normsI ?norms_cent // join_subG normG. -Qed. - -Let chiefH0 : chief_factor M H0 H. -Proof. by have [] := Ptype_Fcore_kernel_exists. Qed. -Let ltH0H : H0 \proper H. -Proof. by case/andP: chiefH0 => /maxgroupp/andP[]. Qed. -Let nH0M : M \subset 'N(H0). -Proof. by case/andP: chiefH0 => /maxgroupp/andP[]. Qed. -Let sH0H : H0 \subset H. Proof. exact: proper_sub ltH0H. Qed. -Let nsH0M : H0 <| M. Proof. by rewrite /normal (subset_trans sH0H) ?gFsub. Qed. -Let nsH0H : H0 <| H. Proof. by rewrite (normalS _ (Fcore_sub _)). Qed. -Let minHbar : minnormal Hbar (M / H0). -Proof. exact: chief_factor_minnormal. Qed. -Let ntHbar : Hbar :!=: 1. Proof. by case/mingroupp/andP: minHbar. Qed. -Let solHbar: solvable Hbar. Proof. by rewrite quotient_sol. Qed. -Let abelHbar : p.-abelem Hbar. -Proof. by have [] := minnormal_solvable minHbar _ solHbar. Qed. -Let p_pr : prime p. Proof. by have [/pgroup_pdiv[]] := and3P abelHbar. Qed. -Let abHbar : abelian Hbar. Proof. exact: abelem_abelian abelHbar. Qed. - -(* This is Peterfalvi, Hypothesis (9.5). *) -Fact Ptype_Fcompl_kernel_key : unit. Proof. by []. Qed. -Definition Ptype_Fcompl_kernel := - locked_with Ptype_Fcompl_kernel_key 'C_U(Hbar | 'Q)%G. -Local Notation C := Ptype_Fcompl_kernel. -Local Notation "` 'C'" := (gval C) (at level 0, only parsing) : group_scope. -Local Notation Ubar := (U / `C)%G. -Local Notation "` 'Ubar'" := (`U / `C)%g (at level 0) : group_scope. -Local Notation W1bar := (W1 / `H0)%G. -Local Notation "` 'W1bar'" := (`W1 / `H0)%g (at level 0) : group_scope. -Local Notation W2bar := 'C_Hbar(`W1bar)%G. -Local Notation "` 'W2bar'" := 'C_`Hbar(`W1bar) (at level 0) : group_scope. -Let c := #|C|. -Let u := #|Ubar|. -Local Notation tau := (FT_Dade0 maxM). -Local Notation "chi ^\tau" := (tau chi). -Let calX := Iirr_kerD M^`(1) H 1. -Let calS := seqIndD M^`(1) M M`_\F 1. -Let X_ Y := Iirr_kerD M^`(1) H Y. -Let S_ Y := seqIndD M^`(1) M M`_\F Y. - -Local Notation inMb := (coset (gval H0)). - -Local Notation H0C := (`H0 <*> `C)%G. -Local Notation "` 'H0C'" := (`H0 <*> `C) (at level 0) : group_scope. -Local Notation HC := (`H <*> `C)%G. -Local Notation "` 'HC'" := (`H <*> `C) (at level 0) : group_scope. -Local Notation H0U' := (`H0 <*> `U')%G. -Local Notation "` 'H0U''" := (gval H0 <*> `U')%G (at level 0) : group_scope. -Local Notation H0C' := (`H0 <*> `C^`(1)%g)%G. -Local Notation "` 'H0C''" := (`H0 <*> `C^`(1)) (at level 0) : group_scope. - -Let defW2bar : W2bar :=: W2 / H0. -Proof. -rewrite -defW2 coprime_quotient_cent ?(subset_trans _ nH0M) //. - by have [_ /mulG_sub[]] := sdprodP defM. -exact: coprimegS (joing_subr _ _) coH_UW1. -Qed. - -Let sCU : C \subset U. Proof. by rewrite [C]unlock subsetIl. Qed. - -Let nsCUW1 : C <| U <*> W1. -Proof. -have [_ sUW1M _ nHUW1 _] := sdprod_context defHUW1. -rewrite /normal [C]unlock subIset ?joing_subl // normsI //. - by rewrite join_subG normG. -rewrite /= astabQ norm_quotient_pre ?norms_cent ?quotient_norms //. -exact: subset_trans sUW1M nH0M. -Qed. - -Lemma Ptype_Fcore_extensions_normal : - [/\ H0C <| M, HC <| M, H0U' <| M & H0C' <| M]. -Proof. -have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. -have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. -have [sHM sUM] := (subset_trans sHHU sHUM, subset_trans sUHU sHUM). -have sCM: C \subset M := subset_trans sCU sUM. -have sH0C_M: H0C \subset M by rewrite /normal join_subG (subset_trans sH0H). -have [nH0C nH0_H0C] := (subset_trans sCM nH0M, subset_trans sH0C_M nH0M). -have nsH0C: H0C <| M. - rewrite /normal sH0C_M -{1}defM sdprodEY //= -defHU sdprodEY //= -joingA. - rewrite join_subG andbC normsY ?(normal_norm nsCUW1) //=; last first. - by rewrite (subset_trans _ nH0M) // join_subG sUM. - rewrite -quotientYK // -{1}(quotientGK nsH0H) morphpre_norms //= [C]unlock. - by rewrite cents_norm // centsC -quotient_astabQ quotientS ?subsetIr. -split=> //; first by rewrite /= -{1}(joing_idPl sH0H) -joingA normalY ?gFnormal. - rewrite normalY // /normal gFsub_trans //=. - rewrite -defM sdprodEY //= -defHU sdprodEY //=. - by rewrite !join_subG gFnorm cents_norm ?gFnorm_trans // centsC. -suffices ->: H0C' :=: H0 <*> H0C^`(1) by rewrite normalY ?gFnormal_trans. -by rewrite /= -!quotientYK ?gFsub_trans ?quotient_der ?subsetIl //= cosetpreK. -Qed. -Local Notation nsH0xx_M := Ptype_Fcore_extensions_normal. - -Let Du : u = #|HU : HC|. -Proof. -have nCU := subset_trans (joing_subl U W1) (normal_norm nsCUW1). -by rewrite -(index_sdprodr defHU) -?card_quotient. -Qed. - -(* This is Peterfalvi (9.6). *) -Lemma Ptype_Fcore_factor_facts : - [/\ C :!=: U, #|W2bar| = p & #|Hbar| = p ^ q]%N. -Proof. -have [defUW1 _ ntW1 _ _] := Frobenius_context Ptype_compl_Frobenius. -have coHW1: coprime #|H| #|W1| := coprimegS (joing_subr U W1) coH_UW1. -have [_ sUW1M _ nHUW1 _] := sdprod_context defHUW1. -have nH0UW1 := subset_trans sUW1M nH0M; have [nH0U nH0W1] := joing_subP nH0UW1. -have regUHb: 'C_Hbar(U / H0) = 1. - have [_ sCH0] := Ptype_Fcore_kernel_exists. - by rewrite -coprime_quotient_cent ?(nilpotent_sol nilH) ?quotientS1. -have ->: C != U. - apply: contraNneq ntHbar => defU; rewrite -subG1 -regUHb subsetIidl centsC. - by rewrite -defU [C]unlock -quotient_astabQ quotientS ?subsetIr. -have frobUW1b: [Frobenius U <*> W1 / H0 = (U / H0) ><| W1bar]. - have tiH0UW1 := coprime_TIg (coprimeSg sH0H coH_UW1). - have /isomP[inj_f im_f] := quotient_isom nH0UW1 tiH0UW1. - have:= injm_Frobenius (subxx _) inj_f frobUW1. - by rewrite im_f !morphim_restrm !(setIidPr _) ?joing_subl ?joing_subr. -have{frobUW1b} oHbar: #|Hbar| = (#|W2bar| ^ q)%N. - have nHbUW1 : U <*> W1 / H0 \subset 'N(Hbar) := quotient_norms H0 nHUW1. - have coHbUW1 : coprime #|Hbar| #|U <*> W1 / H0| by apply: coprime_morph. - have [//|_ _ -> //] := Frobenius_Wielandt_fixpoint frobUW1b nHbUW1 coHbUW1 _. - by rewrite -(card_isog (quotient_isog _ _)) // coprime_TIg ?(coprimeSg sH0H). -have abelW2bar: p.-abelem W2bar := abelemS (subsetIl _ _) abelHbar. -rewrite -(part_pnat_id (abelem_pgroup abelW2bar)) p_part in oHbar *. -suffices /eqP cycW2bar: logn p #|W2bar| == 1%N by rewrite oHbar cycW2bar. -have cycW2: cyclic W2 by have [_ _ _ []] := MtypeP. -rewrite eqn_leq -abelem_cyclic //= -/W2bar {1}defW2bar quotient_cyclic //=. -rewrite lt0n; apply: contraNneq ntHbar => W2bar1. -by rewrite trivg_card1 oHbar W2bar1 exp1n. -Qed. - -Lemma def_Ptype_factor_prime : prime #|W2| -> p = #|W2|. -Proof. -move=> prW2; suffices: p \in \pi(W2) by rewrite !(primes_prime, inE) // => /eqP. -rewrite mem_primes p_pr cardG_gt0; have [_ <- _] := Ptype_Fcore_factor_facts. -by rewrite defW2bar dvdn_quotient. -Qed. - -(* The first assertion of (9.4)(b) (the rest is subsumed by (9.6)). *) -Lemma typeIII_IV_core_prime : FTtype M != 2 -> p = #|W2|. -Proof. -by have:= typeII_IV_core => /=; case: ifP => // _ [/def_Ptype_factor_prime]. -Qed. - -Let frobUW1c : [Frobenius U <*> W1 / C = Ubar ><| W1 / C]. -Proof. -apply: Frobenius_quotient frobUW1 _ nsCUW1 _. - by apply: nilpotent_sol; have [_ []] := MtypeP. -by have [] := Ptype_Fcore_factor_facts; rewrite eqEsubset sCU. -Qed. - -Definition typeP_Galois := acts_irreducibly U Hbar 'Q. - -(* This is Peterfalvi (9.7)(a). *) -Lemma typeP_Galois_Pn : - ~~ typeP_Galois -> - {H1 : {group coset_of H0} | - [/\ #|H1| = p, U / H0 \subset 'N(H1), [acts U, on H1 | 'Q], - \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar - & let a := #|U : 'C_U(H1 | 'Q)| in - [/\ a > 1, a %| p.-1, cyclic (U / 'C_U(H1 | 'Q)) - & exists V : {group 'rV['Z_a]_q.-1}, Ubar \isog V]]}. -Proof. -have [_ sUW1M defHUW1 nHUW1 _] := sdprod_context defHUW1. -have [nHU nHW1] := joing_subP nHUW1. -have nH0UW1 := subset_trans sUW1M nH0M; have [nH0U nH0W1] := joing_subP nH0UW1. -rewrite /typeP_Galois acts_irrQ //= => not_minHbarU. -have [H1 minH1 sH1Hb]: {H1 | minnormal (gval H1) (U / H0) & H1 \subset Hbar}. - by apply: mingroup_exists; rewrite ntHbar quotient_norms. -exists H1; have [defH1 | ltH1H] := eqVproper sH1Hb. - by rewrite -defH1 minH1 in not_minHbarU. -have [/andP[ntH1 nH1U] _] := mingroupP minH1. -have actsUH1: [acts U, on H1 | 'Q]. - by rewrite -(cosetpreK H1) actsQ ?norm_quotient_pre. -have [nH0H [neqCU _ oHbar]] := (normal_norm nsH0H, Ptype_Fcore_factor_facts). -have nUW1b: W1bar \subset 'N(U / H0) by apply: quotient_norms. -have oW1b: #|W1bar| = q. - rewrite -(card_isog (quotient_isog _ _)) // coprime_TIg //. - by rewrite (coprimeSg sH0H) // (coprimegS (joing_subr U W1)). -have [oH1 defHbar]: #|H1| = p /\ \big[dprod/1]_(w in W1bar) H1 :^ w = Hbar. - have nHbUW1: U <*> W1 / H0 \subset 'N(Hbar) by apply: quotient_norms. - pose rUW1 := abelem_repr abelHbar ntHbar nHbUW1. - have irrUW1: mx_irreducible rUW1. - apply/abelem_mx_irrP/mingroupP; split=> [|H2]; first by rewrite ntHbar. - case/andP=> ntH2 nH2UW1 sH2H; case/mingroupP: minHbar => _; apply=> //. - by rewrite ntH2 -defHUW1 quotientMl // mulG_subG sub_abelian_norm. - have nsUUW1: U / H0 <| U <*> W1 / H0 by rewrite quotient_normal // normalYl. - pose rU := subg_repr rUW1 (normal_sub nsUUW1). - pose V1 := rowg_mx (abelem_rV abelHbar ntHbar @* H1). - have simV1: mxsimple rU V1 by apply/mxsimple_abelem_subg/mxsimple_abelemGP. - have [W0 /subsetP sW01 [sumW0 dxW0]] := Clifford_basis irrUW1 simV1. - have def_q: q = (#|W0| * \rank V1)%N. - transitivity (\rank (\sum_(w in W0) V1 *m rUW1 w))%R. - by rewrite sumW0 mxrank1 /= (dim_abelemE abelHbar) // oHbar pfactorK. - rewrite (mxdirectP dxW0) -sum_nat_const; apply: eq_bigr => x /sW01/= Wx. - by rewrite mxrankMfree ?row_free_unit ?repr_mx_unit. - have oH1: #|H1| = (p ^ \rank V1)%N. - by rewrite -{1}(card_Fp p_pr) -card_rowg rowg_mxK card_injm ?abelem_rV_injm. - have oW0: #|W0| = q. - apply/prime_nt_dvdP=> //; last by rewrite def_q dvdn_mulr. - apply: contraTneq (proper_card ltH1H) => trivW0. - by rewrite oHbar def_q trivW0 mul1n -oH1 ltnn. - have q_gt0 := prime_gt0 pr_q. - rewrite oH1 -(mulKn (\rank V1) q_gt0) -{1}oW0 -def_q divnn q_gt0. - have defHbar: \big[dprod/1]_(w in W0) H1 :^ w = Hbar. - have inj_rV_Hbar := rVabelem_injm abelHbar ntHbar. - have/(injm_bigdprod _ inj_rV_Hbar)/= := bigdprod_rowg sumW0 dxW0. - rewrite sub_im_abelem_rV rowg1 im_rVabelem => <- //=; apply: eq_bigr => w. - by move/sW01=> Ww; rewrite abelem_rowgJ ?rowg_mxK ?abelem_rV_mK. - have injW0: {in W0 &, injective (fun w => H1 :^ w)}. - move=> x y Wx Wy /= eq_Hxy; apply: contraNeq ntH1 => neq_xy. - rewrite -(conjsg_eq1 _ x) -[H1 :^ x]setIid {1}eq_Hxy; apply/eqP. - rewrite (bigD1 y) // (bigD1 x) /= ?Wx // dprodA in defHbar. - by case/dprodP: defHbar => [[_ _ /dprodP[_ _ _ ->] _]]. - have defH1W0: [set H1 :^ w | w in W0] = [set H1 :^ w | w in W1 / H0]. - apply/eqP; rewrite eqEcard (card_in_imset injW0) oW0 -oW1b leq_imset_card. - rewrite andbT; apply/subsetP=> _ /imsetP[w /sW01/= Ww ->]. - move: Ww; rewrite norm_joinEr ?quotientMl // => /mulsgP[x w1 Ux Ww1 ->]. - by rewrite conjsgM (normsP nH1U) // mem_imset. - have injW1: {in W1 / H0 &, injective (fun w => H1 :^ w)}. - by apply/imset_injP; rewrite -defH1W0 (card_in_imset injW0) oW0 oW1b. - by rewrite -(big_imset id injW1) -defH1W0 big_imset. -split=> //; set a := #|_ : _|; pose q1 := #|(W1 / H0)^#|. -have a_gt1: a > 1. - rewrite indexg_gt1 subsetIidl /= astabQ -sub_quotient_pre //. - apply: contra neqCU => cH1U; rewrite [C]unlock (sameP eqP setIidPl) /= astabQ. - rewrite -sub_quotient_pre // -(bigdprodWY defHbar) cent_gen centsC. - by apply/bigcupsP=> w Ww; rewrite centsC centJ -(normsP nUW1b w) ?conjSg. -have Wb1: 1 \in W1bar := group1 _. -have ->: q.-1 = q1 by rewrite -oW1b (cardsD1 1) Wb1. -have /cyclicP[h defH1]: cyclic H1 by rewrite prime_cyclic ?oH1. -have o_h: #[h] = p by rewrite defH1 in oH1. -have inj_Zp_h w := injm_Zp_unitm (h ^ w). -pose phi w := invm (inj_Zp_h w) \o restr_perm <[h ^ w]> \o actperm 'Q. -have dU w: w \in W1bar -> {subset U <= 'dom (phi w)}. - move=> Ww x Ux; have Qx := subsetP (acts_dom actsUH1) x Ux. - rewrite inE Qx /= im_Zp_unitm inE mem_morphpre //=; last first. - by apply: Aut_restr_perm (actperm_Aut 'Q _); rewrite //= quotientT. - rewrite cycleJ -defH1 !inE /=; apply/subsetP=> z H1w_z; rewrite inE actpermK. - rewrite qactJ (subsetP nH0U) ?memJ_norm // normJ mem_conjg. - by rewrite (subsetP nH1U) // -mem_conjg (normsP nUW1b) ?mem_quotient. -have sUD := introT subsetP (dU _ _). -have Kphi w: 'ker (phi w) = 'C(H1 :^ w | 'Q). - rewrite !ker_comp ker_invm -kerE ker_restr_perm defH1 -cycleJ. - apply/setP=> x; rewrite !inE; congr (_ && _) => /=. - by apply: eq_subset_r => h1; rewrite !inE actpermK. -have o_phiU w: w \in W1bar -> #|phi w @* U| = a. - move=> Ww; have [w1 Nw1 Ww1 def_w] := morphimP Ww. - rewrite card_morphim Kphi (setIidPr _) ?sUD // /a indexgI /= !astabQ. - by rewrite centJ def_w morphpreJ // -{1}(normsP nUW1 w1 Ww1) indexJg. -have a_dv_p1: a %| p.-1. - rewrite -(o_phiU 1) // (dvdn_trans (cardSg (subsetT _))) // card_units_Zp //. - by rewrite conjg1 o_h (@totient_pfactor p 1) ?muln1. -have cycZhw w: cyclic (units_Zp #[h ^ w]). - rewrite -(injm_cyclic (inj_Zp_h w)) // im_Zp_unitm Aut_prime_cyclic //=. - by rewrite -orderE orderJ o_h. -have cyc_phi1U: cyclic (phi 1 @* U) := cyclicS (subsetT _) (cycZhw 1). -split=> //; last have{cyc_phi1U a_dv_p1} [z def_z] := cyclicP cyc_phi1U. - by rewrite -(conjsg1 H1) -Kphi (isog_cyclic (first_isog_loc _ _)) ?sUD. -have o_hw w: #[h ^ w] = #[h ^ 1] by rewrite !orderJ. -pose phi1 w x := eq_rect _ (fun m => {unit 'Z_m}) (phi w x) _ (o_hw w). -have val_phi1 w x: val (phi1 w x) = val (phi w x) :> nat. - by rewrite /phi1; case: _ / (o_hw _). -have mem_phi1 w x: w \in W1bar -> x \in U -> phi1 w x \in <[z]>%G. - move=> Ww Ux; have: #|<[z]>%G| = a by rewrite /= -def_z o_phiU. - rewrite /phi1; case: _ / (o_hw w) <[z]>%G => A oA /=. - suffices <-: phi w @* U = A by rewrite mem_morphim // dU. - by apply/eqP; rewrite (eq_subG_cyclic (cycZhw w)) ?subsetT // oA o_phiU. -have o_z: #[z] = a by rewrite orderE -def_z o_phiU. -pose phi0 w x := ecast m 'Z_m o_z (invm (injm_Zpm z) (phi1 w x)). -pose psi x := (\row_(i < q1) (phi0 (enum_val i) x * (phi0 1 x)^-1)%g)%R. -have psiM: {in U &, {morph psi: x y / x * y}}. - have phi0M w: w \in W1bar -> {in U &, {morph phi0 w: x y / x * y}}. - move=> Ww x y Ux Uy; rewrite /phi0; case: (a) / (o_z) => /=. - rewrite -morphM; first 1 [congr (invm _ _)] || by rewrite im_Zpm mem_phi1. - by rewrite /phi1; case: _ / (o_hw w); rewrite /= -morphM ?dU. - move=> x y Ux Uy; apply/rowP=> i; have /setD1P[_ Ww] := enum_valP i. - by rewrite !{1}mxE !{1}phi0M // addrCA -addrA -opprD addrCA addrA. -suffices Kpsi: 'ker (Morphism psiM) = C. - by exists [group of Morphism psiM @* U]; rewrite /Ubar -Kpsi first_isog. -apply/esym/eqP; rewrite eqEsubset; apply/andP; split. - rewrite [C]unlock -(bigdprodWY defHbar); apply/subsetP=> x /setIP[Ux cHx]. - suffices phi0x1 w: w \in W1bar -> phi0 w x = 1. - rewrite !inE Ux; apply/eqP/rowP=> i; have /setD1P[_ Ww] := enum_valP i. - by rewrite !mxE !phi0x1 ?mulgV. - move=> Ww; apply: val_inj; rewrite /phi0; case: (a) / (o_z); congr (val _). - suffices /eqP->: phi1 w x == 1 by rewrite morph1. - rewrite -2!val_eqE [val _]val_phi1 -(o_hw w) [phi _ _]mker // Kphi. - by apply: subsetP (astabS _ _) _ cHx; rewrite sub_gen // (bigcup_sup w). -have sKU: 'ker (Morphism psiM) \subset U by apply: subsetIl. -rewrite -quotient_sub1 -?(Frobenius_trivg_cent frobUW1c); last first. - by apply: subset_trans (normal_norm nsCUW1); rewrite subIset ?joing_subl. -rewrite subsetI quotientS //= quotient_cents2r // [C]unlock subsetI. -rewrite (subset_trans (commSg W1 sKU)) ?commg_subl //= astabQ gen_subG /=. -apply/subsetP=> _ /imset2P[x w1 Kx Ww1 ->]. -have:= Kx; rewrite -groupV 2!inE groupV => /andP[Ux /set1P/rowP psi_x'0]. -have [nH0x Ux'] := (subsetP nH0U x Ux, groupVr Ux); pose x'b := (inMb x)^-1. -rewrite mem_morphpre ?groupR ?morphR //= ?(subsetP nH0W1) //. -have conj_x'b w: w \in W1bar -> (h ^ w) ^ x'b = (h ^ w) ^+ val (phi 1 x^-1). - move=> Ww; transitivity (Zp_unitm (phi w x^-1) (h ^ w)). - have /morphpreP[_ /morphpreP[Px' Rx']] := dU w Ww x^-1 Ux'. - rewrite invmK ?restr_permE ?cycle_id //. - by rewrite actpermE qactJ groupV nH0x morphV. - have:= Ww; rewrite -(setD1K Wb1) autE ?cycle_id // => /setU1P[-> // | W'w]. - have /eqP := psi_x'0 (enum_rank_in W'w w); rewrite 2!mxE enum_rankK_in //. - rewrite -eq_mulgV1 -val_eqE /phi0; case: (a) / (o_z); rewrite /= val_eqE. - rewrite (inj_in_eq (injmP (injm_invm _))) /= ?im_Zpm ?mem_phi1 //. - by rewrite -2!val_eqE /= !val_phi1 // => /eqP->. -rewrite -sub_cent1 -(bigdprodWY defHbar) gen_subG; apply/bigcupsP=> w2 Ww2. -rewrite defH1 -cycleJ cycle_subG cent1C inE conjg_set1 !conjgM // conj_x'b //. -rewrite conjXg -!conjgM -conj_x'b ?groupM ?groupV ?mem_quotient //. -by rewrite !conjgM !conjgKV. -Qed. - -(* This is Peterfalvi (9.7)(b). *) -(* Note that part of this statement feeds directly into the final chapter of *) -(* the proof (PFsection14 and BGappendixC) and is not used before; we have *) -(* thus chosen to formulate the statement of (9.7)(b) accordingly. *) -(* For example, we supply separately the three component of the semi-direct *) -(* product isomorphism, because no use is made of the global isomorphism. We *) -(* also state explicitly that the image of W2bar is Fp because this is the *) -(* fact used in B & G, Appendix C, it is readily available during the proof, *) -(* whereas it can only be derived from the original statement of (9.7)(b) by *) -(* using Galois theory. Indeed the Galois part of the isomorphism is only *) -(* needed for this -- so with the formulation below it will not be used. *) -(* In order to avoid the use of the Wedderburn theorem on finite division *) -(* rings we build the field F from the enveloping algebra of the *) -(* representation of U rather than its endomorphism ring: then the fact that *) -(* Ubar is abelian yields commutativity directly. *) -Lemma typeP_Galois_P : - typeP_Galois -> - {F : finFieldType & {phi : {morphism Hbar >-> F} - & {psi : {morphism U >-> {unit F}} & {eta : {morphism W1 >-> {perm F}} - & forall alpha : {perm F}, reflect (rmorphism alpha) (alpha \in eta @* W1) - & [/\ 'injm eta, {in Hbar & W1, morph_act 'Q 'P phi eta} - & {in U & W1, forall x w, val (psi (x ^ w)) = eta w (val (psi x))}]} - & 'ker psi = C /\ {in Hbar & U, morph_act 'Q 'U phi psi}} - & [/\ #|F| = (p ^ q)%N, isom Hbar [set: F] phi & phi @* W2bar = <[1%R : F]>]} - & [/\ cyclic Ubar, coprime u p.-1 & u %| (p ^ q).-1 %/ p.-1]}. -Proof. -move=> irrU; have [_ sUW1M _ /joing_subP[nHU nHW1] _] := sdprod_context defHUW1. -have [nHbU nHbW1] := (quotient_norms H0 nHU, quotient_norms H0 nHW1). -have{sUW1M} /joing_subP[nH0U nH0W1] := subset_trans sUW1M nH0M. -have [ltCU oW2b oHb] := Ptype_Fcore_factor_facts. -pose rU := abelem_repr abelHbar ntHbar nHbU. -pose inHb := rVabelem abelHbar ntHbar; pose outHb := abelem_rV abelHbar ntHbar. -have{irrU} irrU: mx_irreducible rU by apply/abelem_mx_irrP; rewrite -acts_irrQ. -pose E_U := [pred A | (A \in enveloping_algebra_mx rU)%MS]. -have cEE A: A \in E_U -> centgmx rU A. - case/envelop_mxP=> z_ ->{A}; rewrite -memmx_cent_envelop linear_sum. - rewrite summx_sub // => x Ux; rewrite linearZ scalemx_sub {z_}//=. - rewrite memmx_cent_envelop; apply/centgmxP=> y Uy. - rewrite -repr_mxM // commgC 2?repr_mxM ?(groupR, groupM) // -/rU. - apply/row_matrixP=> i; rewrite row_mul; move: (row i _) => h. - have cHbH': (U / H0)^`(1) \subset 'C(Hbar). - by rewrite -quotient_der ?quotient_cents. - apply: rVabelem_inj; rewrite rVabelemJ ?groupR //. - by apply: (canLR (mulKg _)); rewrite -(centsP cHbH') ?mem_commg ?mem_rVabelem. -have{cEE} [F [outF [inF outFK inFK] E_F]]: - {F : finFieldType & {outF : {rmorphism F -> 'M(Hbar)%Mg} - & {inF : {additive _} | cancel outF inF & {in E_U, cancel inF outF}} - & forall a, outF a \in E_U}}%R. -- pose B := row_base (enveloping_algebra_mx rU). - have freeB: row_free B by apply: row_base_free. - pose outF := [additive of vec_mx \o mulmxr B]. - pose inF := [additive of mulmxr (pinvmx B) \o mxvec]. - have E_F a: outF a \in E_U by rewrite !inE vec_mxK mulmx_sub ?eq_row_base. - have inK: {in E_U, cancel inF outF}. - by move=> A E_A; rewrite /= mulmxKpV ?mxvecK ?eq_row_base. - have outI: injective outF := inj_comp (can_inj vec_mxK) (row_free_inj freeB). - have outK: cancel outF inF by move=> a; apply: outI; rewrite inK ?E_F. - pose one := inF 1%R; pose mul a b := inF (outF a * outF b)%R. - have outM: {morph outF: a b / mul a b >-> a * b}%R. - by move=> a b; rewrite inK //; apply: envelop_mxM; apply: E_F. - have out0: outF 0%R = 0%R by apply: raddf0. - have out1: outF one = 1%R by rewrite inK //; apply: envelop_mx1. - have nzFone: one != 0%R by rewrite -(inj_eq outI) out1 out0 oner_eq0. - have mulA: associative mul by move=> *; apply: outI; rewrite !{1}outM mulrA. - have mulC: commutative mul. - move=> a b; apply: outI; rewrite !{1}outM. - by apply: cent_mxP (E_F a); rewrite memmx_cent_envelop cEE ?E_F. - have mul1F: left_id one mul by move=> a; apply: outI; rewrite outM out1 mul1r. - have mulD: left_distributive mul +%R%R. - by move=> a1 a2 b; apply: canLR outK _; rewrite !raddfD mulrDl -!{1}outM. - pose Fring_NC := RingType 'rV__ (ComRingMixin mulA mulC mul1F mulD nzFone). - pose Fring := ComRingType Fring_NC mulC. - have outRM: multiplicative (outF : Fring -> _) by []. - have mulI (nza : {a | a != 0%R :> Fring}): GRing.rreg (val nza). - case: nza => a /=; rewrite -(inj_eq outI) out0 => nzA b1 b2 /(congr1 outF). - rewrite !{1}outM => /row_free_inj eqB12; apply/outI/eqB12. - by rewrite row_free_unit (mx_Schur irrU) ?cEE ?E_F. - pose inv (a : Fring) := oapp (fun nza => invF (mulI nza) one) a (insub a). - have inv0: (inv 0 = 0)%R by rewrite /inv insubF ?eqxx. - have mulV: GRing.Field.axiom inv. - by move=> a nz_a; rewrite /inv insubT /= (f_invF (mulI (exist _ _ _))). - pose Funit := FieldUnitMixin mulV inv0. - pose FringUcl := @GRing.ComUnitRing.Class _ (GRing.ComRing.class Fring) Funit. - have Ffield := @FieldMixin (GRing.ComUnitRing.Pack FringUcl nat) _ mulV inv0. - pose F := FieldType (IdomainType _ (FieldIdomainMixin Ffield)) Ffield. - by exists [finFieldType of F], (AddRMorphism outRM); first exists inF. -pose in_uF (a : F) : {unit F} := insubd (1 : {unit F}) a. -have in_uF_E a: a != 1 -> val (in_uF a) = a. - by move=> nt_a; rewrite insubdK /= ?unitfE. -have [psi psiK]: {psi : {morphism U >-> {unit F}} - | {in U, forall x, outF (val (psi x)) = rU (inMb x)}}. -- pose psi x := in_uF (inF (rU (inMb x))). - have psiK x: x \in U -> outF (val (psi x)) = rU (inMb x). - move/(mem_quotient H0)=> Ux; have EUx := envelop_mx_id rU Ux. - rewrite in_uF_E ?inFK //; apply: contraTneq (repr_mx_unitr rU Ux). - by move/(canRL_in inFK EUx)->; rewrite rmorph0 unitr0. - suffices psiM: {in U &, {morph psi: x y / x * y}} by exists (Morphism psiM). - move=> x y Ux Uy /=; apply/val_inj/(can_inj outFK); rewrite rmorphM //. - by rewrite !{1}psiK ?groupM // morphM ?(subsetP nH0U) ?repr_mxM ?mem_quotient. -have /trivgPn/sig2W[s W2s nts]: W2bar != 1%G. - by rewrite -cardG_gt1 oW2b prime_gt1. -pose sb := outHb s; have [Hs cW1s] := setIP W2s. -have nz_sb: sb != 0%R by rewrite morph_injm_eq1 ?abelem_rV_injm. -pose phi' a : coset_of H0 := inHb (sb *m outF a)%R. -have Hphi' a: phi' a \in Hbar by apply: mem_rVabelem. -have phi'D: {in setT &, {morph phi' : a b / a * b}}. - by move=> a b _ _; rewrite /phi' !raddfD [inHb _]morphM ?mem_im_abelem_rV. -have inj_phi': injective phi'. - move=> a b /rVabelem_inj eq_sab; apply: contraNeq nz_sb. - rewrite -[sb]mulmx1 idmxE -(rmorph1 outF) -subr_eq0 => /divff <-. - by rewrite rmorphM mulmxA !raddfB /= eq_sab subrr mul0mx. -have injm_phi': 'injm (Morphism phi'D) by apply/injmP; apply: in2W. -have Dphi: 'dom (invm injm_phi') = Hbar. - apply/setP=> h; apply/morphimP/idP=> [[a _ _ ->] // | Hh]. - have /cyclic_mxP[A E_A def_h]: (outHb h <= cyclic_mx rU sb)%MS. - by rewrite -(mxsimple_cyclic irrU) ?submx1. - by exists (inF A); rewrite ?inE //= /phi' inFK // -def_h [inHb _]abelem_rV_K. -have [phi [def_phi Kphi _ im_phi]] := domP _ Dphi. -have{Kphi} inj_phi: 'injm phi by rewrite Kphi injm_invm. -have{im_phi} im_phi: phi @* Hbar = setT by rewrite im_phi -Dphi im_invm. -have phiK: {in Hbar, cancel phi phi'} by rewrite def_phi -Dphi; apply: invmK. -have{def_phi Dphi injm_phi'} phi'K: cancel phi' phi. - by move=> a; rewrite def_phi /= invmE ?inE. -have phi'1: phi' 1%R = s by rewrite /phi' rmorph1 mulmx1 [inHb _]abelem_rV_K. -have phi_s: phi s = 1%R by rewrite -phi'1 phi'K. -have phiJ: {in Hbar & U, forall h x, phi (h ^ inMb x) = phi h * val (psi x)}%R. - move=> h x Hh Ux; have Uxb := mem_quotient H0 Ux. - apply: inj_phi'; rewrite phiK ?memJ_norm ?(subsetP nHbU) // /phi' rmorphM. - by rewrite psiK // mulmxA [inHb _]rVabelemJ // -/inHb [inHb _]phiK. -have Kpsi: 'ker psi = C. - apply/setP=> x; rewrite [C]unlock 2!in_setI /= astabQ; apply: andb_id2l => Ux. - have Ubx := mem_quotient H0 Ux; rewrite 3!inE (subsetP nH0U) //= inE. - apply/eqP/centP=> [psi_x1 h Hh | cHx]; last first. - by apply/val_inj; rewrite -[val _]mul1r -phi_s -phiJ // conjgE -cHx ?mulKg. - red; rewrite (conjgC h) -[h ^ _]phiK ?memJ_norm ?(subsetP nHbU) ?phiJ //. - by rewrite psi_x1 mulr1 phiK. -have etaP (w : subg_of W1): injective (fun a => phi (phi' a ^ inMb (val w))). - case: w => w /=/(mem_quotient H0)/(subsetP nHbW1) => nHw a b eq_ab. - apply/inj_phi'/(conjg_inj (inMb w)). - by apply: (injmP inj_phi) eq_ab; rewrite memJ_norm ?mem_rVabelem. -pose eta w : {perm F} := perm (etaP (subg W1 w)). -have etaK: {in Hbar & W1, forall h w, eta w (phi h) = phi (h ^ inMb w)}. - by move=> h w Hh Ww; rewrite /= permE subgK ?phiK. -have eta1 w: w \in W1 -> eta w 1%R = 1%R. - move=> Ww; rewrite -phi_s etaK //. - by rewrite conjgE (centP cW1s) ?mulKg ?mem_quotient. -have etaM: {in W1 &, {morph eta: w1 w2 / w1 * w2}}. - move=> w1 w2 Ww1 Ww2; apply/permP=> a; rewrite -[a]phi'K permM. - rewrite !etaK ?memJ_norm ?groupM ?(subsetP nHbW1) ?mem_quotient //. - by rewrite -conjgM -morphM ?(subsetP nH0W1). -have etaMpsi a: {in U & W1, forall x w, - eta w (a * val (psi x)) = eta w a * val (psi (x ^ w)%g)}%R. -- move=> x w Ux Ww; rewrite -[a]phi'K (etaK _ w (Hphi' a) Ww). - rewrite -!phiJ // ?memJ_norm ?(subsetP nHbW1, subsetP nUW1) ?mem_quotient //. - rewrite etaK ?memJ_norm ?(subsetP nHbU) ?mem_quotient // -!conjgM. - by rewrite conjgC -morphJ ?(subsetP nH0U x Ux, subsetP nH0W1 w Ww). -have psiJ: {in U & W1, forall x w, val (psi (x ^ w)) = eta w (val (psi x))}. - by move=> x w Ux Ww /=; rewrite -[val _]mul1r -(eta1 w Ww) -etaMpsi ?mul1r. -have etaRM w: w \in W1 -> rmorphism (eta w). - move=> Ww; have nUw := subsetP nHbW1 _ (mem_quotient _ Ww). - have etaD: additive (eta w). - move=> a b; rewrite -[a]phi'K -[b]phi'K -!zmodMgE -!zmodVgE. - rewrite -morphV // -morphM ?{1}etaK ?groupM ?groupV // conjMg conjVg. - by rewrite morphM 1?morphV ?groupV // memJ_norm. - do 2![split=> //] => [a b|]; last exact: eta1. - rewrite -[a]outFK; have /envelop_mxP[d ->] := E_F a. - rewrite raddf_sum mulr_suml ) mulr_suml. - apply: eq_bigr => _ /morphimP[x Nx Ux ->]; move: {d}(d _) => dx. - rewrite -[dx]natr_Zp scaler_nat !(mulrnAl, raddfMn); congr (_ *+ dx)%R. - by rewrite -psiK //= outFK mulrC etaMpsi // mulrC psiJ. -have oF: #|F| = (p ^ q)%N by rewrite -cardsT -im_phi card_injm. -pose nF := <[1%R : F]>; have o_nF: #|nF| = p. - by rewrite -orderE -phi_s (order_injm inj_phi) // (abelem_order_p abelHbar). -have cyc_uF := @field_unit_group_cyclic F. -exists F. - exists phi; last first. - split=> //; first exact/isomP; apply/esym/eqP; rewrite eqEcard o_nF -phi_s. - by rewrite (@cycle_subG F) mem_morphim //= card_injm ?subsetIl ?oW2b. - exists psi => //; last first. - by split=> // h x Hh Ux; rewrite qactJ (subsetP nH0U) ?phiJ. - have inj_eta: 'injm (Morphism etaM). - have /properP[_ [h Hh notW2h]]: W2bar \proper Hbar. - by rewrite properEcard subsetIl oW2b oHb (ltn_exp2l 1) prime_gt1. - apply/subsetP=> w /morphpreP[Ww /set1P/permP/(_ (phi h))]. - rewrite etaK // permE => /(injmP inj_phi) => chw. - rewrite -(@prime_TIg _ W1 <[w]>) //; first by rewrite inE Ww cycle_id. - rewrite proper_subn // properEneq cycle_subG Ww andbT. - apply: contraNneq notW2h => defW1; rewrite inE Hh /= -defW1. - rewrite quotient_cycle ?(subsetP nH0W1) // cent_cycle cent1C inE. - by rewrite conjg_set1 chw ?memJ_norm // (subsetP nHbW1) ?mem_quotient. - exists (Morphism etaM) => [alpha |]; last first. - by split=> // h w Hh Ww /=; rewrite qactJ (subsetP nH0W1) -?etaK. - pose autF (f : {perm F}) := rmorphism f. (* Bits of Galois theory... *) - have [r prim_r]: {r : F | forall f g, autF f -> autF g -> f r = g r -> f = g}. - have /cyclicP/sig_eqW[r def_uF] := cyc_uF [set: {unit F}]%G. - exists (val r) => f g fRM gRM eq_fgr; apply/permP=> a. - rewrite (_ : f =1 RMorphism fRM) // (_ : g =1 RMorphism gRM) //. - have [-> | /in_uF_E <-] := eqVneq a 0%R; first by rewrite !rmorph0. - have /cycleP[m ->]: in_uF a \in <[r]> by rewrite -def_uF inE. - by rewrite val_unitX !rmorphX /= eq_fgr. - have /sigW[P /and3P[Pr0 nP lePq]]: - exists P: {poly F}, [&& root P r, all (mem nF) P & #|root P| <= q]. - - pose Mr := (\matrix_(i < q.+1) (sb *m outF (r ^+ i)))%R. - have /rowV0Pn[v /sub_kermxP vMr0 nz_v]: kermx Mr != 0%R. - rewrite kermx_eq0 neq_ltn ltnS (leq_trans (rank_leq_col Mr)) //. - by rewrite (dim_abelemE abelHbar) // oHb pfactorK. - pose P : {poly F} := (\poly_(i < q.+1) (v 0 (inord i))%:R)%R. - have szP: size P <= q.+1 by apply: size_poly. - exists P; apply/and3P; split. - + apply/eqP/inj_phi'; congr (inHb _); rewrite rmorph0 mulmx0 -vMr0. - rewrite horner_poly !raddf_sum mulmx_sum_row; apply: eq_bigr => i _. - rewrite rowK inord_val //= mulr_natl rmorphMn -scaler_nat scalemxAr. - by rewrite natr_Zp. - + apply/(all_nthP 0%R)=> i /leq_trans/(_ szP) le_i_q. - by rewrite coef_poly /= le_i_q mem_cycle. - rewrite cardE -ltnS (leq_trans _ szP) //. - rewrite max_poly_roots ?enum_uniq //; last first. - by apply/allP=> r'; rewrite mem_enum. - apply: contraNneq nz_v => /polyP P0; apply/eqP/rowP=> i; apply/eqP. - have /eqP := P0 i; rewrite mxE coef0 coef_poly ltn_ord inord_val. - have charF: p \in [char F]%R by rewrite !inE p_pr -order_dvdn -o_nF /=. - by rewrite -(dvdn_charf charF) (dvdn_charf (char_Fp p_pr)) natr_Zp. - have{Pr0 nP} fPr0 f: autF f -> root P (f r). - move=> fRM; suff <-: map_poly (RMorphism fRM) P = P by apply: rmorph_root. - apply/polyP=> i; rewrite coef_map. - have [/(nth_default _)-> | lt_i_P] := leqP (size P) i; first exact: rmorph0. - by have /cycleP[n ->] := all_nthP 0%R nP i lt_i_P; apply: rmorph_nat. - apply: (iffP morphimP) => [[w _ Ww ->] | alphaRM]; first exact: etaRM. - suffices /setP/(_ (alpha r)): [set (eta w) r | w in W1] = [set t | root P t]. - rewrite inE fPr0 // => /imsetP[w Ww def_wr]; exists w => //. - by apply: prim_r => //; apply: etaRM. - apply/eqP; rewrite eqEcard; apply/andP; split. - by apply/subsetP=> _ /imsetP[w Ww ->]; rewrite inE fPr0 //; apply: etaRM. - rewrite (@cardsE F) card_in_imset // => w1 w2 Ww1 Ww2 /= /prim_r eq_w12. - by apply: (injmP inj_eta) => //; apply: eq_w12; apply: etaRM. -have isoUb: isog Ubar (psi @* U) by rewrite /Ubar -Kpsi first_isog. -pose unF := [set in_uF a | a in nF^#]. -have unF_E: {in nF^#, cancel in_uF val} by move=> a /setD1P[/in_uF_E]. -have unFg: group_set unF. - apply/group_setP; split=> [|_ _ /imsetP[a nFa ->] /imsetP[b nFb ->]]. - have nF1: 1%R \in nF^# by rewrite !inE cycle_id oner_eq0. - by apply/imsetP; exists 1%R => //; apply: val_inj; rewrite unF_E. - have nFab: (a * b)%R \in nF^#. - rewrite !inE mulf_eq0 negb_or. - have [[-> /cycleP[m ->]] [-> /cycleP[n ->]]] := (setD1P nFa, setD1P nFb). - by rewrite -natrM mem_cycle. - by apply/imsetP; exists (a * b)%R => //; apply: val_inj; rewrite /= !unF_E. -have <-: #|Group unFg| = p.-1. - by rewrite -o_nF (cardsD1 1 nF) group1 (card_in_imset (can_in_inj unF_E)). -have <-: #|[set: {unit F}]| = (p ^ q).-1. - rewrite -oF -(cardC1 1) cardsT card_sub; apply: eq_card => a /=. - by rewrite !inE unitfE. -rewrite /u (isog_cyclic isoUb) (card_isog isoUb) cyc_uF. -suffices co_u_p1: coprime #|psi @* U| #|Group unFg|. - by rewrite -(Gauss_dvdr _ co_u_p1) mulnC divnK ?cardSg ?subsetT. -rewrite -(cyclic_dprod (dprodEY _ _)) ?cyc_uF //. - by rewrite (sub_abelian_cent2 (cyclic_abelian (cyc_uF [set:_]%G))) ?subsetT. -apply/trivgP/subsetP=> _ /setIP[/morphimP[x Nx Ux ->] /imsetP[a nFa /eqP]]. -have nCx: x \in 'N(C) by rewrite -Kpsi (subsetP (ker_norm _)). -rewrite -val_eqE (unF_E a) //; case/setD1P: nFa => _ /cycleP[n {a}->]. -rewrite zmodXgE => /eqP def_psi_x; rewrite mker ?set11 // Kpsi coset_idr //. -apply/set1P; rewrite -set1gE -(Frobenius_trivg_cent frobUW1c) /= -/C. -rewrite inE mem_quotient //= -sub1set -quotient_set1 ?quotient_cents2r //. -rewrite gen_subG /= -/C -Kpsi; apply/subsetP=> _ /imset2P[_ w /set1P-> Ww ->]. -have Uxw: x ^ w \in U by rewrite memJ_norm ?(subsetP nUW1). -apply/kerP; rewrite (morphM, groupM) ?morphV ?groupV //. -apply/(canLR (mulKg _))/val_inj; rewrite psiJ // mulg1 def_psi_x. -exact: (rmorph_nat (RMorphism (etaRM w Ww))). -Qed. - -Local Open Scope ring_scope. - -Let redM := [predC irr M]. -Let mu_ := filter redM (S_ H0). - -(* This subproof is shared between (9.8)(b) and (9.9)(b). *) -Let nb_redM_H0 : size mu_ = p.-1 /\ {subset mu_ <= S_ H0C}. -Proof. -have pddM := FT_prDade_hypF maxM MtypeP; pose ptiWM := prDade_prTI pddM. -have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. -have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. -have nb_redM K: - K <| M -> K \subset HU -> K :&: H = H0 -> count redM (S_ K) = p.-1. -- move=> nsKM sKHU tiKHbar; have [sKM nKM] := andP nsKM; pose b L := (L / K)%G. - have [nsKHU [_ [_ sW2HU cycW2 _] _]] := (normalS sKHU sHUM nsKM, ptiWM). - have nKW2 := subset_trans sW2HU (normal_norm nsKHU). - have oW2b: #|b W2| = p. - have [_ <- _] := Ptype_Fcore_factor_facts; rewrite defW2bar. - rewrite !card_quotient ?(subset_trans (subset_trans sW2HU sHUM)) //. - by rewrite -indexgI -{2}(setIidPl sW2H) setIAC -setIA tiKHbar indexgI. - have{cycW2} cycW2b: cyclic (b W2) by apply: quotient_cyclic. - have ntW2b: (W2 / K != 1)%g by rewrite -cardG_gt1 oW2b prime_gt1. - have{ntW2b} [defWb ptiWMb]:= primeTIhyp_quotient ptiWM ntW2b sKHU nsKM. - pose muK j := (primeTIred ptiWMb j %% K)%CF. - apply/eqP; have <-: size (image muK (predC1 0)) = p.-1. - by rewrite size_map -cardE cardC1 card_Iirr_cyclic ?oW2b. - rewrite -size_filter -uniq_size_uniq ?filter_uniq ?seqInd_uniq // => [|phi]. - by apply/dinjectiveP=> j1 j2 _ _ /(can_inj (cfModK nsKM))/prTIred_inj. - rewrite mem_filter; apply/imageP/andP=> [[j nz_j ->] | [red_phi]]; last first. - case/seqIndP=> s /setDP[kerK ker'H] Dphi; rewrite !inE in kerK ker'H. - pose s1 := quo_Iirr K s; have Ds: s = mod_Iirr s1 by rewrite quo_IirrK. - rewrite {phi}Dphi Ds mod_IirrE ?cfIndMod // in kerK ker'H red_phi *. - have{red_phi} red_s1: 'Ind 'chi_s1 \notin irr (M / K) by rewrite -cfMod_irr. - have [[j Ds1] | [/idPn//]] := prTIres_irr_cases ptiWMb s1. - rewrite Ds1 cfInd_prTIres -/(muK j) in ker'H *; exists j => //. - by apply: contraNneq ker'H => ->; rewrite prTIres0 rmorph1 cfker_cfun1. - have red_j: redM (muK j) by rewrite /redM /= cfMod_irr // prTIred_not_irr. - have [s DmuKj]: exists s, muK j = 'Ind[M, HU] 'chi_s. - exists (mod_Iirr (primeTI_Ires ptiWMb j)). - by rewrite mod_IirrE // cfIndMod // cfInd_prTIres. - split=> //; apply/seqIndP; exists s; rewrite // !inE andbC. - rewrite -(@sub_cfker_Ind_irr _ M) ?gFnorm // -DmuKj cfker_mod //=. - have [[j1 Ds] | [/idPn]] := prTIres_irr_cases ptiWM s; last by rewrite -DmuKj. - rewrite Ds cfker_prTIres //; apply: contraNneq nz_j => j1_0. - apply/eqP/(prTIred_inj ptiWMb)/(can_inj (cfModK nsKM)); rewrite -{1}/(muK j). - by rewrite DmuKj Ds j1_0 -cfInd_prTIres !prTIres0 -cfIndMod ?rmorph1. -have [sH0HU sH0M] := (subset_trans sH0H sHHU, subset_trans sH0H (gFsub _ _)). -have sz_mu: size mu_ = p.-1. - by rewrite size_filter nb_redM ?(setIidPl sH0H) // /normal sH0M. -have s_muC_mu: {subset filter redM (S_ H0C) <= mu_}. - move=> phi; rewrite /= !mem_filter => /andP[->]; apply: seqIndS. - by rewrite setSD // Iirr_kerS ?joing_subl. -have UmuC: uniq (filter redM (S_ H0C)) by rewrite filter_uniq ?seqInd_uniq. -have [|Dmu _] := leq_size_perm UmuC s_muC_mu; last first. - by split=> // phi; rewrite -Dmu mem_filter => /andP[]. -have [nsH0C_M _ _ _] := nsH0xx_M. -have sCHU := subset_trans sCU sUHU; have sCM := subset_trans sCHU sHUM. -have sHOC_HU: H0C \subset HU by apply/joing_subP. -rewrite sz_mu size_filter nb_redM //= norm_joinEr ?(subset_trans sCM) //. -by rewrite -group_modl //= setIC [C]unlock setIA tiHU setI1g mulg1. -Qed. - -Let isIndHC (zeta : 'CF(M)) := - [/\ zeta 1%g = (q * u)%:R, zeta \in S_ H0C - & exists2 xi : 'CF(HC), xi \is a linear_char & zeta = 'Ind xi]. - -(* This is Peterfalvi (9.8). *) -Lemma typeP_nonGalois_characters (not_Galois : ~~ typeP_Galois) : - let a := #|U : 'C_U(sval (typeP_Galois_Pn not_Galois) | 'Q)| in - [/\ (*a*) {in X_ H0, forall s, (a %| 'chi_s 1%g)%C}, - (*b*) size mu_ = p.-1 /\ {in mu_, forall mu_j, isIndHC mu_j}, - (*c*) exists t, isIndHC 'chi_t - & (*d*) let irr_qa := [pred zeta in irr M | zeta 1%g == (q * a)%:R] in - let lb_n := (p.-1 * #|U|)%N in let lb_d := (a ^ 2 * #|U'|)%N in - (lb_d %| lb_n /\ lb_n %/ lb_d <= count irr_qa (S_ H0U'))%N]. -Proof. -case: (typeP_Galois_Pn _) => H1 [oH1 nH1U nH1Uq defHbar aP]; rewrite [sval _]/=. -move=> a; case: aP; rewrite -/a => a_gt1 a_dv_p1 cycUb1 isoUb. -set part_a := ({in _, _}); pose HCbar := (HC / H0)%G. -have [_ /mulG_sub[sHUM sW1M] nHUW1 tiHUW1] := sdprodP defM. -have [nsHHU _ /mulG_sub[sHHU sUHU] nHU tiHU] := sdprod_context defHU. -have [nH0H nHHU] := (normal_norm nsH0H, normal_norm nsHHU). -have sHHC: H \subset HC by rewrite joing_subl. -have [nH0HU sCHU] := (subset_trans sHUM nH0M, subset_trans sCU sUHU). -have nsH0_HU: H0 <| HU by rewrite /normal (subset_trans sH0H). -have nH0C := subset_trans sCHU nH0HU. -have [nsH0C_M nsHC_M nsH0U'_M _] := nsH0xx_M; have [sHC_M _] := andP nsHC_M. -have nsH0HC: H0 <| HC := normalS (subset_trans sH0H sHHC) sHC_M nsH0M. -have defHCbar: Hbar \x (C / H0) = HCbar. - rewrite /= quotientY // [C]unlock /= astabQ quotient_setIpre. - by rewrite dprodEY ?subsetIr // setIA -quotientGI // tiHU quotient1 setI1g. -have sHC_HU: HC \subset HU by rewrite join_subG sHHU. -have nsHC_HU: HC <| HU := normalS sHC_HU sHUM nsHC_M. -have defHb1 := defHbar; rewrite (big_setD1 1%g) ?group1 ?conjsg1 //= in defHb1. -have [[_ H1c _ defH1c] _ _ _] := dprodP defHb1; rewrite defH1c in defHb1. -have [nsH1H _] := dprod_normal2 defHb1; have [sH1H nH1H] := andP nsH1H. -have nHW1: W1 \subset 'N(H) := subset_trans sW1M (gFnorm _ _). -have nHbW1: W1bar \subset 'N(Hbar) by rewrite quotient_norms. -have sH1wH w: w \in W1bar -> H1 :^ w \subset Hbar. - by move/(normsP nHbW1) <-; rewrite conjSg. -have nsH1wHUb w: w \in W1bar -> H1 :^ w <| HU / H0. - move=> W1w; rewrite -(normsP (quotient_norms _ nHUW1) w W1w) normalJ. - rewrite /normal (subset_trans sH1H) ?quotientS //. - by rewrite -defHU sdprodE // quotientMl // mulG_subG nH1H. -have nH1wHUb := normal_norm (nsH1wHUb _ _). -have Part_a: part_a. - move=> s; rewrite !inE => /andP[kers'H kersH0]. - have [t sHt] := constt_cfRes_irr H s; pose theta := ('chi_t / H0)%CF. - have{kers'H} t_neq0: t != 0. - by rewrite -subGcfker (sub_cfker_constt_Res_irr sHt). - have{kersH0} kertH0: H0 \subset cfker 'chi_t. - by rewrite (sub_cfker_constt_Res_irr sHt). - have Ltheta: theta \is a linear_char. - by rewrite /theta -quo_IirrE // (char_abelianP _ _). - have Dtheta : _ = theta := cfBigdprod_Res_lin defHbar Ltheta. - set T := 'I_HU['chi_t]; have sHT: H \subset T by rewrite sub_Inertia. - have sTHU: T \subset HU by rewrite Inertia_sub. - suffices{s sHt} a_dv_iTHU: a %| #|HU : T|. - have [_ defInd_t _ imInd_t _] := cfInd_sum_Inertia t nsHHU. - have /imsetP[r tTr ->]: s \in Ind_Iirr HU @: irr_constt ('Ind[T] 'chi_t). - by rewrite imInd_t constt_Ind_Res. - by rewrite defInd_t ?cfInd1 // dvdC_mulr ?dvdC_nat // Cint_Cnat ?Cnat_irr1. - have /exists_inP[w W1w nt_t_w]: [exists w in W1bar, 'Res[H1 :^ w] theta != 1]. - rewrite -negb_forall_in; apply: contra t_neq0 => /forall_inP=> tH1w1. - rewrite -irr_eq1 -(cfQuoK nsH0H kertH0) -/theta -Dtheta. - rewrite [cfBigdprod _ _]big1 ?rmorph1 // => w /tH1w1/eqP->. - by rewrite /cfBigdprodi rmorph1. - have defT: H ><| (U :&: T) = T. - by rewrite (sdprod_modl defHU) // (setIidPr sTHU). - have /irrP[k Dk]: 'Res theta \in irr (H1 :^ w). - by rewrite lin_char_irr ?cfRes_lin_char. - rewrite -divgS // -(sdprod_card defHU) -(sdprod_card defT) divnMl // divgI. - rewrite -indexgI; have ->: a = #|U : 'C_U(H1 :^ w | 'Q)|. - have [w1 nH0w1 W1w1 ->] := morphimP W1w; rewrite astabQ centJ morphpreJ //. - by rewrite -astabQ indexgI -(normsP nUW1 _ W1w1) indexJg -indexgI. - rewrite indexgS ?setIS // sub_astabQ ?(subset_trans sTHU) //= -inertia_quo //. - apply: subset_trans (sub_inertia_Res _ (nH1wHUb w W1w)) _. - by rewrite Dk (inertia_irr_prime _ p_pr) ?subsetIr ?cardJg // -irr_eq1 -Dk. -pose isoJ := conj_isom H1; pose cfJ w i := 'chi_(isom_Iirr (isoJ w) i). -pose thetaH (f : {ffun _}) := cfBigdprod defHbar (fun w => cfJ w (f w)). -pose theta f := cfDprodl defHCbar (thetaH f). -have abH1: abelian H1 by rewrite cyclic_abelian ?prime_cyclic ?oH1. -have linH1 i: 'chi[H1]_i \is a linear_char by apply/char_abelianP. -have lin_thetaH f: thetaH f \is a linear_char. - by apply: cfBigdprod_lin_char => w _; rewrite /cfJ isom_IirrE cfIsom_lin_char. -have nz_thetaH f: thetaH f 1%g != 0 by rewrite lin_char_neq0. -have Dtheta f: {in W1bar & H1, forall w xb, theta f (xb ^ w) = 'chi_(f w) xb}. - move=> w xb W1w H1xb /=; have sHHCb := quotientS H0 sHHC. - transitivity ('Res[H1 :^ w] ('Res[Hbar] (theta f)) (xb ^ w)); last first. - by rewrite cfDprodlK cfBigdprodKabelian // isom_IirrE cfIsomE. - by rewrite cfResRes ?sH1wH // cfResE ?memJ_conjg ?(subset_trans (sH1wH w _)). -have lin_theta f: theta f \is a linear_char by rewrite cfDprodl_lin_char. -pose Ftheta := pffun_on (0 : Iirr H1) W1bar (predC1 0). -have inj_theta: {in Ftheta &, injective theta}. - move=> f1 f2 /pffun_onP[/supportP W1f1 _] /pffun_onP[/supportP W1f2 _] eq_f12. - apply/ffunP=> w. - have [W1w | W1'w] := boolP (w \in W1bar); last by rewrite W1f1 ?W1f2. - by apply/irr_inj/cfun_inP=> x H1x; rewrite -!Dtheta ?eq_f12. -have irr_thetaH0 f: (theta f %% H0)%CF \in irr HC. - by rewrite cfMod_irr ?lin_char_irr. -have def_Itheta f: f \in Ftheta -> 'I_HU[theta f %% H0]%CF = HC. - case/pffun_onP=> _ nz_fW1; apply/eqP; rewrite eqEsubset sub_Inertia //. - rewrite inertia_mod_pre //= -{1}(sdprodW defHU) -group_modl; last first. - rewrite (subset_trans sHHC) // -sub_quotient_pre ?normal_norm //. - by rewrite sub_Inertia ?quotientS. - rewrite -gen_subG genM_join genS ?setUS //= {2}[C]unlock setIS //= astabQ. - rewrite morphpreS // centsC -{1}(bigdprodWY defHbar) gen_subG. - apply/bigcupsP=> w W1w; rewrite centsC. - apply: subset_trans (sub_inertia_Res _ (quotient_norms _ nHHU)) _. - rewrite cfDprodlK inertia_bigdprod_irr // subIset // orbC (bigcap_min w) //. - rewrite (inertia_irr_prime _ p_pr) ?cardJg ?subsetIr // isom_Iirr_eq0. - by apply: nz_fW1; apply: image_f. -have irrXtheta f: f \in Ftheta -> 'Ind (theta f %% H0)%CF \in irr HU. - move/def_Itheta; rewrite -(cfIirrE (irr_thetaH0 f)) => I_f_HC. - by rewrite inertia_Ind_irr ?I_f_HC //. -pose Mtheta := [set cfIirr (theta f %% H0)%CF | f in Ftheta]. -pose Xtheta := [set cfIirr ('Ind[HU] 'chi_t) | t in Mtheta]. -have oXtheta: (u * #|Xtheta| = p.-1 ^ q)%N. - transitivity #|Ftheta|; last first. - rewrite card_pffun_on cardC1 card_Iirr_abelian // oH1. - rewrite -(card_isog (quotient_isog _ _)) ?oW1 ?(subset_trans sW1M) //. - by apply/trivgP; rewrite -tiHUW1 setSI ?(subset_trans sH0H). - rewrite Du -card_imset_Ind_irr ?card_in_imset //. - - move=> f1 f2 Df1 Df2 /(congr1 (tnth (irr HC))); rewrite !{1}cfIirrE //. - by move/(can_inj (cfModK nsH0HC)); apply: inj_theta. - - by move=> _ /imsetP[f Df ->]; rewrite cfIirrE ?irrXtheta. - move=> _ y /imsetP[f /familyP Ff ->] HUy; apply/imsetP. - pose yb := inMb y; have HUyb: yb \in (HU / H0)%g by apply: mem_quotient. - have nHb_y: inMb y \in 'N(Hbar) by rewrite (subsetP (quotient_norms _ nHHU)). - have nH1b_y := subsetP (nH1wHUb _ _) yb HUyb. - exists [ffun w => conjg_Iirr (f w) (inMb y ^ w^-1)]. - apply/familyP=> w; rewrite ffunE. - by case: ifP (Ff w) => _; rewrite !inE conjg_Iirr_eq0. - apply: irr_inj; rewrite !(cfIirrE, conjg_IirrE) // (cfConjgMod _ nsHC_HU) //. - rewrite cfConjgDprodl //; first congr (cfDprodl _ _ %% H0)%CF; last first. - rewrite /= -quotientYidl // (subsetP _ _ HUyb) ?quotient_norms //. - by rewrite (subset_trans sHUM) ?normal_norm. - rewrite cfConjgBigdprod //; apply: eq_bigr => w W1w; congr (cfBigdprodi _ _). - rewrite ffunE /cfJ !isom_IirrE conjg_IirrE. - apply/cfun_inP=> _ /imsetP[x Hx ->]; rewrite cfIsomE // cfConjgE ?nH1b_y //. - rewrite -conjgM conjgCV conjVg conjgM cfIsomE //; last first. - by rewrite -mem_conjg (normP _) // -mem_conjg -normJ ?nH1b_y. - by rewrite cfConjgE // -mem_conjg -normJ ?nH1b_y. -have sXthXH0C: Xtheta \subset X_ H0C. - apply/subsetP=> _ /imsetP[t Mt ->]; have{Mt} [f Ff Dt] := imsetP Mt. - rewrite !inE cfIirrE; last by rewrite Dt cfIirrE ?irrXtheta. - rewrite !sub_cfker_Ind_irr ?(subset_trans sHUM) ?normal_norm ?gFnormal //. - rewrite {t}Dt cfIirrE // join_subG andbCA {1}cfker_mod //. - rewrite !{1}sub_cfker_mod //= andbC {1}cfker_sdprod /=. - apply: contraL (familyP Ff 1%g) => kerHb; rewrite group1 negbK. - have:= sub_cfker_Res (subxx _) kerHb; rewrite cfDprodlK. - move/(subset_trans (sH1wH _ (group1 _)))/(sub_cfker_Res (subxx _)). - rewrite cfBigdprodKabelian // isom_IirrE cfker_isom morphim_conj /=. - by rewrite !conjsg1 subsetIidl subGcfker. -pose mu_f (i : Iirr H1) := [ffun w => if w \in W1bar then i else 0]. -have Fmu_f (i : Iirr H1): i != 0 -> mu_f i \in Ftheta. - by move=> nz_i; apply/familyP=> w; rewrite ffunE; case: ifP; rewrite !inE. -pose mk_mu i := 'Ind[HU] (theta (mu_f i) %% H0)%CF. -have sW1_Imu i: W1 \subset 'I[theta (mu_f i) %% H0]%CF. - apply/subsetP=> w W1w; have Mw := subsetP sW1M w W1w. - have nHC_W1 := subset_trans sW1M (normal_norm nsHC_M). - rewrite inE (subsetP nHC_W1) ?(cfConjgMod _ nsHC_M) //; apply/eqP. - have W1wb: inMb w \in W1bar by rewrite mem_quotient. - rewrite cfConjgDprodl ?(subsetP _ _ W1wb) ?quotient_norms //; last first. - by rewrite (subset_trans (joing_subr U W1)) ?normal_norm. - congr (cfDprodl _ _ %% H0)%CF. - apply/cfun_inP=> _ /(mem_bigdprod defHbar)[x [H1x -> _]]. - have Hx w1: w1 \in W1bar -> x w1 \in Hbar. - by move=> W1w1; rewrite (subsetP (sH1wH w1 _)) ?H1x. - rewrite !lin_char_prod ?cfConjg_lin_char //; apply/eq_bigr=> w1 W1w1. - rewrite cfConjgE ?(subsetP nHbW1) //. - have W1w1w: (w1 * (inMb w)^-1)%g \in W1bar by rewrite !in_group. - rewrite -(cfResE _ (sH1wH _ W1w1w)) -?mem_conjg -?conjsgM ?mulgKV ?H1x //. - rewrite -(cfResE _ (sH1wH _ W1w1)) ?H1x ?cfBigdprodKabelian //. - rewrite !ffunE W1w1 W1w1w -[x w1](conjgKV w1) -conjgM !isom_IirrE. - by rewrite !cfIsomE -?mem_conjg ?H1x. -have inj_mu: {in predC1 0 &, injective (fun i => cfIirr (mk_mu i))}. - move=> i1 i2 nz_i1 nz_i2 /(congr1 (tnth (irr HU))). - rewrite !{1}cfIirrE ?irrXtheta ?Fmu_f // /mk_mu. - do 2![move/esym; rewrite -{1}(cfIirrE (irr_thetaH0 _))]. - move/(cfclass_Ind_irrP _ _ nsHC_HU); rewrite !{1}cfIirrE //. - case/cfclassP=> _ /(mem_sdprod defHU)[x [y [Hx Uy -> _]]]. - rewrite (cfConjgM _ nsHC_HU) ?(subsetP sHHU x) ?(subsetP sUHU) //. - rewrite {x Hx}(cfConjg_id _ (subsetP sHHC x Hx)) => Dth1. - suffices /setIP[_ /inertiaJ]: y \in 'I_HU[theta (mu_f i2) %% H0]%CF. - rewrite -Dth1 => /(can_inj (cfModK nsH0HC))/inj_theta/ffunP/(_ 1%g). - by rewrite !ffunE group1 => -> //; apply: Fmu_f. - rewrite def_Itheta ?Fmu_f //= (subsetP (joing_subr _ _)) //. - have nCy: y \in 'N(C). - by rewrite (subsetP (normal_norm nsCUW1)) ?mem_gen ?inE ?Uy. - have [_ _ /trivgPn[wb W1wb ntwb] _ _] := Frobenius_context frobUW1c. - have /morphimP[w nCw W1w Dw] := W1wb; have Mw := subsetP sW1M w W1w. - rewrite coset_idr //; apply/set1P; rewrite -set1gE; apply: wlog_neg => nty. - rewrite -((Frobenius_reg_ker frobUW1c) wb); last by rewrite !inE ntwb. - rewrite inE mem_quotient //=; apply/cent1P/commgP. - rewrite Dw -morphR //= coset_id //. - suffices: [~ y, w] \in U :&: HC. - rewrite /= norm_joinEr ?(subset_trans sCU) // -group_modr ?subsetIl //=. - by rewrite setIC tiHU mul1g. - have Uyw: [~ y, w] \in U; last rewrite inE Uyw. - by rewrite {1}commgEl groupMl ?groupV // memJ_norm ?(subsetP nUW1) // Uy. - rewrite -(def_Itheta _ (Fmu_f _ nz_i1)) 2!inE /= andbA -in_setI. - rewrite (setIidPl (normal_norm nsHC_HU)) (subsetP sUHU) //=. - rewrite Dth1 -(cfConjgM _ nsHC_HU) ?(subsetP sUHU) //. - have My: y \in M := subsetP (subset_trans sUHU sHUM) y Uy. - rewrite mulKVg (cfConjgM _ nsHC_M) ?in_group //. - have /inertiaJ-> := subsetP (sW1_Imu i2) _ (groupVr W1w). - rewrite (cfConjgM _ nsHC_M) // -Dth1. - by have /inertiaJ-> := subsetP (sW1_Imu i1) w W1w. -pose Xmu := [set cfIirr (mk_mu i) | i in predC1 0]. -have def_IXmu: {in Xmu, forall s, 'I_M['chi_s] = M}. - move=> _ /imsetP[i nz_i ->]; apply/setIidPl. - rewrite -subsetIidl -{1}(sdprodW defM) mulG_subG sub_Inertia //. - rewrite !cfIirrE ?irrXtheta ?Fmu_f //=. - apply: subset_trans (sub_inertia_Ind _ (der_norm 1 M)). - by rewrite subsetI sW1M /=. -pose Smu := [seq 'Ind[M] 'chi_s | s in Xmu]. -have sSmu_mu: {subset Smu <= mu_}. - move=> _ /imageP[s Xmu_s ->]; rewrite mem_filter /=. - rewrite irrEchar cfnorm_Ind_irr ?gFnormal // def_IXmu //. - rewrite -(index_sdprod defM) (eqC_nat _ 1) gtn_eqF ?prime_gt1 // andbF. - rewrite mem_seqInd ?gFnormal /normal ?(subset_trans sH0H) ?gFsub //=. - suffices /(subsetP sXthXH0C): s \in Xtheta. - by apply: subsetP; rewrite setSD // Iirr_kerS ?joing_subl. - have /imsetP[i nz_i ->] := Xmu_s; rewrite /Xtheta -imset_comp. - by apply/imsetP; exists (mu_f i); rewrite /= ?cfIirrE ?Fmu_f. -have ResIndXmu: {in Xmu, forall s, 'Res ('Ind[M] 'chi_s) = q%:R *: 'chi_s}. - move=> s /def_IXmu Imu_s; rewrite cfResInd_sum_cfclass ?gFnormal ?Imu_s //. - by rewrite -(index_sdprod defM) -Imu_s cfclass_inertia big_seq1. -have uSmu: uniq Smu. - apply/dinjectiveP=> s1 s2 Xs1 Xs2 /(congr1 'Res[HU]); rewrite !ResIndXmu //. - by move/(can_inj (scalerK (neq0CG W1)))/irr_inj. -have sz_Smu: size Smu = p.-1. - by rewrite size_map -cardE card_in_imset // cardC1 card_Iirr_abelian ?oH1. -have [sz_mu s_mu_H0C] := nb_redM_H0. -have Dmu: Smu =i mu_. - by have [|//] := leq_size_perm uSmu sSmu_mu; rewrite sz_mu sz_Smu. -split=> {Part_a part_a}//. -- split=> // phi mu_phi; have S_HOC_phi := s_mu_H0C _ mu_phi. - move: mu_phi; rewrite -Dmu => /imageP[_ /imsetP[i nz_i ->]]. - rewrite cfIirrE ?irrXtheta ?Fmu_f // => Dphi. - split=> //; rewrite Dphi ?cfInd1 ?cfIndInd //. - rewrite -(index_sdprod defM) -/q -Du mulrA -natrM. - by rewrite lin_char1 1?cfMod_lin_char ?mulr1. - by exists (theta (mu_f i) %% H0)%CF; rewrite 1?cfMod_lin_char. -- have /eqVproper: Xmu \subset Xtheta. - apply/subsetP=> _ /imsetP[i nz_i ->]; rewrite -[Xtheta]imset_comp /=. - by apply/imsetP; exists (mu_f i); rewrite /= ?cfIirrE ?Fmu_f. - case=> [defXmu | /andP[_ /subsetPn[s theta_s Xmu'_s]]]; last first. - have [_ /imsetP[f Dth_f ->] Ds] := imsetP theta_s; rewrite cfIirrE // in Ds. - have /irrP[t Dt]: 'Ind 'chi_s \in irr M; last 1 [exists t; rewrite -{t}Dt]. - apply: contraR Xmu'_s => red_Ind_s. - have: 'Ind 'chi_s \in mu_. - rewrite mem_filter /= red_Ind_s mem_seqInd ?gFnormal //=. - apply: subsetP theta_s; rewrite (subset_trans sXthXH0C) ?setSD //. - by rewrite Iirr_kerS ?joing_subl. - rewrite -Dmu => /imageP[s1 Xmu_s1] /(congr1 (cfdot ('Ind 'chi_s1)))/eqP. - rewrite cfnorm_Ind_irr ?gFnormal // eq_sym -cfdot_Res_l. - rewrite ResIndXmu // cfdotZl cfdot_irr -natrM mulnC. - by case: (s1 =P s) => [<- // | _] /idPn[]; apply: neq0CiG. - split; first 2 [by rewrite mem_seqInd ?gFnormal ?(subsetP sXthXH0C)]. - rewrite Ds cfIirrE ?irrXtheta ?cfInd1 // -Du -(index_sdprod defM) -/q. - by rewrite mulrA -natrM lin_char1 ?cfMod_lin_char ?mulr1. - exists (theta f %% H0)%CF; first by rewrite cfMod_lin_char. - by rewrite Ds cfIirrE ?irrXtheta //= cfIndInd. - suffices /(congr1 odd): u = (p.-1 ^ q.-1)%N. - rewrite odd_exp -(subnKC (prime_gt1 pr_q)) /= -subn1 odd_sub ?prime_gt0 //. - by rewrite -oH1 (oddSg sH1H) ?quotient_odd // mFT_odd. - have p1_gt0: (0 < p.-1)%N by rewrite -(subnKC (prime_gt1 p_pr)). - apply/eqP; rewrite -(eqn_pmul2r p1_gt0) -expnSr prednK ?prime_gt0 //. - by rewrite -oXtheta -defXmu card_in_imset // cardC1 card_Iirr_abelian ?oH1. -clear Xmu def_IXmu Smu sSmu_mu ResIndXmu uSmu sz_Smu sz_mu s_mu_H0C Dmu. -clear Mtheta Xtheta irrXtheta oXtheta sXthXH0C mu_f Fmu_f mk_mu sW1_Imu inj_mu. -clear nz_thetaH lin_thetaH lin_theta Ftheta inj_theta irr_thetaH0 def_Itheta. -clear theta Dtheta => irr_qa lb_n lb_d. -have sU'U: U' \subset U := der_sub 1 U. -have nH0U := subset_trans sUHU nH0HU; have nH0U' := subset_trans sU'U nH0U. -have sU'CH1: U' \subset 'C_U(H1 | 'Q). - by rewrite subsetI sU'U sub_astabQ nH0U' (centsS sH1H) ?quotient_cents. -have sCH1_U: 'C_U(H1 | 'Q) \subset U := subsetIl U _. -have dvd_lb: lb_d %| lb_n. - rewrite -[lb_d]mulnA dvdn_mul // -(Lagrange sCH1_U). - by rewrite mulnC dvdn_pmul2r ?cardSg ?indexg_gt0. -split; rewrite ?leq_divLR // /lb_n -(Lagrange sCH1_U) -/a -(Lagrange sU'CH1). -rewrite mulnCA -mulnA mulnC !mulnA !leq_pmul2r ?cardG_gt0 ?indexg_gt0 // mulnC. -pose H1CH1 := (H1 <*> 'C_(U / H0)(H1))%G; pose HCH1 := (H <*> 'C_U(H1 | 'Q))%G. -have defH1CH1: H1 \x 'C_(U / H0)(H1) = H1CH1. - rewrite dprodEY ?subsetIr ?coprime_TIg ?(coprimeSg sH1H) //. - by rewrite (coprimegS (subsetIl _ _)) ?coprime_morph. -have sHCH1_HU: HCH1 \subset HU by rewrite join_subG sHHU (subset_trans sCH1_U). -have nsHCH1_HU: HCH1 <| HU. - rewrite /normal sHCH1_HU -(sdprodW defHU) mulG_subG normsG ?joing_subl //=. - by rewrite normsY // sub_der1_norm. -have nsH0_HCH1: H0 <| HCH1. - by rewrite (normalS _ sHCH1_HU) // (subset_trans sH0H) ?joing_subl. -have nsH1cHU: H1c <| HU / H0. - rewrite -(bigdprodWY defH1c) /normal gen_subG norms_gen ?andbT //. - by apply/bigcupsP=> w /setD1P[_ /nsH1wHUb/andP[]]. - by apply/norms_bigcup/bigcapsP=> w /setD1P[_ /nH1wHUb]. -have defHCH1: H1c ><| H1CH1 = (HCH1 / H0)%G. - have /sdprodP[_ /mulG_sub[sH1cH _] nH1cH1 tiH1cH1] := dprodWsdC defHb1. - rewrite sdprodE /= -(dprodW defH1CH1). - - rewrite mulgA (dprodWC defHb1) -morphim_setIpre -astabQ -quotientMl //. - by rewrite norm_joinEr // (subset_trans sCH1_U). - - rewrite mul_subG ?subIset // (subset_trans (quotientS _ sUHU)) //. - exact: normal_norm nsH1cHU. - rewrite -(setIidPl sH1cH) setIAC -setIA -group_modl // coprime_TIg ?mulg1 //. - by rewrite coprime_sym (coprimegS (subsetIl _ _)) ?coprime_morph. -have [nsH1cHCH1 sH1CH1_HCH1 _ nH1cH1C _] := sdprod_context defHCH1. -pose Clam := ('C_(U / H0)(H1) / (U' / H0))%G. -pose lam (j : Iirr Clam) := 'chi_(mod_Iirr j). -pose theta i j := cfSdprod defHCH1 (cfDprod defH1CH1 'chi_i (lam j)). -have nsU'CH1: U' <| 'C_U(H1 | 'Q) by rewrite (normalS _ sCH1_U) ?gFnormal. -have nsU'CH1b: U' / H0 <| 'C_(U / H0)(H1). - by rewrite -morphim_setIpre -astabQ quotient_normal. -have abClam: abelian Clam. - by rewrite sub_der1_abelian //= quotient_der ?dergS ?subsetIl. -have lam_lin j: lam j \is a linear_char. - by rewrite /lam mod_IirrE ?cfMod_lin_char //; apply/char_abelianP. -have theta_lin i j: theta i j \is a linear_char. - by rewrite cfSdprod_lin_char ?cfDprod_lin_char. -have <-: #|Clam| = #|'C_U(H1 | 'Q) : U'|. - rewrite -card_quotient ?normal_norm //= /= -morphim_setIpre -astabQ. - have nsU'U : U' <| U by apply: der_normal. - rewrite -(restrmEsub _ _ sCH1_U) -(restrm_quotientE _ sU'U) -morphim_quotm. - rewrite card_injm ?quotientS ?injm_quotm ?(isom_inj (quotient_isom _ _)) //. - by rewrite coprime_TIg ?(coprimeSg sH0H). -pose Mtheta := [set mod_Iirr (cfIirr (theta i j)) | i in [set~ 0], j in setT]. -have ->: (p.-1 * #|Clam|)%N = #|Mtheta|. - rewrite [Mtheta]curry_imset2X card_imset ?cardsX => [|[i1 j1] [i2 j2] /=/eqP]. - by rewrite cardsC1 cardsT !card_Iirr_abelian ?(abelianS sH1H) ?oH1. - rewrite (can_eq (mod_IirrK _)) // -(inj_eq irr_inj) !cfIirrE ?lin_char_irr //. - rewrite (can_eq (cfSdprodK _)) -!dprod_IirrE (inj_eq irr_inj). - by rewrite (can_eq (dprod_IirrK _)) => /eqP[->] /(can_inj (mod_IirrK _))->. -have{lam_lin} thetaH1 i j: 'Res[H1] (theta i j) = 'chi_i. - rewrite -(cfResRes _ _ sH1CH1_HCH1) ?joing_subl // cfSdprodK cfDprodKl //. - exact: lin_char1. -have Itheta r: r \in Mtheta -> 'I_HU['chi_r]%CF = HCH1. - case/imset2P=> i j; rewrite /= in_setC1 => nz_i _ Dr; apply/eqP. - rewrite eqEsubset sub_Inertia //= Dr mod_IirrE // cfIirrE ?lin_char_irr //. - rewrite andbT -(quotientSGK _ (normal_sub nsH0_HCH1)) ?subIset ?nH0HU //. - rewrite inertia_mod_quo //. - apply: subset_trans (sub_inertia_Res _ (nH1wHUb _ (group1 _))) _. - rewrite /= conjsg1 thetaH1 (inertia_irr_prime _ p_pr) //. - rewrite -quotient_setIpre -astabQ quotientS // -{1}(sdprodW defHU). - by rewrite -genM_join sub_gen // group_modl // sub_astabQ nH0H (centsS sH1H). -have irr_Xtheta: {in Mtheta, forall r, 'Ind[HU] 'chi_r \in irr HU}. - by move=> r Mr; rewrite /= inertia_Ind_irr ?Itheta. -pose Xtheta := [set cfIirr ('Ind[HU] 'chi_r) | r in Mtheta]. -have Da: a = #|HU : HCH1| by rewrite -(index_sdprodr defHU). -have Xtheta_1: {in Xtheta, forall s, 'chi_s 1%g = a%:R}. - move=> _ /imsetP[r Mr ->]; have /imset2P[i j _ _ Dr] := Mr. - rewrite cfIirrE ?irr_Xtheta ?cfInd1 //= -Da lin_char1 ?mulr1 //. - by rewrite Dr mod_IirrE ?cfMod_lin_char // cfIirrE ?lin_char_irr. -have nsH0U'HU: H0U' <| HU. - by apply: normalS nsH0U'_M; rewrite // -(sdprodWY defHU) genS ?setUSS. -have sXthetaXH0U': Xtheta \subset X_ H0U'. - apply/subsetP=> _ /imsetP[r Mr ->]; have [i j nz_i _ Dr] := imset2P Mr. - rewrite !inE cfIirrE ?irr_Xtheta ?sub_cfker_Ind_irr //= ?normal_norm //. - rewrite Dr mod_IirrE // cfIirrE ?lin_char_irr // join_subG andbCA. - rewrite {1}cfker_mod //= !{1}sub_cfker_mod //; apply/andP; split; last first. - rewrite -(sdprodWY (sdprod_cfker _ _)) sub_gen ?subsetU // orbC. - rewrite (subset_trans _ (cfker_dprod _ _ _)) // sub_gen ?subsetU // orbC. - by rewrite /lam mod_IirrE ?cfker_mod. - apply: contraL nz_i => /(subset_trans sH1H); rewrite !inE negbK. - by move/(sub_cfker_Res (subxx _)); rewrite thetaH1 subGcfker. -have nsCH1_U: 'C_U(H1 | 'Q) <| U by rewrite sub_der1_normal. -have nH1cU: (U / H0)%g \subset 'N(H1c). - rewrite -(bigdprodWY defH1c) norms_gen ?norms_bigcup //. - apply/bigcapsP=> w /setD1P[_ W1w]. - by rewrite normJ -sub_conjgV (normsP (quotient_norms H0 nUW1)) ?groupV. -have ->: #|Mtheta| = (#|Xtheta| * a)%N. - rewrite Da mulnC -card_imset_Ind_irr // => _ xy /imset2P[i j nz_i _ ->]. - case/(mem_sdprod defHU)=> x [y [Hx Uy -> _]]; have HUy := subsetP sUHU y Uy. - pose yb := inMb y; have Uyb: yb \in (U / H0)%g by rewrite mem_quotient. - pose iy := conjg_Iirr i yb; pose jy := conjg_Iirr j (coset (U' / H0)%g yb). - apply/imset2P; exists iy jy; rewrite !inE ?conjg_Iirr_eq0 // in nz_i *. - apply: irr_inj; have HCH1x: x \in HCH1 by rewrite mem_gen ?inE ?Hx. - rewrite conjg_IirrE (cfConjgM _ nsHCH1_HU) ?(subsetP sHHU x) {Hx}//. - rewrite {x HCH1x}(cfConjg_id _ HCH1x) !{1}mod_IirrE //. - rewrite !{1}cfIirrE ?lin_char_irr //. - rewrite cfConjgMod_norm ?(subsetP nH0U) ?(subsetP (normal_norm nsHCH1_HU)) //. - have nCH1_Ub: (U / H0)%g \subset 'N('C_(U / H0)(H1)). - by rewrite normsI ?normG ?norms_cent. - rewrite cfConjgSdprod ?cfConjgDprod ?(subsetP _ _ Uyb) ?normsY //. - rewrite /theta /lam !{1}mod_IirrE // !{1}conjg_IirrE. - by rewrite cfConjgMod_norm ?(subsetP _ _ Uyb) // quotient_norms ?gFnorm. -rewrite leq_pmul2r ?indexg_gt0 // cardE -(size_map (fun s => 'Ind[M] 'chi_s)). -have kerH1c s: s \in Xtheta -> H1c \subset (cfker 'chi_s / H0)%g. - case/imsetP=> r Mr {s}->; have [i j _ _ Dr] := imset2P Mr. - rewrite -(setIidPr (normal_sub nsH1cHCH1)) -morphim_setIpre quotientS //. - rewrite cfIirrE ?irr_Xtheta ?sub_cfker_Ind_irr //; last first. - by rewrite normsI ?normal_norm // -(quotientGK nsH0_HU) cosetpre_normal. - rewrite Dr mod_IirrE // cfker_morph ?normal_norm // cfIirrE ?lin_char_irr //. - by rewrite setIS ?joing_subl ?morphpreS // cfker_sdprod. -have injXtheta: - {in M & Xtheta &, forall w s1 s2, 'chi_s1 = 'chi_s2 ^ w -> w \in HU}%CF. -- move=> _ s1 s2 /(mem_sdprod defM)[y [w [HUy W1w -> _]]] Xs1 Xs2. - rewrite groupMl // cfConjgMnorm ?(subsetP (normG _) y) ?(subsetP nHUW1) //. - rewrite {y HUy}(cfConjg_id _ HUy) => Ds1. - have nH0w: w \in 'N(H0) by rewrite ?(subsetP nH0M) ?(subsetP sW1M). - rewrite (subsetP (normal_sub nsH0_HU)) // coset_idr //. - have /setDP[]:= subsetP sXthetaXH0U' s1 Xs1; rewrite !inE join_subG /=. - case/andP=> kerH0s1 _; apply: contraNeq; rewrite -eq_invg1 => ntw. - rewrite -(quotientSGK nH0H) // -(dprodW defHb1) mul_subG ?kerH1c //=. - rewrite Ds1 cfker_conjg ?(subsetP nHUW1) // quotientJ // -sub_conjgV. - rewrite (subset_trans _ (kerH1c s2 Xs2)) // -(bigdprodWY defH1c) sub_gen //. - by rewrite (bigcup_max (inMb w)^-1%g) // !inE ntw groupV mem_quotient. -rewrite -size_filter uniq_leq_size //. - apply/dinjectiveP=> s1 s2 Xs1 Xs2. - case/(cfclass_Ind_irrP _ _ (der_normal 1 M))/cfclassP=> y My Ds2. - by apply: irr_inj; rewrite Ds2 cfConjg_id ?(injXtheta y s1 s2). -move=> _ /imageP[s Xs ->]; rewrite mem_filter /= cfInd1 // -(index_sdprod defM). -rewrite Xtheta_1 // -natrM eqxx mem_seqInd ?gFnormal //. -rewrite (subsetP sXthetaXH0U') // !andbT inertia_Ind_irr ?gFnormal //. -by apply/subsetP=> y /setIP[My /inertiaJ/esym/injXtheta->]. -Qed. - -Import ssrnum Num.Theory. - -(* This is Peterfalvi (9.9); we have exported the fact that HU / H0 is a *) -(* Frobenius group in case (c), as this is directly used in (9.10). *) -Lemma typeP_Galois_characters (is_Galois : typeP_Galois) : - [/\ (*a*) {in X_ H0, forall s, (u %| 'chi_s 1%g)%Cx}, - {in X_ H0C', forall s, 'chi_s 1%g = u%:R /\ - (exists2 xi : 'CF(HC), xi \is a linear_char & 'chi_s = 'Ind xi)}, - (*b*) size mu_ = p.-1 /\ {in mu_, forall mu_j, isIndHC mu_j} - & (*c*) all redM (S_ H0C') -> - [/\ C :=: 1%g, u = (p ^ q).-1 %/ p.-1 - & [Frobenius HU / H0 = Hbar ><| (U / H0)]]]. -Proof. -have [F [phi [psi _ [Kpsi phiJ]]]] := typeP_Galois_P is_Galois. -case=> [oF /isomP[inj_phi im_phi] phiW2] [cycUbar co_u_p1 u_dv_pq1]. -have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. -have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. -have [nsH0C_M nsHC_M _ nsH0C'_M] := nsH0xx_M; have nH0H := normal_norm nsH0H. -have nsH0HU: H0 <| HU := normalS (subset_trans sH0H sHHU) sHUM nsH0M. -have nH0U: U \subset 'N(H0) := subset_trans sUHU (normal_norm nsH0HU). -have nH0C := subset_trans sCU nH0U. -have sH0C_HU: H0C \subset HU by rewrite -(sdprodWY defHU) genS ?setUSS. -have nsH0C_HU: H0C <| HU := normalS sH0C_HU sHUM nsH0C_M. -have nH0C_HU := normal_norm nsH0C_HU. -have [coH0U coHC] := (coprimeSg sH0H coHU, coprimegS sCU coHU). -have [nH0C_H nH0C_U] := (subset_trans sHHU nH0C_HU, subset_trans sUHU nH0C_HU). -have tiHOC_H: H0C :&: H = H0. - by rewrite /= norm_joinEr // -group_modl // setIC coprime_TIg ?mulg1. -have{coH0U} tiHOC_U: H0C :&: U = C. - by rewrite /= norm_joinEr // setIC -group_modr // setIC coprime_TIg ?mul1g. -have isoHbar: Hbar \isog H / H0C. - by have:= second_isog nH0C_H; rewrite tiHOC_H. -have isoUbar: Ubar \isog U / H0C. - by have:= second_isog nH0C_U; rewrite tiHOC_U. -have frobHU: [Frobenius HU / H0C = (H / H0C) ><| (U / H0C)]. - have defHUbar: (H / H0C) ><| (U / H0C) = (HU / H0C)%g. - exact: quotient_coprime_sdprod. - apply/Frobenius_semiregularP=> //; first by rewrite -(isog_eq1 isoHbar). - by rewrite -(isog_eq1 isoUbar); have [] := Frobenius_context frobUW1c. - move=> yb /setD1P[ntyb /morphimP[y nH0Cy Uy] Dyb] /=; rewrite Dyb. - apply/trivgP/subsetP=> _ /setIP[/morphimP[/= x nHOCx Hx ->] /cent1P/commgP]. - rewrite -morphR //; set xy := [~ x, y] => /eqP/coset_idr/=H0Cxy. - have [nH0x nH0y] := (subsetP nH0H x Hx, subsetP nH0U y Uy). - rewrite inE coset_id ?mem_gen // inE coset_idr //; apply: contraNeq ntyb. - rewrite -(morph_injm_eq1 inj_phi) ?mem_quotient // => nz_x. - rewrite {yb}Dyb /= coset_id ?mem_gen // -Kpsi !inE Uy orbC /= -val_eqE. - rewrite -(inj_eq (mulfI nz_x)) mulr1 -[_ * _]phiJ ?mem_quotient // qactJ nH0y. - rewrite -morphJ // conjg_mulR -/xy mkerr ?eqxx // ker_coset -tiHOC_H inE. - by rewrite andbC groupM ?groupV ?memJ_norm ?(subsetP nHU) //= H0Cxy ?groupR. -have{coHC} tiHbC: (Hbar :&: C / H0 = 1)%g by rewrite coprime_TIg ?coprime_morph. -have{tiHbC} defHCbar: Hbar \x (C / H0) = (HC / H0)%g. - by rewrite dprodEY ?quotientY // [C]unlock/= astabQ quotient_setIpre subsetIr. -have sHCHU: HC \subset HU by rewrite -(sdprodWY defHU) genS ?setUS. -have nsHCHU: HC <| HU := normalS sHCHU sHUM nsHC_M. -have sH0HC: H0 \subset HC := subset_trans sH0H (joing_subl H C). -have nsH0HC: H0 <| HC := normalS sH0HC sHCHU nsH0HU. -have nsHHUb: Hbar <| HU / H0 by rewrite quotient_normal. -have I_XH0_C i: i != 0 -> 'I_HU['chi[Hbar]_i %% H0]%CF = HC. - move=> /= nz_i; apply/esym/eqP. - have nsCHUb: C / H0 <| HU / H0 by rewrite -quotientYidl ?quotient_normal. - have sH0C_HC: H0C \subset HC by rewrite genS ?setSU. - have nsH0C_HC: H0C <| HC := normalS sH0C_HC sHCHU nsH0C_HU. - have [j Dj]: exists j, 'chi_j = (cfDprodl defHCbar 'chi_i %% H0)%CF. - by rewrite -dprodl_IirrE -mod_IirrE //; set j := mod_Iirr _; exists j. - have kerH0Cj: H0C \subset cfker 'chi_j. - by rewrite Dj sub_cfker_mod ?join_subG ?normG // quotientYidl ?cfker_sdprod. - rewrite inertia_mod_pre // -(inertia_dprodl defHCbar) ?normal_norm //. - rewrite -inertia_mod_pre // -Dj eqEsubset sub_Inertia //=. - rewrite -(quotientSGK _ sH0C_HC) ?subIset ?nH0C_HU -?inertia_quo //. - rewrite -(quotientYidr nH0C_H) joingA (joing_idPl sH0H) in frobHU. - rewrite -?quo_IirrE ?(inertia_Frobenius_ker (FrobeniusWker frobHU)) //. - by rewrite quo_Iirr_eq0 // -irr_eq1 Dj cfMod_eq1 // cfDprodl_eq1 irr_eq1. -have{I_XH0_C} irr_IndHC r: r \in Iirr_kerD HC H H0 -> 'Ind 'chi_r \in irr HU. - rewrite !inE => /andP[ker'H kerH0]; apply: inertia_Ind_irr => //. - apply: subset_trans (sub_inertia_Res _ (normal_norm nsHHU)) _. - rewrite -{kerH0}(quo_IirrK _ kerH0) // mod_IirrE // in ker'H *. - have /codomP[[i j] Dr] := dprod_Iirr_onto defHCbar (quo_Iirr H0 r). - rewrite {r}Dr dprod_IirrE cfResMod ?joing_subl ?sub_cfker_mod //= in ker'H *. - rewrite cfDprod_Resl linearZ inertia_scale_nz ?irr1_neq0 ?I_XH0_C //. - by apply: contraNneq ker'H => ->; rewrite irr0 cfDprod_cfun1l cfker_sdprod. -have [nb_mu H0C_mu] := nb_redM_H0; set part_a' := ({in X_ H0C', _}). -have Part_a s: s \in X_ H0 -> exists r, 'chi_s = 'Ind[HU, HC] 'chi_r. - rewrite !inE => /andP[Ks'H KsH0]; have [r sHCr] := constt_cfRes_irr HC s. - have{KsH0} KrH0: H0 \subset cfker 'chi_r. - by rewrite (sub_cfker_constt_Res_irr sHCr) // ?normal_norm. - have{Ks'H} Kr'H: ~~ (H \subset cfker 'chi_r). - by rewrite (sub_cfker_constt_Res_irr sHCr) ?joing_subl // ?normal_norm. - have [|s1 Ds1] := irrP _ (irr_IndHC r _); first by rewrite !inE Kr'H. - rewrite -constt_Ind_Res Ds1 constt_irr inE in sHCr. - by rewrite (eqP sHCr) -Ds1; exists r. -have [nH0HC nH0C'] := (normal_norm nsH0HC, subset_trans (der_sub 1 _) nH0C). -have Part_a': part_a'. - move=> s /setDP[KsH0C' Ks'H]; have [|r Ds] := Part_a s. - by rewrite inE Ks'H (subsetP (Iirr_kerS _ _) _ KsH0C') ?joing_subl. - suffices lin_r: 'chi_r \is a linear_char. - by split; [rewrite Du Ds cfInd1 ?lin_char1 ?mulr1 | exists 'chi_r]. - have KrH0C': H0C' \subset cfker 'chi_r. - rewrite inE Ds sub_cfker_Ind_irr // in KsH0C'. - by rewrite (subset_trans sHUM) ?normal_norm. - rewrite lin_irr_der1 (subset_trans _ KrH0C') //= (norm_joinEr nH0C'). - rewrite -quotientSK ?gFsub_trans ?quotient_der //= -/C. - by rewrite -(der_dprod 1 defHCbar) (derG1P abHbar) dprod1g. -split=> // [s /Part_a[r ->] | | {Part_a' part_a'}red_H0C']. -- by rewrite Du cfInd1 // dvdC_mulr // Cint_Cnat ?Cnat_irr1. -- split=> // mu_j /H0C_mu H0C_mu_j; have [s XH0Cs Dmuj] := seqIndP H0C_mu_j. - have [|s1u [xi lin_xi Ds]] := Part_a' s. - by rewrite (subsetP _ _ XH0Cs) ?Iirr_kerDS // genS ?setUS ?der_sub. - split=> //; first by rewrite Dmuj cfInd1 // s1u -natrM -(index_sdprod defM). - by rewrite Dmuj Ds cfIndInd //; exists xi. -have C1: C :=: 1%g. - apply: contraTeq red_H0C' => ntC; apply/allPn. - have sCM: C \subset M := subset_trans sCU (subset_trans sUHU sHUM). - have{sCM} solCbar: solvable (C / H0). - by rewrite quotient_sol ?(solvableS sCM) ?mmax_sol. - have [|{ntC solCbar} j lin_j nz_j] := solvable_has_lin_char _ solCbar. - rewrite -(isog_eq1 (quotient_isog _ _)) ?(subset_trans sCU) //. - by rewrite coprime_TIg ?(coprimegS sCU) ?(coprimeSg sH0H). - have [i lin_i nz_i] := solvable_has_lin_char ntHbar solHbar. - pose r := mod_Iirr (dprod_Iirr defHCbar (i, j)). - have KrH0: H0 \subset cfker 'chi_r by rewrite mod_IirrE ?cfker_mod. - have Kr'H: ~~ (H \subset cfker 'chi_r). - rewrite -subsetIidl -cfker_Res ?joing_subl ?irr_char // mod_IirrE //. - rewrite cfResMod ?joing_subl // sub_cfker_mod // dprod_IirrE. - by rewrite cfDprodKl ?lin_char1 // subGcfker -irr_eq1. - have [|s Ds] := irrP _ (irr_IndHC r _); first by rewrite !inE Kr'H. - have Ks'H: s \notin Iirr_ker HU H. - by rewrite inE -Ds sub_cfker_Ind_irr ?normal_norm. - exists ('Ind 'chi_s). - rewrite mem_seqInd ?gFnormal // inE Ks'H inE -Ds. - rewrite sub_cfker_Ind_irr // ?(subset_trans sHUM) ?normal_norm //=. - rewrite mod_IirrE // join_subG cfker_mod // sub_cfker_mod ?quotient_der //. - apply: subset_trans (dergS 1 (quotientS H0 (joing_subr H C))) _. - by rewrite -lin_irr_der1 dprod_IirrE cfDprod_lin_char. - apply: contra nz_j => red_j; have /implyP := H0C_mu ('Ind 'chi_s). - rewrite mem_filter red_j !mem_seqInd ?gFnormal // !in_setD Ks'H !inE -Ds. - rewrite irr_eq1 !sub_cfker_Ind_irr ?(normal_norm nsH0HU) //. - rewrite mod_IirrE // join_subG cfker_mod //= sub_cfker_mod // dprod_IirrE. - by move/(sub_cfker_Res (subxx _)); rewrite cfDprodKr ?lin_char1 ?subGcfker. -rewrite /= -/C C1 joingG1 in frobHU; split=> //; move/FrobeniusWker in frobHU. -have nsHbHU: Hbar <| (HU / H0) by rewrite quotient_normal. -have ->: (p ^ q).-1 = (#|X_ H0| * u)%N. - rewrite -oF -cardsT -im_phi card_injm // -(card_Iirr_abelian abHbar). - rewrite -(cardsC1 0) (card_imset_Ind_irr nsHbHU) => [|i|i y]; last first. - - by rewrite !inE conjg_Iirr_eq0. - - by rewrite !inE => nz_i; rewrite inertia_Ind_irr ?inertia_Frobenius_ker. - rewrite index_quotient_eq ?(subset_trans sHUM) ?subIset ?sH0H ?orbT //. - apply/eqP; rewrite Du /= C1 joingG1 mulnC eqn_pmul2r //. - rewrite -(card_imset _ (can_inj (mod_IirrK _))) // -imset_comp. - apply/eqP/eq_card=> s; apply/imsetP/idP=> [[i nz_i -> /=] | Xs]. - rewrite !inE mod_IirrE 1?{1}cfker_mod // andbT in nz_i *. - rewrite cfIirrE ?inertia_Ind_irr ?inertia_Frobenius_ker // sub_cfker_mod //. - by rewrite sub_cfker_Ind_irr ?quotientS ?normal_norm // subGcfker. - have [[]] := (Part_a s Xs, setDP Xs). - rewrite /= C1 joingG1 !inE => r Ds [kerH0s]. - have:= kerH0s; rewrite Ds !sub_cfker_Ind_irr ?normal_norm // => kerH0 ker'H. - exists (quo_Iirr H0 r). - by rewrite !inE -subGcfker quo_IirrE // cfker_quo ?quotientSGK. - by rewrite quo_IirrE // cfIndQuo // -Ds -quo_IirrE // irrK quo_IirrK. -suffices ->: #|X_ H0| = p.-1 by rewrite -(subnKC (prime_gt1 p_pr)) mulKn. -rewrite -nb_mu (size_red_subseq_seqInd_typeP MtypeP _ H0C_mu) //; last first. -- exact/allP/filter_all. -- by rewrite filter_uniq ?seqInd_uniq. -apply/esym/eq_card => i; rewrite inE mem_filter mem_seqInd ?gFnormal //. -rewrite andb_idl // => Xi; rewrite (allP red_H0C') //. -by rewrite mem_seqInd ?gFnormal //= C1 (trivgP (der_sub 1 _)) joingG1. -Qed. - -(* This combination of (9.8)(b) and (9.9)(b) covers most uses of these lemmas *) -(* in sections 10-14. *) -Lemma typeP_reducible_core_Ind (ptiWM := FT_primeTI_hyp MtypeP) : - [/\ size mu_ = p.-1, has predT mu_, - {subset mu_ <= [seq primeTIred ptiWM j | j in predC1 0]} - & {in mu_, forall mu_j, isIndHC mu_j}]. -Proof. -have [[sz_mu _] /mulG_sub[sHHU _]] := (nb_redM_H0, sdprodW defHU). -rewrite has_predT sz_mu -subn1 subn_gt0 prime_gt1 //; split=> // [mu_j|]. - rewrite mem_filter => /andP[red_chi /seqIndP[s /setDP[_ kerH's] Dchi]]. - have [[j Ds] | [/idPn[]]] := prTIres_irr_cases ptiWM s; last by rewrite -Dchi. - rewrite Dchi Ds cfInd_prTIres image_f ?inE //=. - by apply: contraNneq kerH's => j0; rewrite inE Ds j0 prTIres0 cfker_cfun1. -have[/typeP_Galois_characters[_ _ []] // | Gal'M] := boolP typeP_Galois. -by have [_ []] := typeP_nonGalois_characters Gal'M. -Qed. - -(* This is Peterfalvi (9.10), formulated as a constructive alternative. *) -Lemma typeP_reducible_core_cases : - {t : Iirr M & 'chi_t \in S_ H0C' /\ 'chi_t 1%g = (q * u)%:R - & {xi | xi \is a linear_char & 'chi_t = 'Ind[M, HC] xi}} - + [/\ typeP_Galois, [Frobenius HU / H0 = Hbar ><| (U / H0)], - cyclic U, #|U| = (p ^ q).-1 %/ p.-1 - & FTtype M == 2 -> [Frobenius HU = H ><| U]]. -Proof. -have [GalM | Gal'M] := boolP typeP_Galois; last first. - pose eqInHCb nu r := ('chi_r \is a linear_char) && (nu == 'Ind[M, HC] 'chi_r). - pose isIndHCb (nu : 'CF(M)) := - (nu 1%g == (q * u)%:R) && [exists r, eqInHCb nu r]. - suffices /sig2W[t H0C't]: exists2 t, 'chi_t \in S_ H0C' & isIndHCb 'chi_t. - case/andP=> /eqP t1qu /exists_inP/sig2W[r lin_r /eqP def_t]. - by left; exists t => //; exists 'chi_r. - have [_ _ [t [t1qu H0Ct IndHCt]] _] := typeP_nonGalois_characters Gal'M. - exists t; first by rewrite (seqIndS _ H0Ct) ?Iirr_kerDS ?genS ?setUS ?der_sub. - rewrite /isIndHCb t1qu eqxx; have [xi lin_xi ->] := IndHCt. - by apply/exists_inP; exists (cfIirr xi); rewrite cfIirrE ?lin_char_irr. -have [_ IndHC_SH0C' _] := typeP_Galois_characters GalM; rewrite all_predC. -case: hasP => [/sig2W[eta H0C'eta /irrP/sig_eqW[t Dt]] _ | _ [//|C1 <- frobHU]]. - have /sig2_eqW[s /IndHC_SH0C'[s1u IndHCs] Deta] := seqIndP H0C'eta. - have [joinHU [xi lin_xi Ds]] := (sdprodWY defHU, sig2_eqW IndHCs). - left; exists t; first split; rewrite -Dt // Deta. - by rewrite cfInd1 ?der_sub // -(index_sdprod defM) s1u -natrM. - by exists xi; rewrite ?Ds ?cfIndInd ?der_sub // -joinHU genS ?setUS ?subsetIl. -have cycU: cyclic U. - rewrite (isog_cyclic (quotient1_isog _)) -C1. - by have [_ _ []] := typeP_Galois_P GalM. -right; split=> //; first by rewrite /u /Ubar C1 -(card_isog (quotient1_isog _)). -case/(compl_of_typeII maxM MtypeP) => /= _ _ _ UtypeF <-. -have [_ -> _] := typeF_context UtypeF. -by apply/forall_inP=> S /and3P[_ /cyclicS->]. -Qed. - -Import ssrint. - -(* This is Peterfalvi (9.11) *) -(* We had to cover a small gap in step (9.11.4) of the proof, which starts by *) -(* proving that U1 \subset {1} u A(M), then asserts this obviously implies *) -(* HU1 \subset {1} u A(M). It is not, as while {1} u A(M) does contain H, it *) -(* is not (necessarily) a subgroup. We had to use the solvability of HU1 in a *) -(* significant way (using Philip Hall's theorems) to bridge the gap; it's *) -(* also possible to exploit lemma (2.1) (partition_cent_rcoset in PFsection1) *) -(* in a slightly different argument, but the inference is nontrivial in *) -(* either case. *) -Lemma Ptype_core_coherence : coherent (S_ H0C') M^# tau. -Proof. -have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. -have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. -have nsCU: C <| U := normalS sCU (joing_subl _ _) nsCUW1. -have [_ nCU] := andP nsCU; have sC'C: C^`(1)%g \subset C := der_sub 1 _. -have coHC := coprimegS sCU coHU; have coH0C := coprimeSg sH0H coHC. -have [nsH0C_M nsHC_M nsH0U'_M nsH0C'_M] := nsH0xx_M; have [_ nH0H]:= andP nsH0H. -have nH0HU := subset_trans sHUM nH0M; have nH0U := subset_trans sUHU nH0HU. -have nH0C := subset_trans sCU nH0U; have nH0C' := subset_trans sC'C nH0C. -have sHCHU: HC \subset HU by rewrite join_subG sHHU (subset_trans sCU). -have [nsHCHU nHC] := (normalS sHCHU sHUM nsHC_M, subset_trans sCU nHU). -have tiHCbar: Hbar :&: (C / H0)%g = 1%g by rewrite coprime_TIg ?coprime_morph. -have defHCbar: Hbar \x (C / H0) = (HC / H0)%g. - by rewrite dprodEY ?quotientY // [C]unlock/= astabQ quotient_setIpre subsetIr. -have{tiHCbar} defHC'bar: (HC / H0)^`(1)%g = (C^`(1) / H0)%g. - by rewrite -(der_dprod 1 defHCbar) (derG1P abHbar) dprod1g quotient_der. -have sU'U := der_sub 1 U; have nH0U' := subset_trans sU'U nH0U. -have sU'C: U' \subset C. - by rewrite [C]unlock subsetI sub_astabQ sU'U nH0U' quotient_cents. -have uS0: uniq (S_ H0C') by apply: seqInd_uniq. -have [rmR scohS0]: exists R : 'CF(M) -> seq 'CF(G), subcoherent (S_ H0C') tau R. - move: (FTtypeP_coh_base _ _) (FTtypeP_subcoherent maxM MtypeP) => R scohR. - exists R; apply: (subset_subcoherent scohR). - split=> //; last exact: cfAut_seqInd. - by apply: seqIndS; rewrite Iirr_kerDS ?sub1G ?Fcore_sub_FTcore. -have [GalM | Gal'M] := boolP typeP_Galois. - have [_ XOC'u _ _] := typeP_Galois_characters GalM. - apply: uniform_degree_coherence scohS0 _. - apply: all_pred1_constant (#|M : HU| * u)%:R _ _; rewrite all_map. - by apply/allP=> _ /seqIndP[s /XOC'u[s1u _] ->] /=; rewrite natrM cfInd1 ?s1u. -have:= typeP_nonGalois_characters Gal'M. -set U1 := 'C_U(_ | _); set a := #|_ : _|. -case: (_ Gal'M) => /= H1 [oH1 nH1U _ defHbar aP] in U1 a *. -rewrite -/U1 -/a in aP; case: aP => a_gt1 a_dv_p1 cycU1 _. -case=> [a_dv_XH0 [nb_mu IndHCmu] has_irrHC lb_Sqa]; rewrite -[S_ _]/(S_ H0C'). -have defHb1 := defHbar; rewrite (big_setD1 1%g) ?group1 ?conjsg1 //= in defHb1. -have [[_ H1c _ defH1c] _ _ _] := dprodP defHb1; rewrite defH1c in defHb1. -have [nsH1H _] := dprod_normal2 defHb1; have [sH1H _] := andP nsH1H. -have nsU1U: U1 <| U; last have [sU1U nU1U] := andP nsU1U. - by rewrite norm_normalI // astabQ norm_quotient_pre ?norms_cent. -have Da: a = #|HU : H <*> U1|. - rewrite /a -!divgS /= ?join_subG ?sHHU ?norm_joinEr ?(subset_trans sU1U) //=. - by rewrite -(sdprod_card defHU) coprime_cardMg ?(coprimegS sU1U) ?divnMl. -have sCU1: C \subset U1 by rewrite [C]unlock setIS ?astabS. -have a_dv_u: a %| u by rewrite Da Du indexgS ?genS ?setUS. -have [a_gt0 q_gt0 u_gt0 p1_gt0]: [/\ 0 < a, 0 < q, 0 < u & 0 < p.-1]%N. - rewrite !cardG_gt0 ltnW // -subn1 subn_gt0 prime_gt1 //. -have [odd_p odd_q odd_a]: [/\ odd p, odd q & odd a]. - by rewrite mFT_odd -oH1 (oddSg sH1H) ?(dvdn_odd a_dv_u) ?mFT_quo_odd. -have Dp: p = (2 * p.-1./2 + 1)%N. - by rewrite mul2n -[p]odd_double_half odd_p half_double addn1. -(* Start of main proof. *) -pose S1 := filter [pred zeta : 'CF(M) | zeta 1%g == (q * a)%:R] (S_ H0C'). -have ntS1: (0 < size S1)%N. - have [lb_dv lbS1] := lb_Sqa; apply: leq_trans (leq_trans lbS1 _). - by rewrite ltn_divRL // mul0n muln_gt0 p1_gt0 cardG_gt0. - rewrite -size_filter uniq_leq_size ?filter_uniq ?seqInd_uniq // => chi. - rewrite !mem_filter -andbA /= => /and3P[_ ->]. - by apply: seqIndS; rewrite Iirr_kerDS // genS ?setUS ?dergS ?subsetIl. -have sS10: cfConjC_subset S1 (S_ H0C'). - split=> [||chi]; first by rewrite filter_uniq. - by apply: mem_subseq; apply: filter_subseq. - rewrite !mem_filter !inE cfunE => /andP[/eqP <- S0chi]. - by rewrite cfAut_seqInd // andbT conj_Cnat ?(Cnat_seqInd1 S0chi). -have cohS1: coherent S1 M^# tau. - apply: uniform_degree_coherence (subset_subcoherent scohS0 sS10) _. - by apply: all_pred1_constant (q * a)%:R _ _; rewrite all_map filter_all. -pose S3 := filter [predC S1] (S_ H0C'); move: {2}_.+1 (ltnSn (size S3)) => nS. -move: @S3 (sS10) (cohS1); have: {subset S1 <= S1} by []. -elim: nS {-1}S1 => // nS IHnS S2 => sS12 S3 sS20 cohS2; rewrite ltnS => leS3nS. -have [ntS3|] := boolP (size S3 > 0)%N; last first. - rewrite size_filter -has_count has_predC negbK => /allP sS02. - exact: subset_coherent sS02 cohS2. -(* Ultimateley we'll contradict the maximality of S2 in (9.11.1) & (9.11.8). *) -suff [chi]: exists2 chi, chi \in S3 & coherent (chi :: chi^* :: S2)%CF M^# tau. - rewrite mem_filter => /andP[/= S2'chi S0chi]; have [uS2 sS2S0 ccS2] := sS20. - move/IHnS; apply=> [psi /sS12 S1psi||]; first by rewrite 2?mem_behead. - split. - - rewrite /= !inE negb_or S2'chi (contra (ccS2 _)) ?cfConjCK // eq_sym. - by rewrite (seqInd_conjC_neq _ _ _ S0chi) ?mFT_odd. - - by apply/allP; rewrite /= S0chi cfAut_seqInd //=; apply/allP. - apply/allP; rewrite /= !inE cfConjCK !eqxx orbT /=. - by apply/allP=> psi /ccS2; rewrite !inE orbA orbC => ->. - apply: leq_trans leS3nS; rewrite ltnNge; apply: contra S2'chi. - case/leq_size_perm=> [|psi|/(_ chi)]; first by rewrite filter_uniq. - by rewrite !mem_filter !inE orbA negb_or -andbA => /andP[]. - by rewrite !mem_filter !inE eqxx S0chi !andbT => /esym/negbFE. -(* This is step (9.11.1). *) clear nS IHnS leS3nS. -without loss [[eqS12 irrS1 H0C_S1] [Da_p defC] [S3qu ne_qa_qu] [oS1 oS1ua]]: - / [/\ [/\ S1 =i S2, {subset S1 <= irr M} & {subset S1 <= S_ H0C}], - a = p.-1./2 /\ C :=: U', - (forall chi, chi \in S3 -> chi 1%g == (q * u)%:R) /\ (q * u != q * a)%N - & size S1 = (p.-1 * u %/ a ^ 2)%N /\ size S1 = (2 * u %/ a)%N]. -- move=> IHwlog; have{sS20} [[uS2 sS20 ccS2] [uS1 _ _]] := (sS20, sS10). - pose is_qu := [pred chi : 'CF(M) | chi 1%g == (q * u)%:R]. - pose isn't_qu := [pred chi | is_qu chi ==> all is_qu S3]. - have /hasP[chi S3chi qu'chi]: has isn't_qu S3. - rewrite /isn't_qu; have [_|] := boolP (all _ _); last by rewrite has_predC. - by rewrite (eq_has (fun _ => implybT _)) has_predT. - have [S2'chi S0chi]: chi \notin S2 /\ chi \in S_ H0C'. - by apply/andP; rewrite mem_filter in S3chi. - have [s X0C's Dchi] := seqIndP S0chi. - have Dchi1: chi 1%g = q%:R * 'chi_s 1%g. - by rewrite Dchi cfInd1 // -(index_sdprod defM). - (* We'll show lb0 <= lb1 <= lb <= lb3 <= sumnS S1' <= sumnS S2 <= lb0, *) - (* with equality under conditions that imply the conclusion of (9.11.1). *) - pose lb0 := (2 * q * a)%:R * chi 1%g. - pose lb1 : algC := (2 * a * q ^ 2 * u)%:R. - pose lb2 : algC := (p.-1 * q ^ 2 * u)%:R. - pose lb3 : algC := (p.-1 * q ^ 2 * #|U : U'|)%:R. - pose S1' := filter [predI irr M & S_ H0U'] S1. - pose szS1' := ((p.-1 * #|U : U'|) %/ a ^ 2)%N; set lbS1' := _ %/ _ in lb_Sqa. - pose Snorm (psi : 'CF(M)) := psi 1%g ^+ 2 / '[psi]. - pose sumnS Si := \sum_(psi <- Si) Snorm psi. - have lb01: lb0 <= lb1 ?= iff (chi 1%g == (q * u)%:R). - rewrite /lb1 mulnA -mulnA natrM /lb0 mulnAC mono_lerif; last first. - by apply: ler_pmul2l; rewrite ltr0n !muln_gt0 a_gt0. - apply: lerif_eq; rewrite Dchi1 natrM ler_pmul2l ?gt0CG //. - have [KsH0C' _] := setDP X0C's; rewrite inE in KsH0C'. - have [t sHCt] := constt_cfRes_irr HC s. - have KtH0C': H0C' \subset cfker 'chi_t. - apply: subset_trans (cfker_constt (cfRes_char _ (irr_char s)) sHCt). - by rewrite cfker_Res ?irr_char // subsetI genS ?setUSS. - rewrite -constt_Ind_Res in sHCt. - apply: ler_trans (char1_ge_constt (cfInd_char _ (irr_char t)) sHCt) _. - rewrite cfInd1 // -Du lin_char1 ?mulr1 // lin_irr_der1. - apply: subset_trans KtH0C'; rewrite /= (norm_joinEr nH0C') /= -/C. - rewrite -quotientSK ?(subset_trans (der_sub _ _)) ?(subset_trans sHCHU) //. - by rewrite -defHC'bar quotient_der ?(subset_trans sHCHU). - have lb12: lb1 <= lb2 ?= iff (a == p.-1./2). - rewrite -(@eqn_pmul2l 2) // -(canLR (addnK 1) Dp) subn1 lerif_nat. - rewrite !(mono_leqif (fun _ _ => leq_pmul2r _)) ?expn_gt0 ?q_gt0 //. - apply: leqif_eq; rewrite dvdn_leq // Gauss_dvd //. - by rewrite {1}Dp addn1 dvdn_mulr. - by rewrite prime_coprime ?dvdn2 ?negbK. - have lb23: lb2 <= lb3 ?= iff (C :==: U') :> algC. - rewrite lerif_nat [u]card_quotient //. - rewrite (mono_leqif (fun _ _ => leq_pmul2l _)) ?muln_gt0 ?p1_gt0 ?q_gt0 //. - rewrite -(mono_leqif (fun _ _ => leq_pmul2l (cardG_gt0 C))) Lagrange //. - rewrite -(Lagrange sU'U) (mono_leqif (fun _ _ => leq_pmul2r _)) //. - by rewrite eq_sym; apply: subset_leqif_cards. - have lb3S1': lb3 <= sumnS S1' ?= iff (size S1' == szS1'). - rewrite /szS1' -(divnMr (cardG_gt0 U')) mulnAC -mulnA Lagrange // -/lbS1'. - have{lb_Sqa} [dv_lb lbSqa] := lb_Sqa; rewrite [sumnS S1']big_seq. - rewrite (eq_bigr (fun _ => ((q * a) ^ 2)%:R)) => [|psi]; last first. - rewrite !mem_filter -!andbA => /and4P[/irrP[r ->] _ /=/eqP r1qa _]. - by rewrite /Snorm cfnorm_irr divr1 r1qa natrX. - rewrite -big_seq (big_nth 0) -natr_sum sum_nat_const_nat subn0. - rewrite mulnC natrM [*%R]lock /lb3 natrM natf_indexg ?der_sub // mulrA. - rewrite -natrM mulnAC -(divnK dv_lb) mulnAC mulnA natrM mulfK ?neq0CG //. - rewrite -/lbS1' -mulnA -expnMn natrM mulrC -lock mono_lerif; last first. - by apply: ler_pmul2l; rewrite ltr0n !muln_gt0 a_gt0 q_gt0. - rewrite eq_sym lerif_nat; apply: leqif_eq; rewrite (leq_trans lbSqa) //. - rewrite -size_filter uniq_leq_size ?filter_uniq ?seqInd_uniq // => psi. - rewrite !mem_filter -!andbA /= => /and3P[-> -> S0psi]; rewrite S0psi. - by apply: seqIndS S0psi; rewrite Iirr_kerDS //= genS ?setUS ?dergS. - have lbS1'2: sumnS S1' <= sumnS S2 ?= iff ~~ has [predC S1'] S2. - have Ds2: perm_eq S2 (S1' ++ filter [predC S1'] S2). - rewrite -(perm_filterC (mem S1')) perm_cat2r. - rewrite uniq_perm_eq ?filter_uniq // => psi. - by rewrite mem_filter andb_idr //= mem_filter => /andP[_ /sS12]. - rewrite [sumnS S2](eq_big_perm _ Ds2) big_cat /= -/(sumnS S1') big_filter. - rewrite -all_predC -big_all_cond !(big_tnth _ _ S2) big_andE. - rewrite -{1}[_ S1']addr0 mono_lerif; last exact: ler_add2l. - set sumS2' := \sum_(i | _) _; rewrite -[0]/(sumS2' *+ 0) -sumrMnl. - apply: lerif_sum => i _; apply/lerifP; rewrite lt0r !mulf_eq0 invr_eq0. - set psi := tnth _ i; have Spsi := sS20 psi (mem_tnth _ _). - rewrite !negb_or (seqInd1_neq0 _ Spsi) //= (cfnorm_seqInd_neq0 _ Spsi) //=. - by rewrite divr_ge0 ?exprn_ge0 ?cfnorm_ge0 ?Cnat_ge0 ?(Cnat_seqInd1 Spsi). - have [lb0S2 | ] := boolP (lb0 < sumnS S2). - exists chi => //; have /hasP[xi S1xi _]: has predT S1 by rewrite has_predT. - have xi1: xi 1%g = (q * a)%:R. - by rewrite mem_filter in S1xi; have [/eqP] := andP S1xi. - apply: (extend_coherent scohS0 _ (sS12 _ S1xi)) => //. - split=> //; last by rewrite mulrAC xi1 -natrM mulnA. - rewrite xi1 Dchi1 irr1_degree -natrM dvdC_nat dvdn_pmul2l ?cardG_gt0 //. - rewrite -dvdC_nat /= !nCdivE -irr1_degree a_dv_XH0 //. - by rewrite (subsetP (Iirr_kerDS _ _ _) _ X0C's) ?joing_subl. - have lb1S2 := lerif_trans lb12 (lerif_trans lb23 (lerif_trans lb3S1' lbS1'2)). - rewrite ltr_neqAle !(lerif_trans lb01 lb1S2) andbT has_predC !negbK. - case/and5P=> /eqP-chi1qu /eqP-Da_p /eqP-defC /eqP-sz_S1' /allP/=sS21'. - have defS1': S1' = S1. - apply/eqP; rewrite -(geq_leqif (size_subseq_leqif (filter_subseq _ S1))). - by rewrite uniq_leq_size // => psi /sS12/sS21'. - apply: IHwlog; split=> //. - + split=> psi; do 1?[rewrite -defS1' mem_filter andbC => /and3P[_ _] //=]. - by apply/idP/idP=> [/sS12 | /sS21']; rewrite ?defS1'. - by congr (_ \in S_ _); apply/group_inj; rewrite /= defC. - + split; first by apply/allP; apply: contraLR qu'chi; rewrite /= chi1qu eqxx. - rewrite -eqC_nat -chi1qu; apply: contra S2'chi => chi1qa. - by rewrite sS12 // mem_filter /= chi1qa. - rewrite -defS1' sz_S1' /szS1' -defC -card_quotient // -/u. - by split=> //; rewrite -mulnn {1}Dp addn1 -Da_p mulnAC divnMr. -have nCW1: W1 \subset 'N(C). - by rewrite (subset_trans (joing_subr U W1)) ?normal_norm. -(* This is step (9.11.2). *) clear sS20 cohS2 sS12 has_irrHC lb_Sqa sU'C. -have [tiU1 le_u_a2]: {in W1^#, forall w, U1 :&: U1 :^ w = C} /\ (u <= a ^ 2)%N. - have tiU1 w: w \in W1^# -> U1 :&: U1 :^ w = C; last split => //. - case/setD1P=> ntw W1w; have nH0w := subsetP (subset_trans sW1M nH0M) w W1w. - pose wb := coset H0 w; have W1wb: wb \in W1bar^#. - rewrite !inE mem_quotient ?(contraNneq _ ntw) // => /coset_idr H0w. - rewrite -in_set1 -set1gE -tiHUW1 inE (subsetP sHHU) // (subsetP sH0H) //. - by rewrite H0w. - have ntH1 w1: H1 :^ w1 :!=: 1%g by rewrite -cardG_gt1 cardJg oH1 prime_gt1. - pose t_ w1 := - if pred2 1%g wb w1 then sval (has_nonprincipal_irr (ntH1 w1)) else 0. - pose theta := - cfDprodl defHCbar (cfBigdprod defHbar (fun w1 => 'chi_(t_ w1))). - have lin_theta : theta \is a linear_char. - rewrite cfDprodl_lin_char ?cfBigdprod_lin_char // => w1 _. - by rewrite irr_prime_lin ?cardJg ?oH1. - have nsH0HC: H0 <| HC. - by rewrite /normal join_subG nH0H sub_gen ?subsetU ?sH0H. - move defK: H0C => K. (* to avoid divergence in Coq kernel *) - have kerK: K \subset cfker (theta %% H0). - rewrite -defK sub_cfker_mod ?join_subG ?normG ?quotientYidl //. - exact: cfker_sdprod. - have sKHC: K \subset HC by rewrite -defK genS ?setSU. - have nsKHC: K <| HC by rewrite (normalS sKHC (normal_sub nsHC_M)) -?defK. - have sH0K: H0 \subset K by rewrite -defK joing_subl. - have nsKHU: K <| HU. - by rewrite (normalS (subset_trans sKHC sHCHU) sHUM) -?defK. - have [t2 Dt2]: {t2 : Iirr (HC / K) | 'chi_t2 %% K = theta %% H0}%CF. - exists (cfIirr ((theta %% H0) / K)). - by rewrite cfIirrE ?cfQuoK ?cfQuo_irr ?cfMod_irr ?lin_char_irr. - have nsHChatHU: HC / K <| HU / K by rewrite quotient_normal. - have sHChatHU := normal_sub nsHChatHU. - pose That := 'I_(HU / K)['chi_t2]%G. - have sThatHU: That \subset (HU / K)%G := Inertia_sub _ _. - have abThatHC: abelian (That / (HC / K)). - rewrite (abelianS (quotientS _ sThatHU)) //. - rewrite (isog_abelian (third_isog _ _ _)) // defC. - rewrite -(isog_abelian (quotient_sdprodr_isog defHU _)) ?gFnormal //. - by rewrite sub_der1_abelian. - have hallHChat: Hall That (HC / K). - rewrite /Hall -(card_isog (third_isog sH0K nsH0HC nsKHC)) /=. - rewrite sub_Inertia // -[in #|_|]defK /= quotientYidl //. - rewrite -(card_isog (sdprod_isog (dprodWsdC defHCbar))). - apply: coprime_dvdr (indexSg (sub_Inertia _ sHChatHU) sThatHU) _. - apply: coprime_dvdr (index_quotient _) _. - by rewrite subIset // normal_norm. - by rewrite -Du coprime_morphl // coprime_morphr. - have [s t2HUs] := constt_cfInd_irr t2 sHChatHU. - have s_1: ('chi_s %% K)%CF 1%g = #|U : U1 :&: U1 :^ w|%:R. - rewrite cfMod1. - have [||_ _ ->] // := cfInd_Hall_central_Inertia _ abThatHC. - rewrite -cfMod1 Dt2 cfMod1 lin_char1 //= mulr1 -inertia_mod_quo // Dt2. - rewrite index_quotient_eq ?normal_norm ?Inertia_sub ?setIS //; last first. - by rewrite (subset_trans sKHC) ?sub_inertia. - rewrite /= inertia_morph_pre //= -quotientE inertia_dprodl; first 1 last. - - by rewrite quotient_norms ?normal_norm. - - rewrite /= -(quotientYidl nH0C) quotient_norms ?normal_norm //. - by rewrite -defK in nsKHU. - have nH1wHU w1: w1 \in (W1 / H0)%g -> (HU / H0)%g \subset 'N(H1 :^ w1). - move=> W1w1; rewrite -(normsP (quotient_norms H0 nHUW1) _ W1w1) normJ. - rewrite conjSg /= -(sdprodW defHU) quotientMl ?mul_subG //. - exact: normal_norm. - rewrite indexgI /= inertia_bigdprod_irr // (big_setD1 1%g) ?group1 //=. - rewrite 2!{1}setIA setIid (bigD1 wb) //= {1 2}/t_ /= !eqxx ?orbT /=. - rewrite !(inertia_irr_prime _ p_pr) ?cardJg //=; - try by case: (has_nonprincipal_irr _). - rewrite conjsg1 centJ setIA -setIIr /=. - elim/big_rec: _ => [|w1 Uk /andP[/setD1P[ntw1 Ww1] w'w1] IHk]; last first. - rewrite /t_ -if_neg negb_or ntw1 w'w1 irr0 Inertia1 -?setIIr 1?setIA //. - rewrite /normal nH1wHU //= -(normsP (quotient_norms H0 nHUW1) _ Ww1). - by rewrite conjSg (subset_trans sH1H) ?quotientS. - rewrite setIT !morphpreI morphpreJ ?(subsetP nH0W1) //= -astabQ. - rewrite quotientGK //; last by rewrite /normal (subset_trans sH0H). - rewrite -(sdprodWY (sdprod_modl defHU _)); last first. - rewrite subsetI -sub_conjgV. - rewrite (normsP (gFnorm _ _)) ?groupV ?(subsetP sW1M) //= andbb. - by rewrite sub_astabQ nH0H sub_abelian_cent. - rewrite -(index_sdprodr defHU) ?subsetIl // conjIg (normsP nUW1) //. - by rewrite -setIIr. - apply/esym/eqP; rewrite eqEcard subsetI -sub_conjgV. - rewrite (normsP _ _ (groupVr W1w)) ?sCU1 /=; last first. - by rewrite (subset_trans (joing_subr U W1)) ?normal_norm. - have{s_1} : pred2 u a #|U : U1 :&: U1 :^ w|. - rewrite /= -!eqC_nat -{}s_1 -mod_IirrE //. - pose phi := 'Ind[M] 'chi_(mod_Iirr s). - have Sphi: phi \in S_ H0C'. - rewrite mem_seqInd ?gFnormal // !inE mod_IirrE //. - rewrite andbC (subset_trans _ (cfker_mod _ _)) //=; last first. - by rewrite -defK genS ?setUS ?der_sub. - rewrite sub_cfker_mod ?(subset_trans sHHU) ?normal_norm //. - have sHHC: H \subset HC by rewrite joing_subl. - rewrite -(sub_cfker_constt_Ind_irr t2HUs) ?quotientS //; last first. - by rewrite quotient_norms ?normal_norm. - rewrite -sub_cfker_mod ?(subset_trans sHHU (normal_norm nsKHU)) //. - rewrite Dt2 sub_cfker_mod //. - apply: contra (valP (has_nonprincipal_irr (ntH1 1%g))). - move/eq_cfker_Res; rewrite cfDprodlK => kerHbar. - have:= sH1H; rewrite -{1}(conjsg1 H1) -kerHbar => /eq_cfker_Res. - by rewrite cfBigdprodKabelian ?group1 // /t_ /= eqxx -subGcfker => ->. - have [/S3qu | ] := boolP (phi \in S3). - rewrite cfInd1 // natrM -(index_sdprod defM). - by rewrite (inj_eq (mulfI (neq0CG _))) => ->. - rewrite mem_filter Sphi andbT negbK /= -eqS12 mem_filter Sphi andbT /=. - rewrite cfInd1 // natrM -(index_sdprod defM) (inj_eq (mulfI (neq0CG _))). - by rewrite orbC => ->. - case/pred2P=> [iUCu | iUCa]. - rewrite -(leq_pmul2r u_gt0) -{1}iUCu /u card_quotient ?Lagrange //. - by rewrite /= -setIA subsetIl. - rewrite subset_leq_card // subIset // [C]unlock subsetI subsetIl sub_astabQ. - rewrite subIset ?nH0U //= centsC -(bigdprodWY defHbar) gen_subG. - apply/orP; left; apply/bigcupsP=> w1 Ww1; rewrite centsC centJ -sub_conjgV. - rewrite (normsP _ _ (groupVr Ww1)) ?quotient_norms //. - by rewrite /U1 astabQ quotient_setIpre subsetIr. - rewrite prime_meetG //; apply/trivgPn; exists w; rewrite // !inE W1w. - rewrite (sameP setIidPr eqP) eqEcard subsetIr /= cardJg. - by rewrite -(leq_pmul2r a_gt0) -{2}iUCa !Lagrange //= -setIA subsetIl. - have /trivgPn[w W1w ntw]: W1 :!=: 1%g by rewrite -cardG_gt1 prime_gt1. - rewrite -(leq_pmul2l u_gt0) mulnn. - have nCU1 := subset_trans sU1U nCU. - have {1}->: u = (#|(U1 / C)%g| * a)%N. - by rewrite mulnC /u !card_quotient // Lagrange_index. - rewrite expnMn leq_pmul2r ?expn_gt0 ?orbF // -mulnn. - rewrite -{2}[U1](conjsgK w) quotientJ ?groupV ?(subsetP nCW1) //. - rewrite cardJg -TI_cardMg /= -/U1 ?subset_leq_card //. - rewrite mul_subG ?quotientS ?subsetIl //. - by rewrite -(normsP nUW1 w W1w) conjSg subsetIl. - by rewrite -quotientGI // tiU1 ?trivg_quotient // !inE ntw. -pose S4 := filter [predD S_ H0C & redM] S3. -have sS43: {subset S4 <= S3} by apply: mem_subseq; apply: filter_subseq. -(* This is step (9.11.3). *) -have nsHM: H <| M by apply: gFnormal. -have oS4: (q * u * size S4 + p.-1 * (q + u))%N = (p ^ q).-1. - rewrite mulnAC {1}[q](index_sdprod defM) -[S4]filter_predI. - rewrite (size_irr_subseq_seqInd _ (filter_subseq _ _)) //; last first. - by move=> xi; rewrite mem_filter -!andbA negbK => /andP[]. - set Xn := finset _; pose sumH0C := \sum_(s in X_ H0C) 'chi_s 1%g ^+ 2. - have /eqP: sumH0C = (q * size S1 * a ^ 2 + (#|Xn| + p.-1) * u ^ 2)%:R. - rewrite [q](index_sdprod defM) natrD natrM natrX. - rewrite (size_irr_subseq_seqInd _ (filter_subseq _ _)) //= -/S1. - have sH0CC': {subset S_ H0C <= S_ H0C'}. - by apply: seqIndS; rewrite Iirr_kerDS // genS ?setUS ?der_sub. - rewrite [sumH0C](big_setID [set s | 'Ind 'chi_s \in S1]) /=; congr (_ + _). - rewrite mulr_natl -[rhs in _ = rhs]sumr_const; apply: eq_big => s. - by rewrite in_setI inE andb_idl // => /H0C_S1; rewrite mem_seqInd. - rewrite 2!inE mem_filter andbCA /= cfInd1 // -(index_sdprod defM) natrM. - by case/andP=> /eqP/(mulfI (neq0CG _))->. - rewrite (eq_bigr (fun _ => u%:R ^+ 2)) => [|s]; last first. - rewrite 2!inE eqS12 => /andP[S2's H0Cs]; congr (_ ^+ 2). - have /S3qu/eqP: 'Ind 'chi_s \in S3. - by rewrite mem_filter /= S2's sH0CC' ?mem_seqInd. - by rewrite natrM cfInd1 // -(index_sdprod defM) => /(mulfI (neq0CG _)). - rewrite sumr_const -mulr_natl natrM natrX -nb_mu; congr (_%:R * _). - have [_ s_mu_H0C] := nb_redM_H0. - rewrite (size_red_subseq_seqInd_typeP MtypeP _ s_mu_H0C); last first. - - by apply/allP; apply: filter_all. - - by rewrite filter_uniq ?seqInd_uniq. - rewrite -/mu_ -[#|_|](cardsID Xn) (setIidPr _); last first. - apply/subsetP=> s; rewrite inE in_setD mem_filter /= -!andbA -eqS12. - rewrite mem_seqInd ?gFnormal // => /and4P[_ -> S1'xi _]. - by rewrite inE S1'xi. - congr (_ + _)%N; apply: eq_card => i; rewrite inE -/mu_ 2!inE. - rewrite -[seqInd M _]/(S_ H0C') mem_filter /= andbC 2!inE eqS12 -!andbA. - rewrite -(mem_seqInd nsHUM) // -/(S_ H0C); set xi := 'Ind _. - apply/idP/idP=> [/and3P[-> H0Cxi] | mu_xi]. - rewrite H0Cxi sH0CC' //= andbT negbK mem_filter unfold_in => ->. - by rewrite (seqIndS _ H0Cxi) // Iirr_kerDS ?joing_subl. - have [xi1u H0Cxi _] := IndHCmu _ mu_xi. - rewrite H0Cxi -eqS12 mem_filter sH0CC' //= !andbT xi1u eqC_nat ne_qa_qu. - by rewrite andbT negbK mem_filter in mu_xi *; case/andP: mu_xi. - rewrite oS1 -mulnA divnK ?dvdn_mul // !mulnA -mulnDl mulnC natrM {}/sumH0C. - rewrite /X_ -Iirr_kerDY joingC joingA (joing_idPl sH0H) /=. - rewrite sum_Iirr_kerD_square ?genS ?setSU //; last first. - by apply: normalS nsH0C_M; rewrite // -(sdprodWY defHU) genS ?setUSS. - rewrite -Du (inj_eq (mulfI (neq0CG _))) -(prednK (indexg_gt0 _ _)). - rewrite mulrSr addrK eqC_nat addnC mulnDl addnAC (mulnC q) -addnA -mulnDr. - move/eqP <-; congr _.-1. - have nH0HC: HC \subset 'N(H0) by rewrite join_subG nH0H. - rewrite -(index_quotient_eq _ _ nH0HC) ?genS ?setSU //; last first. - by rewrite setIC subIset ?joing_subl. - rewrite quotientYidl // -(index_sdprod (dprodWsdC defHCbar)). - by case: Ptype_Fcore_factor_facts. -have /hasP[psi1 S1psi1 _]: has predT S1 by rewrite has_predT. -pose gamma := 'Ind[M, H <*> U1] 1; pose alpha := gamma - psi1. -(* This is step (9.11.4). *) -pose nm_alpha : algC := a%:R + 1 + (q.-1 * a ^ 2)%:R / u%:R. -have [Aalpha Nalpha]: alpha \in 'CF(M, 'A(M)) /\ '[alpha] = nm_alpha. - have sHU1_HU: H <*> U1 \subset HU by rewrite -(sdprodWY defHU) genS ?setUS. - have sHU1_M := subset_trans sHU1_HU sHUM. - have sHU1_A1: H <*> U1 \subset 1%g |: 'A(M). - pose pi := \pi(H); rewrite -subDset; apply/subsetP=> y /setD1P[nty HU1y]. - apply/bigcupP; rewrite notMtype1 /=; have sHMs := Fcore_sub_FTcore maxM. - have defHU1: H ><| U1 = H <*> U1 := sdprod_subr defHU sU1U. - have nsH_HU1: H <| H <*> U1 by have [] := sdprod_context defHU1. - have [HUy [_ nH_HU1]] := (subsetP sHU1_HU y HU1y, normalP nsH_HU1). - have hallH: pi.-Hall(H <*> U1) H. - by rewrite Hall_pi // -(coprime_sdprod_Hall_l defHU1) (coprimegS sU1U). - have hallU1: pi^'.-Hall(H <*> U1) U1. - by rewrite -(compl_pHall _ hallH) sdprod_compl. - have [pi'y | pi_y] := boolP (pi^'.-elt y); last first. - exists y.`_pi; last by rewrite 3!inE nty HUy cent1C groupX ?cent1id. - rewrite !inE (sameP eqP constt1P) pi_y (subsetP sHMs) //. - by rewrite (mem_normal_Hall hallH) ?groupX ?p_elt_constt. - have solHU1: solvable (H <*> U1) by rewrite (solvableS sHU1_M) ?mmax_sol. - have [||z HU1z U1yz] := Hall_Jsub _ hallU1 _ pi'y; rewrite ?cycle_subG //. - have /trivgPn[x /setIP[Hx cxyz] ntx]: 'C_H[y ^ z] != 1%g. - apply: contraTneq (prime_gt1 p_pr) => regHy; rewrite -oH1 cardG_gt1 negbK. - move: U1yz; rewrite -cycleJ subsetI sub_astabQ => /and3P[sYU nHY cH1Y]. - rewrite centsC in cH1Y; rewrite -(setIidPl cH1Y) -(setIidPl sH1H) -setIA. - rewrite -coprime_quotient_cent ?(coprimegS sYU) // cent_cycle regHy. - by rewrite quotient1 setIg1. - exists (x ^ z^-1)%g; last by rewrite 3!inE nty HUy cent1J mem_conjgV cent1C. - by rewrite 2!inE conjg_eq1 ntx (subsetP sHMs) // -mem_conjg nH_HU1. - have{sHU1_A1} Aalpha: alpha \in 'CF(M, 'A(M)). - have A'1: 1%g \notin 'A(M) by have /subsetD1P[] := FTsupp_sub M. - rewrite -['A(M)](setU1K A'1) cfun_onD1 !cfunE subr_eq0 cfInd1 // cfun11. - rewrite mulr1 -(Lagrange_index sHUM) // -(index_sdprod defM) -/q. - rewrite -(index_sdprodr defHU) ?subsetIl // -/a eq_sym andbC. - have:= S1psi1; rewrite mem_filter /= => /andP[-> _] /=. - rewrite rpredB //. - apply: cfun_onS (cfInd_on sHU1_M (cfun_onG _)). - rewrite class_supportEr; apply/bigcupsP=> w Mw. - by rewrite sub_conjg conjUg conjs1g (normsP (FTsupp_norm M)) ?groupV. - have /seqIndP[s /setDP[_ ker'H ] ->] := H0C_S1 _ S1psi1. - rewrite (prDade_Ind_irr_on (FT_prDade_hypF maxM MtypeP)) //. - by rewrite inE in ker'H. - have ->: '[alpha] = '[gamma] + 1. - have /irrP[t Dt] := irrS1 _ S1psi1. - rewrite cfnormBd; first by rewrite Dt cfnorm_irr. - have /seqIndP[s /setDP[_ ker'H ] Dpsi1] := H0C_S1 _ S1psi1. - apply: contraNeq ker'H; rewrite Dt /gamma -irr0 -irr_consttE => tHU1_0. - rewrite inE -(sub_cfker_Ind_irr _ sHUM) ?gFnorm // -Dpsi1 Dt. - rewrite -(sub_cfker_constt_Ind_irr tHU1_0) ?gFnorm ?joing_subl //. - by rewrite irr0 cfker_cfun1 joing_subl. - split=> //; rewrite /nm_alpha addrAC natrM mulrAC mulrC; congr (_ + 1). - rewrite -{1}(mulnK a a_gt0) natf_div ?dvdn_mull // -mulrDr mulnn natrX. - have /sdprod_isom[nH_UW1 isomMH]: H ><| (U <*> W1) = M. - rewrite sdprodEY ?join_subG ?nHU ?(subset_trans sW1M) ?gFnorm //. - by rewrite joingA (sdprodWY defHU) (sdprodWY defM). - rewrite /= -(setIidPl sHHU) norm_joinEr // setIAC -setIA -group_modl //. - by rewrite (setIC W1) tiHUW1 mulg1. - have sU1_UW1: U1 \subset U <*> W1 by rewrite subIset ?joing_subl. - rewrite /gamma -(cfMod_cfun1 _ H) cfIndMod ?joing_subl //. - rewrite cfMod_iso //= quotientYidl ?(subset_trans sU1_UW1) //. - rewrite -(restrm_quotientE _ sU1_UW1) -(cfIsom_cfun1 (restr_isom _ isomMH)). - rewrite (cfIndIsom isomMH) // {nH_UW1 isomMH}cfIsom_iso. - rewrite -(cfIndInd _ (joing_subl U W1)) // cfInd_cfun1 //= -/U1 -/a. - rewrite linearZ cfnormZ normr_nat /=; congr (_ * _). - have defUW1: U ><| W1 = U <*> W1. - by rewrite sdprodEY // -(setIidPl sUHU) -setIA tiHUW1 setIg1. - apply: canLR (mulKf (neq0CG _)) _; rewrite -(sdprod_card defUW1) natrM -/q. - rewrite mulrAC mulrDr mulrCA -{1}(Lagrange sU1U) /= -/U1 -/a -(Lagrange sCU). - rewrite -card_quotient // !natrM !mulfK ?neq0CiG ?neq0CG //. - transitivity (\sum_(x in U <*> W1) \sum_(w1 in W1) \sum_(w2 in W1) - (x ^ w1 \in U1 :&: U1 :^ w2)%g%:R : algC). - - apply: eq_bigr => x _; rewrite (cfIndEsdprod _ _ defUW1) mulr_suml. - apply: eq_bigr => w1 W1w1; rewrite rmorph_sum mulr_sumr. - rewrite (reindex_inj invg_inj) (eq_bigl _ _ (groupV W1)) /=. - rewrite (reindex_acts 'R _ (groupVr W1w1)) ?astabsR //=. - apply: eq_bigr => w2 _; rewrite inE !cfuniE // rmorph_nat -natrM mulnb. - by congr (_ && _)%:R; rewrite invMg invgK conjgM -mem_conjg. - rewrite exchange_big /= mulr_natr -sumr_const; apply: eq_bigr => w1 W1w1. - transitivity (\sum_(w in W1) #|U1 :&: U1 :^ w|%:R : algC). - rewrite exchange_big /=; apply: eq_bigr => w W1w. - rewrite (reindex_acts 'J _ (groupVr W1w1)) ?astabsJ ?normsG ?joing_subr //=. - symmetry; rewrite big_mkcond -sumr_const /= big_mkcond /=. - apply: eq_bigr => x _; rewrite conjgKV. - by case: setIP => [[/(subsetP sU1_UW1)-> //] | _]; rewrite if_same. - rewrite (big_setD1 1%g) //= conjsg1 setIid; congr (_ + _). - rewrite [q](cardsD1 1%g) group1 /= mulr_natl -sumr_const. - by apply: eq_bigr => w W1w; rewrite tiU1. -(* This is step (9.11.5). *) -have [gtS4alpha s4gt0]: (size S4)%:R > '[alpha] /\ (size S4 > 0)%N. - suffices gtS4alpha: (size S4)%:R > '[alpha]. - by split=> //; rewrite -ltC_nat (ler_lt_trans (cfnorm_ge0 alpha)). - rewrite Nalpha -(@ltr_pmul2r _ u%:R) ?ltr0n // mulrDl divfK ?neq0CG //. - rewrite -(ltr_pmul2l (gt0CG W1)) -/q -mulrSr -!(natrM, natrD) ltC_nat. - rewrite mulnA mulnAC -(ltn_add2r (p.-1 * (q + u))) oS4 {1}Dp addn1 -Da_p /=. - apply: leq_ltn_trans (_ : q.+2 * a ^ 3 + q ^ 2 * a ^ 2 + 2 * q * a < _)%N. - rewrite (addnC q) 2!mulnDr addnA (mulnAC _ a q) leq_add2r. - rewrite mulnA addnAC -mulnDl mulnS -addnA -mulnDl addn2 mulnCA -mulnA. - rewrite -[q in (_ <= _ + q * _)%N](prednK q_gt0) (mulSn q.-1) addnA. - by rewrite leq_add2r mulnA -mulnDl addnC leq_mul. - have q_gt2: (2 < q)%N. - by rewrite ltn_neqAle prime_gt1 ?(contraTneq _ odd_q) => // <-. - apply: leq_trans (_ : a.*2 ^ q + 'C(q, 2) * a.*2 ^ 2 + q * a.*2 <= _)%N. - rewrite -mul2n (mulnCA q) (mulnA 2) ltn_add2r !expnMn -addSn leq_add //. - apply: leq_ltn_trans (_ : q.-1.*2.+1 * a ^ q < _)%N. - rewrite leq_mul ?leq_pexp2l //. - by rewrite -(subnKC q_gt2) -addnn !addnS !ltnS leq_addl. - rewrite ltn_pmul2r ?expn_gt0 ?a_gt0 // -doubleS. - by rewrite -(prednK q_gt0) expnS mul2n leq_double ltn_expl. - rewrite mulnA leq_pmul2r ?expn_gt0 ?a_gt0 // -(subnKC q_gt2). - rewrite mulnCA mulnA addSn -mul_bin_diag bin1 -mulnA leq_pmul2l //. - by rewrite mulnS -addSnnS leq_addr. - rewrite Dp -Da_p mul2n (addnC a.*2) expnDn -(subnKC q_gt2) !addSn add0n. - rewrite 3!big_ord_recl big_ord_recr /= !exp1n /= bin1 binn !mul1n /bump /=. - by do 2!rewrite addnC leq_add2l; apply: leq_addl. -have{cohS1} [tau1 cohS1] := cohS1; have [[Itau1 Ztau1] Dtau1] := cohS1. -have sS30: cfConjC_subset S3 (S_ H0C'). - split=> [|chi|chi]; first by rewrite filter_uniq ?seqInd_uniq. - by rewrite mem_filter => /andP[]. - rewrite !mem_filter /= -!eqS12 => /andP[S1'chi S_chi]. - rewrite cfAut_seqInd // (contra _ S1'chi) //. - by have [_ _ ccS1] := sS10; move/ccS1; rewrite cfConjCK. -have scohS3: subcoherent S3 tau rmR := subset_subcoherent scohS0 sS30. -have [tau3 cohS3]: coherent S3 M^# tau. - apply: uniform_degree_coherence scohS3 _. - apply: all_pred1_constant (q * u)%:R _ _. - by rewrite all_map; apply/allP=> chi /S3qu. -have [IZtau3 Dtau3] := cohS3; have [Itau3 Ztau3] := IZtau3. -have notA1: 1%g \notin 'A(M) by have /subsetD1P[] := FTsupp_sub M. -have sS0_1A: {subset S_ H0C' <= 'CF(M, 1%g |: 'A(M))}. - move=> _ /seqIndP[s /setDP[_ ker'H] ->]; rewrite inE in ker'H. - by rewrite (prDade_Ind_irr_on (FT_prDade_hypF maxM MtypeP)). -have sS0A: {subset 'Z[S_ H0C', M^#] <= 'Z[irr M, 'A(M)]}. - move=> chi; rewrite (zcharD1_seqInd_Dade _ notA1) //. - by apply: zchar_sub_irr; apply: seqInd_vcharW. -have Zalpha: alpha \in 'Z[irr M]. - rewrite rpredB ?char_vchar ?cfInd_char ?rpred1 //. - exact: seqInd_char (H0C_S1 _ S1psi1). -have ZAalpha: alpha \in 'Z[irr M, 'A(M)] by rewrite zchar_split Zalpha. -have [Itau Ztau]: {in 'Z[irr M, 'A(M)], isometry tau, to 'Z[irr G]}. - apply: sub_iso_to (Dade_Zisometry _); last exact: zcharW. - by apply: zchar_onS; apply: FTsupp_sub0. -have oSgamma: {in S_ H0C', forall lam, '[gamma, lam] = 0}. - move=> _ /seqIndP[s /setDP[_ ker'H ] ->]. - rewrite ['Ind _]cfun_sum_constt cfdot_sumr big1 // => t sMt. - rewrite cfdotZr [gamma]cfun_sum_constt cfdot_suml big1 ?mulr0 // => t0 gMt0. - rewrite cfdotZl cfdot_irr (negPf (contraNneq _ ker'H)) ?mulr0 // => Dt0. - rewrite inE (sub_cfker_constt_Ind_irr sMt) ?gFnorm // -Dt0. - rewrite /gamma -irr0 in gMt0. - rewrite -(sub_cfker_constt_Ind_irr gMt0) ?gFnorm ?joing_subl //. - by rewrite irr0 cfker_cfun1 joing_subl. - by rewrite (subset_trans _ sHUM) // join_subG sHHU subIset ?sUHU. -(* This is step (9.11.6). *) -have [/eqP psi1qa Spsi1]: psi1 1%g == (q * a)%:R /\ psi1 \in S_ H0C'. - by move: S1psi1; rewrite mem_filter => /andP[]. -have o_alpha_S3: orthogonal alpha^\tau (map tau3 S3). - rewrite /orthogonal /= andbT all_map. - apply: contraFT (ltr_geF gtS4alpha) => /allPn[lam0 S3lam0 /= alpha_lam0]. - set ca := '[_, _] in alpha_lam0; pose al0 := (-1) ^+ (ca < 0)%R *: alpha. - have{alpha_lam0} al0_lam0: '[al0^\tau, tau3 lam0] > 0. - have Zca: ca \in Cint by rewrite Cint_cfdot_vchar ?Ztau // Ztau3 ?mem_zchar. - by rewrite linearZ cfdotZl (canLR (signrMK _) (CintEsign Zca)) normr_gt0. - rewrite -Itau // -(cfnorm_sign (ca < 0)%R) -linearZ /= -/al0. - have S4_dIirrK: {in map tau3 S4, cancel (dirr_dIirr id) (@dchi _ _)}. - apply: dirr_dIirrPE => _ /mapP[lam S4lam ->]. - rewrite mem_filter -andbA negbK in S4lam. - have [/irrP[i Dlam] _ S3lam] := and3P S4lam. - by rewrite dirrE Itau3 ?Ztau3 ?mem_zchar //= Dlam cfnorm_irr. - rewrite -(size_map tau3) -(size_map (dirr_dIirr id)). - rewrite -(card_uniqP _); last first. - rewrite !map_inj_in_uniq ?filter_uniq ?seqInd_uniq //. - apply: sub_in2 (Zisometry_inj Itau3) => lam. - by rewrite mem_filter => /andP[_ /mem_zchar->]. - exact: can_in_inj S4_dIirrK. - apply: ler_trans (_ : #|dirr_constt al0^\tau|%:R <= _); last first. - have Zal0: al0^\tau \in 'Z[irr G] by rewrite Ztau ?rpredZsign. - rewrite cnorm_dconstt // -sumr_const ler_sum // => i al0_i. - by rewrite sqr_Cint_ge1 ?gtr_eqF -?dirr_consttE // Cint_Cnat ?Cnat_dirr. - rewrite leC_nat subset_leq_card //; apply/subsetP=> _ /mapP[nu S4nu ->]. - rewrite dirr_consttE S4_dIirrK //; congr (_ > 0): al0_lam0. - rewrite {al0}linearZ !cfdotZl /=; congr (_ * _) => {ca}; apply/eqP. - have{nu S4nu} [lam S4lam ->] := mapP S4nu. - rewrite mem_filter in S4lam; have{S4lam} [_ S3lam] := andP S4lam. - have Zdlam: lam0 - lam \in 'Z[S3, M^#]. - rewrite zcharD1E rpredB ?mem_zchar //= !cfunE subr_eq0. - by have [/eqP->] := (S3qu _ S3lam, S3qu _ S3lam0). - rewrite -subr_eq0 -cfdotBr -raddfB Dtau3 //. - rewrite Itau // ?sS0A //; last exact: zchar_filter Zdlam. - suffices{lam S3lam Zdlam} oS3a: {in S3, forall lam, '[alpha, lam] = 0}. - by rewrite cfdotBr subr_eq0 !oS3a. - move=> lam; rewrite mem_filter /= -eqS12 => /andP[S1'lam H0C'lam]. - by rewrite cfdotBl oSgamma // (seqInd_ortho _ Spsi1) ?(memPn S1'lam) // subr0. -have{s4gt0 gtS4alpha} /hasP[lam1 S4lam1 _]: has predT S4 by rewrite has_predT. -have [/irrP[l1 Dl1] S3lam1]: lam1 \in irr M /\ lam1 \in S3. - by move: S4lam1; rewrite mem_filter -andbA negbK => /and3P[]. -have [S1'lam1 Slam1]: lam1 \notin S1 /\ lam1 \in S_ H0C'. - by move: S3lam1; rewrite mem_filter eqS12 => /andP[]. -have S3lam1s: lam1^*%CF \in S3 by have [[_ _ ->]] := scohS3. -have ZS3dlam1: lam1 - lam1^*%CF \in 'Z[S3, M^#]. - rewrite zcharD1E rpredB ?mem_zchar //. - by have:= seqInd_sub_aut_zchar nsHUM conjC Slam1; rewrite zcharD1 => /andP[]. -have ZAdlam1: lam1 - lam1^*%CF \in 'Z[irr M, 'A(M)]. - rewrite sS0A // zchar_split rpredB ?mem_zchar ?cfAut_seqInd //. - by rewrite (zchar_on ZS3dlam1). -pose beta := lam1 - (u %/ a)%:R *: psi1. -have ZAbeta: beta \in 'Z[irr M, 'A(M)]. - apply: sS0A; rewrite zcharD1E rpredB ?scaler_nat ?rpredMn ?mem_zchar //=. - by rewrite !cfunE subr_eq0 psi1qa -natrM mulnCA divnK // S3qu. -have [_ _ poSS _ _] := scohS0; have [_ oSS] := pairwise_orthogonalP poSS. -have o1S1: orthonormal S1. - rewrite orthonormalE filter_pairwise_orthogonal // andbT. - by apply/allP=> _ /irrS1/irrP[t ->]; rewrite /= cfnorm_irr. -have o1S4: orthonormal S4. - rewrite orthonormalE !filter_pairwise_orthogonal // andbT. - apply/allP=> nu; rewrite mem_filter /= -andbA negbK. - by case/andP=> /irrP[t ->]; rewrite cfnorm_irr. -have n1psi1: '[psi1] = 1 by have [_ -> //] := orthonormalP o1S1; rewrite eqxx. -have n1lam1: '[lam1] = 1 by have [_ -> //] := orthonormalP o1S4; rewrite eqxx. -have oS14tau: orthogonal (map tau1 S1) (map tau3 S4). - apply/orthogonalP=> psi _ S1psi /mapP[lam /sS43 S3lam ->]. - apply: {psi lam S3lam}orthogonalP S1psi (map_f tau3 S3lam). - apply: (coherent_ortho scohS0 sS10 cohS1 sS30 cohS3) => psi /=. - by rewrite mem_filter !inE eqS12 => /andP[-> _]. -have [Gamma [S4_Gamma normGamma [b Dbeta]]]: - exists Gamma, [/\ Gamma \in 'Z[map tau3 S4], '[Gamma] = 1 - & exists b : bool, beta^\tau - = Gamma - (u %/ a)%:R *: tau1 psi1 + b%:R *: \sum_(psi <- S1) tau1 psi]. -- have [G S4G [G' [Dbeta _ oG'4]]] := orthogonal_split (map tau3 S4) beta^\tau. - have [B S1B [Delta [dG' _ oD1]]] := orthogonal_split (map tau1 S1) G'. - have sZS43: {subset 'Z[S4] <= 'Z[S3]} := zchar_subset sS43. - have [Itau34 Ztau34] := sub_iso_to sZS43 sub_refl IZtau3. - have Z_G: G \in 'Z[map tau3 S4]. - have [_ -> ->] := orthonormal_span (map_orthonormal Itau34 o1S4) S4G. - rewrite big_seq rpred_sum // => xi S4xi; rewrite rpredZ_Cint ?mem_zchar //. - rewrite -(addrK G' G) -Dbeta cfdotBl (orthoPl oG'4) // subr0. - rewrite Cint_cfdot_vchar ?Ztau //. - by have{xi S4xi} [xi S4xi ->] := mapP S4xi; rewrite Ztau34 ?mem_zchar. - have oD4: orthogonal Delta (map tau3 S4). - apply/orthoPl=> xi S4xi; rewrite -(addKr B Delta) addrC -dG' cfdotBl. - by rewrite (orthoPl oG'4) // (span_orthogonal oS14tau) ?subrr // memv_span. - have [_ -> dB] := orthonormal_span (map_orthonormal Itau1 o1S1) S1B. - pose b := (u %/ a)%:R + '[B, tau1 psi1]. - have betaS1_B: {in S1, forall psi, '[beta^\tau, tau1 psi] = '[B, tau1 psi]}. - move=> psi S1psi; rewrite Dbeta dG' !cfdotDl (orthoPl oD1) ?map_f // addr0. - rewrite cfdotC (span_orthogonal oS14tau) ?rmorph0 ?add0r //. - by rewrite memv_span ?map_f. - have Zb: b \in Cint. - rewrite rpredD ?rpred_nat // -betaS1_B // Cint_cfdot_vchar ?Ztau //. - by rewrite Ztau1 ?mem_zchar. - have{dB} dB: B = - (u %/ a)%:R *: tau1 psi1 + b *: \sum_(psi <- S1) tau1 psi. - rewrite dB big_map !(big_rem _ S1psi1) /= scalerDr addrA -scalerDl addKr. - rewrite scaler_sumr; congr (_ + _); apply: eq_big_seq => psi. - rewrite mem_rem_uniq ?filter_uniq ?seqInd_uniq // => /andP[/= psi_1' S1psi]. - apply/esym/eqP; rewrite -subr_eq0 -scalerBl -addrA -!betaS1_B // -cfdotBr. - have [/eqP psi_qa Spsi]: psi 1%g == (q * a)%:R /\ psi \in S_ H0C'. - by move: S1psi; rewrite mem_filter => /andP[]. - have Z1dpsi: psi1 - psi \in 'Z[S1, M^#]. - by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE psi1qa psi_qa subrr. - rewrite -raddfB Dtau1 // Itau //; last first. - by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi). - rewrite cfdotC cfdotBr cfdotZr !cfdotBl 2?oSS ?(memPn S1'lam1) // subrr. - by rewrite add0r n1psi1 oSS // subr0 mulr1 rmorphN conjCK subrr scale0r. - have Gge1: 1 <= '[G] ?= iff ('[G] == 1). - rewrite eq_sym; apply: lerif_eq. - have N_G: '[G] \in Cnat. - apply: Cnat_cfnorm_vchar; apply: zchar_sub_irr Z_G => _ /mapP[nu S4nu ->]. - by rewrite Ztau34 ?mem_zchar. - rewrite -(truncCK N_G) ler1n lt0n -eqC_nat truncCK {N_G}// cfnorm_eq0. - have: '[beta^\tau, (lam1 - lam1^*%CF)^\tau] != 0. - rewrite Itau // cfdotBl cfdotZl !cfdotBr n1lam1. - rewrite (seqInd_conjC_ortho _ _ _ Slam1) ?mFT_odd // subr0. - rewrite !oSS ?cfAut_seqInd -?(inv_eq (@cfConjCK _ _)) ?(memPn S1'lam1) //. - by rewrite !(subr0, mulr0) oner_eq0. - by have [_ _ ->] := sS10. - rewrite Dbeta -Dtau3 //; apply: contraNneq => ->. - rewrite add0r raddfB cfdotBr !(orthoPl oG'4) ?map_f ?subr0 //. - move: S4lam1; rewrite ![_ \in S4]mem_filter /= !negbK /= cfAut_irr S3lam1s. - by case/andP=> /andP[-> /cfAut_seqInd->]. - have ubG: '[G] + (b ^+ 2 - b) * (u %/ a).*2%:R + '[Delta] = 1. - apply: (addrI ((u %/ a) ^ 2)%:R); transitivity '[beta^\tau]. - rewrite -!addrA addrCA Dbeta cfnormDd; last first. - by rewrite cfdotC (span_orthogonal oG'4) ?rmorph0 // memv_span ?inE. - congr (_ + _); rewrite !addrA dG' cfnormDd; last first. - by rewrite cfdotC (span_orthogonal oD1) ?rmorph0 // memv_span ?inE. - congr (_ + _); rewrite dB scaleNr [- _ + _]addrC cfnormB !cfnormZ. - rewrite normr_nat Cint_normK // scaler_sumr cfdotZr rmorph_nat. - rewrite cfnorm_map_orthonormal // cfproj_sum_orthonormal //. - rewrite Itau1 ?mem_zchar // n1psi1 mulr1 rmorphM rmorph_nat conj_Cint //. - rewrite -mulr2n oS1ua -muln_divA // mul2n -addrA addrCA -natrX mulrBl. - by congr (_ + (_ - _)); rewrite -mulrnAl -mulrnA muln2 mulrC. - rewrite Itau // cfnormBd; last first. - by rewrite cfdotZr oSS ?mulr0 // (memPnC S1'lam1). - by rewrite cfnormZ normr_nat n1psi1 n1lam1 mulr1 addrC -natrX. - have ubDelta: '[G] <= '[G] + '[Delta] ?= iff (Delta == 0). - rewrite addrC -lerif_subLR subrr -cfnorm_eq0 eq_sym. - by apply: lerif_eq; apply: cfnorm_ge0. - have{ubG} ubDeltaG: '[G] + '[Delta] <= 1 ?= iff pred2 0 1 b. - rewrite -{1}ubG addrAC [_ + _ + _] addrC -lerif_subLR subrr /=. - set n := _%:R; rewrite mulrC -{1}(mulr0 n) mono_lerif; last first. - by apply: ler_pmul2l; rewrite ltr0n double_gt0 divn_gt0 // dvdn_leq. - rewrite /= -(subr_eq0 b 1) -mulf_eq0 mulrBr mulr1 eq_sym. - apply: lerif_eq; rewrite subr_ge0. - have [-> | nz_b] := eqVneq b 0; first by rewrite expr2 mul0r. - rewrite (ler_trans (real_ler_norm _)) ?Creal_Cint // -[`|b|]mulr1. - by rewrite -Cint_normK // ler_pmul2l ?normr_gt0 // norm_Cint_ge1. - have [_ /esym] := lerif_trans Gge1 (lerif_trans ubDelta ubDeltaG). - rewrite eqxx => /and3P[/eqP normG1 /eqP Delta0 /pred2P b01]. - exists G; split=> //; exists (b != 0). - rewrite Dbeta dG' Delta0 addr0 dB scaleNr addrA; congr (_ + _ *: _). - by case: b01 => ->; rewrite ?eqxx ?oner_eq0. -(* Final step (9.11.8). *) -have alpha_beta: '[alpha^\tau, beta^\tau] = (u %/ a)%:R. - rewrite Itau // cfdotBr cfdotZr rmorph_nat !cfdotBl !oSgamma // !sub0r. - by rewrite n1psi1 mulrN opprK mulr1 addrC oSS ?subr0 // (memPn S1'lam1). -have [X S1X [Delta [Dalpha _ oD1]]]:= orthogonal_split (map tau1 S1) alpha^\tau. -pose x := 1 + '[X, tau1 psi1]. -have alphaS1_X: {in S1, forall psi, '[alpha^\tau, tau1 psi] = '[X, tau1 psi]}. - by move=> psi S1psi; rewrite Dalpha cfdotDl (orthoPl oD1) ?map_f // addr0. -have Zx: x \in Cint. - rewrite rpredD ?rpred1 // -alphaS1_X // Cint_cfdot_vchar ?Ztau //. - by rewrite Ztau1 ?mem_zchar. -have{alphaS1_X S1X} defX: X = x *: (\sum_(psi <- S1) tau1 psi) - tau1 psi1. - have [_ -> ->] := orthonormal_span (map_orthonormal Itau1 o1S1) S1X. - rewrite addrC -scaleN1r big_map !(big_rem _ S1psi1) /= scalerDr addrA. - rewrite -scalerDl addKr scaler_sumr; congr (_ + _); apply: eq_big_seq => psi. - rewrite mem_rem_uniq ?filter_uniq ?seqInd_uniq // => /andP[/= psi_1' S1psi]. - apply/esym/eqP; rewrite -subr_eq0 -scalerBl -addrA -!alphaS1_X // -cfdotBr. - have [/eqP psi_qa Spsi]: psi 1%g == (q * a)%:R /\ psi \in S_ H0C'. - by move: S1psi; rewrite mem_filter => /andP[]. - have Z1dpsi: psi1 - psi \in 'Z[S1, M^#]. - by rewrite zcharD1E rpredB ?mem_zchar //= !cfunE psi1qa psi_qa subrr. - rewrite -raddfB Dtau1 // Itau //; last first. - by rewrite sS0A // zchar_split rpredB ?mem_zchar ?(zchar_on Z1dpsi). - rewrite cfdotBr !cfdotBl !oSgamma // n1psi1 cfdotC oSS // rmorph0. - by rewrite !subr0 add0r subrr scale0r. -have{x Zx X defX Delta Dalpha oD1} b_mod_ua: (b == 0 %[mod u %/ a])%C. - rewrite -oppr0 -eqCmodN (eqCmod_trans _ (eqCmodm0 _)) // {2}nCdivE. - rewrite -alpha_beta Dbeta -addrA cfdotDr. - rewrite (span_orthogonal o_alpha_S3) ?add0r; first 1 last. - - by rewrite memv_span ?inE. - - apply: subvP (zchar_span S4_Gamma); apply: sub_span; apply: mem_subseq. - by rewrite map_subseq ?filter_subseq. - rewrite Dalpha addrC cfdotDl (span_orthogonal oD1); first 1 last. - - by rewrite memv_span ?inE. - - rewrite addrC rpredB ?rpredZ //; last by rewrite memv_span ?map_f. - by rewrite big_seq rpred_sum // => psi S1psi; rewrite memv_span ?map_f. - rewrite add0r addrC defX cfdotBr cfdotBl cfdotZl cfdotZr !scaler_sumr. - rewrite cfdotZr !rmorph_nat cfdotBl Itau1 ?mem_zchar // n1psi1. - rewrite cfnorm_map_orthonormal // cfdotC !cfproj_sum_orthonormal //. - rewrite rmorph_nat oS1ua -muln_divA // natrM !mulrA addrC mulrC addrA. - rewrite -mulNr -mulrDl eqCmod_sym eqCmod_addl_mul // addrC !rpredB ?rpred1 //. - by rewrite !rpredM ?rpred_nat. -have{b_mod_ua alpha_beta} b0: b = 0%N :> nat. - have:= b_mod_ua; rewrite /eqCmod subr0 dvdC_nat => /eqnP. - rewrite modn_small // (leq_ltn_trans (leq_b1 b)) // ltn_divRL // mul1n. - by rewrite ltn_neqAle -(eqn_pmul2l q_gt0) eq_sym ne_qa_qu dvdn_leq. -exists lam1 => //; suffices: coherent (lam1 :: lam1^* :: S1)%CF M^# tau. - by apply: subset_coherent => phi; rewrite !inE eqS12. -move: Dbeta; rewrite b0 scale0r addr0. -apply: (extend_coherent_with scohS0 sS10 cohS1); first by []. -rewrite rpred_nat psi1qa -natrM mulnCA (eqP (S3qu _ S3lam1)) divnK //. -rewrite cfdotC (span_orthogonal oS14tau) ?(zchar_span S4_Gamma) ?conjC0 //. -by rewrite rpredZ ?memv_span ?map_f. -Qed. - -End Nine. |