proposition: Lemma FTtype34_not_ortho_cycTIiso zeta : zeta \in S1 -> ~~ eq_proj_eta (tau (bridge0 zeta)) (eta_col 0).
proof: Proof. move=> S1zeta; set psi := tau _; apply/negP=> proj_psi_eta. have irr_zeta: zeta \in irr M := irrS1 S1zeta. have Szeta: zeta \in S_ 1 by apply: seqInd_sub S1zeta. have Zzeta_S1: {in S1, forall xi, zeta - xi \in 'Z[S1, M^#]}. by move=> * /=; rewrite zcharD1E rpredB ?mem_zchar //= !cfunE !S1_1 ?subrr. have n1S1: {in S1, forall xi, '[xi] = 1} by move=> xi /irrS1/irrWnorm. have Z_S1: {in S1, forall xi, xi \in 'Z[S1]} by apply: mem_zchar. have [p_gt0 q_gt0 u_gt0]: [/\ p > 0, q > 0 & u > 0]%N by rewrite !cardG_gt0. have q_gt2: (q > 2)%N by rewrite odd_prime_gt2 ?mFT_odd. have mu2_1 i j: j != 0 -> mu2_ i j 1%g = d%:R. by have [/(_ i j)] := FTtype345_constants maxM MtypeP notMtype2. have [Dd delta1 Dn]: [/\ d = u, delta = 1 & n = (size S1)%:R]. have size_S1 : (size S1 * q = u - 1)%N. rewrite mulnC [q](index_sdprod defM). rewrite (size_irr_subseq_seqInd _ (subseq_refl _)) //. transitivity #|[set mod_Iirr t | t : Iirr (HU / HC) in predC1 0]|. apply/eq_card=> s; rewrite inE mem_seqInd // !inE subGcfker. apply/andP/imsetP=> [[nzs kHCs] | [t nzt ->]]. by exists (quo_Iirr HC s); rewrite ?quo_IirrK // inE quo_Iirr_eq0. by rewrite mod_Iirr_eq0 // mod_IirrE // cfker_mod. rewrite card_imset; last exact: can_inj (mod_IirrK _). have isoUC: U / C \isog HU / HC by apply: quotient_sdprodr_isog. rewrite subn1 cardC1 card_Iirr_abelian -?(card_isog isoUC) //. by rewrite -(isog_abelian isoUC) defU' der_abelian. have Dd: d = u. apply/eqP; rewrite -(eqn_pmul2l q_gt0) -eqC_nat -(mu_1 nz_j1). by rewrite natrM prTIred_1 mu2_1. suffices delta1: delta = 1. by rewrite /n Dd delta1 -(@natrB _ _ 1) // -size_S1 natrM mulfK ?neq0CG. have: (delta == 1 %[mod q])%C. rewrite -(eqCmod_transl _ (prTIirr1_mod ptiWM 0 j1)) mu2_1 // -/q Dd. by rewrite /eqCmod -(@natrB _ u 1) // dvdC_nat -size_S1 dvdn_mull. rewrite -[1]subr0 [delta]signrE -/ptiWM eqCmodDl eqCmodN opprK. by rewrite eqCmod0_nat; case: (Idelta j1); first rewrite gtnNdvd. have deltaZ gamma: delta *: gamma = gamma by rewrite delta1 scale1r. have [tau1 coh_tau1] := cohS1; pose zeta1 := tau1 zeta. without loss Dpsi: tau1 coh_tau1 @zeta1 / psi = eta_col 0 - zeta1. move=> IHtau1; have [[Itau1 Ztau1] Dtau1] := coh_tau1. have tau1_dirr: {in S1, forall xi, tau1 xi \in dirr G}. by move=> xi S1xi; rewrite /= dirrE Ztau1 ?Itau1 ?mem_zchar //= n1S1. pose chi : 'CF(G) := eta_col 0 - psi. have Dpsi: psi = eta_col 0 - chi by rewrite opprD opprK addNKr. have chi'zeta1: chi <> zeta1. by move=> Dchi; case: (IHtau1 tau1); rewrite -/zeta1 -?Dchi. have dirr_chi: chi \in dirr G. apply: dirr_norm1. rewrite rpredB ?rpred_sum // => [i _|]; first exact: cycTIiso_vchar. rewrite Dade_vchar // zchar_split A0bridge0 //. by rewrite rpredB ?char_vchar ?prTIred_char ?irrWchar. apply: (addrI q%:R); transitivity '[psi]; last first. rewrite Dade_isometry ?A0bridge0 // (cfnormBd (omuS1 _ _)) //. by rewrite cfnorm_prTIred n1S1. rewrite Dpsi [RHS]cfnormDd; last first. rewrite opprB cfdotC cfdot_sumr big1 ?conjC0 // => i _. by rewrite (orthoPl proj_psi_eta) ?map_f ?mem_irr. rewrite cfnormN -nirrW1 -sumr_const cfdot_sumr. by congr (_ + _); apply: eq_bigr => i _; rewrite proj_col_eta. have Dchi: {in S1, forall xi, xi != zeta -> chi = - tau1 xi}. move=> xi S1xi /negPf-zeta'xi; have irr_xi := irrS1 S1xi. suffices: '[zeta1 - tau1 xi, chi] = 1. by case/cfdot_add_dirr_eq1; rewrite ?rpredN ?tau1_dirr. rewrite /= cfdotBr cfdot_sumr big1 => [|i _]; last first. have oS1eta := coherent_ortho_cycTIiso MtypeP sS10 coh_tau1. by rewrite cfdotBl !oS1eta ?irrS1 ?subrr. rewrite -raddfB Dtau1 ?Zzeta_S1 // Dade_isometry ?A0bridge0 //; last first. exact: cfun_onS sHU_A0 (zcharD1_seqInd_on _ (Zzeta_S1 xi S1xi)). rewrite cfdotBr cfdotC cfdotBr 2?omuS1 // subrr conjC0 !sub0r opprK. by rewrite cfdotBl n1S1 // cfdotS1 // zeta'xi subr0. have S1zetaC: zeta^*%CF \in S1 by rewrite cfAut_seqInd. have Dchi_zetaC: chi = - tau1 zeta^*%CF. by rewrite -Dchi ?(seqInd_conjC_neq _ _ _ S1zeta) ?mFT_odd. suffices S1le2: (size S1 <= size [:: zeta; zeta^*%CF])%N. case: (IHtau1 (dual_iso tau1)); last by rewrite /= -Dchi_zetaC. exact: dual_coherence scohS1 coh_tau1 S1le2. rewrite uniq_leq_size ?seqInd_uniq // => xi S1xi. rewrite !inE -implyNb; apply/implyP=> zeta'xi; apply/eqP. apply: (Zisometry_inj Itau1); rewrite ?mem_zchar ?cfAut_seqInd //. by apply: oppr_inj; rewrite -Dchi. have [[Itau1 Ztau1] Dtau1] := coh_tau1. have tau1_dirr: {in S1, forall xi, tau1 xi \in dirr G}. by move=> xi S1xi; rewrite /= dirrE Ztau1 ?Itau1 ?mem_zchar //= n1S1. have oS1eta i j: {in S1, forall xi, '[tau1 xi, eta_ i j] = 0}. by move=> xi S1xi /=; rewrite (coherent_ortho_cycTIiso _ _ coh_tau1) ?irrS1. pose alpha_ := FTtype345_bridge MtypeP zeta. have A0alpha i j : j != 0 -> alpha_ i j \in 'CF(M, 'A0(M)). by move/supp_FTtype345_bridge->; rewrite ?S1_1. have alpha_S1 i j: {in S1, forall xi, '[alpha_ i j, xi] = n *- (xi == zeta)}. move=> xi S1xi; rewrite /= !cfdotBl !cfdotZl !omu2S1 // mulr0 subrr add0r. by rewrite cfdotS1 // eq_sym mulr_natr. pose beta_ i j := tau (alpha_ i j) - (eta_ i j - eta_ i 0) + n *: zeta1. pose beta := beta_ 0 j1. have betaE i j: j != 0 -> beta_ i j = beta. move=> nz_j; transitivity (beta_ i j1); congr (_ + _); apply/eqP. rewrite eq_sym -subr_eq0 [rhs in _ + rhs]opprD addrACA -opprD subr_eq0. rewrite -[in X in X == _]linearB /= !opprB !addrA !subrK -!/(mu2_ i _). by rewrite [Dade pddM _]prDade_sub_TIirr ?mu2_1 //= deltaZ. rewrite -subr_eq0 !opprD addrACA -3!opprD opprK subr_eq0 addrACA addrA. rewrite -(prDade_sub2_TIirr pddM) -!/(mu2_ _ _) !deltaZ -linearB /=. by rewrite opprB addrA subrK !deltaZ opprD opprK addrACA addrA. pose j := j1. have Rbeta: cfReal beta. rewrite /cfReal eq_sym -subr_eq0 rmorphD/= !rmorphB/= opprB 2!opprD opprB -/j. rewrite 2![(eta_ 0 _)^*%CF]cfAut_cycTIiso -!cycTIirr_aut !aut_Iirr0 -Dade_aut. set k := aut_Iirr conjC j; rewrite -(betaE 0 k) ?aut_Iirr_eq0 // addrACA. rewrite addrC addr_eq0 addrCA subrK opprD opprK Dn raddfZnat -!raddfB /= -Dn. apply/eqP; rewrite (cfConjC_Dade_coherent coh_tau1) ?mFT_odd // -raddfB. rewrite Dtau1 ?Zzeta_S1 ?cfAut_seqInd //= -linearZ scalerBr; congr (tau _). rewrite opprD !rmorphB !deltaZ /= -!prTIirr_aut !aut_Iirr0 addrACA subrr. by rewrite add0r opprK addrC Dn -raddfZnat. have tau_alpha i: tau (alpha_ i j) = eta_ i j - eta_ i 0 - n *: zeta1. set phi := tau (alpha_ i j); pose sum_tau1 := \sum_(xi <- S1) tau1 xi. have A0alpha_j k: alpha_ k j \in 'CF(M, 'A0(M)) by apply: A0alpha. have Zphi: phi \in 'Z[irr G]. by rewrite Dade_vchar // zchar_split vchar_FTtype345_bridge /=. have [Y S1_Y [X [Dphi oYX oXS1]]] := orthogonal_split (map tau1 S1) phi. have [a Za defY]: exists2 a, a \in Cint & Y = a *: sum_tau1 - n *: zeta1. have [a_ Da defY] := orthonormal_span (map_orthonormal Itau1 o1S1) S1_Y. have{} Da: {in S1, forall xi, a_ (tau1 xi) = '[phi, tau1 xi]}. by move=> xi Sxi; rewrite Da Dphi cfdotDl (orthoPl oXS1) ?map_f ?addr0. exists (a_ (tau1 zeta) + n). by rewrite Dn rpredD ?rpred_nat // Da // Cint_cfdot_vchar ?Ztau1 ?Z_S1. rewrite defY big_map scaler_sumr !(bigD1_seq _ S1zeta) ?seqInd_uniq //=. rewrite addrAC scalerDl addrK !(big_seq_cond (predC1 _)) /=; congr (_ + _). apply: eq_bigr => xi /andP[S1xi zeta'xi]; congr (_ *: _); rewrite !Da //. apply: canRL (addNKr _) _; rewrite addrC -opprB -!raddfB Dtau1 ?Zzeta_S1//=. rewrite Dade_isometry //; last first. exact: cfun_onS (zcharD1_seqInd_on _ (Zzeta_S1 _ S1xi)). by rewrite cfdotBr !alpha_S1 // !mulrb eqxx ifN_eq // !(addr0, opprK). have psi_phi: '[psi, phi] = -1 + n. rewrite cfdotC Dade_isometry ?A0bridge0 //. rewrite cfdotBr !cfdotBl deltaZ !cfdotZl n1S1 // mulr1. rewrite !cfdot_prTIirr_red (negPf nz_j1) eqxx !omu2S1 //= cfdotC omuS1 //. by rewrite conjC0 mulr0 opprB !subr0 add0r rmorphD/= rmorphN Dn !rmorph_nat. have{psi_phi} col0_beta: '[eta_col 0, beta] = a. apply/(addIr (-1 + n))/(canRL (addNKr _)). rewrite addrCA addrA addrACA -{}psi_phi Dpsi cfdotBl; congr (_ + _). rewrite -(betaE i j) // cfdotDr !cfdotBr -/phi cfdotZr -!addrA. apply/(canLR (addNKr _)); rewrite addNr !cfdot_suml. rewrite big1 ?add0r ?opprK => [|k _]; last first. by rewrite cfdot_cycTIiso andbC eq_sym (negPf nz_j1). rewrite addrCA big1 ?mulr0 ?add0r => [|k _]; last first. by rewrite cfdotC oS1eta ?conjC0. rewrite addrC (bigD1 i) // cfnorm_cycTIiso /= addKr big1 // => k i'k. by rewrite cfdot_cycTIiso (negPf i'k). rewrite cfdotC Dphi cfdotDl (orthoPl oXS1) ?map_f // addr0. rewrite defY cfdotBl scaler_sumr cfproj_sum_orthonormal //. rewrite cfdotZl Itau1 ?mem_zchar ?n1S1 // mulr1 rmorphB opprD opprK. by rewrite Dn rmorph_nat conj_Cint. have a_even: (2 %| a)%C. have Zbeta: beta \in 'Z[irr G]. rewrite -{1}(betaE i j) // rpredD ?rpredB ?Zphi ?cycTIiso_vchar //. by rewrite Dn rpredZnat // Ztau1 ?mem_zchar. rewrite -col0_beta cfdot_real_vchar_even ?mFT_odd //; first 1 last. split; first by apply/rpred_sum=> k _; apply: cycTIiso_vchar. apply/eqP; rewrite [RHS](reindex_inj (can_inj (@conjC_IirrK _ _))) /=. rewrite rmorph_sum; apply/eq_bigr=> k _ /=. by rewrite cfAut_cycTIiso -cycTIirr_aut aut_Iirr0. have eta00: eta_ 0 0 = 1 by rewrite cycTIirr00 cycTIiso1. rewrite orbC cfdotDl 2!cfdotBl cfdotZl -eta00 oS1eta // mulr0 addr0. rewrite opprB addrC 2!{1}cfdot_cycTIiso (negPf nz_j1) subr0 /= eta00. rewrite Dade_reciprocity // => [|x _ y _]; last by rewrite !cfun1E !inE. rewrite cfRes_cfun1 !cfdotBl deltaZ !cfdotZl -!/(mu2_ 0 _). rewrite -(prTIirr00 ptiWM) !cfdot_prTIirr cfdotC omu2S1 // conjC0 mulr0. by rewrite (negPf nz_j1) add0r subr0 subrr rpred0. have nY: '[Y] = n * a * (a - 2%:R) + n ^+ 2. rewrite defY cfnormD cfnormN !cfnormZ cfdotNr cfdotZr. rewrite cfnorm_map_orthonormal // -Dn Itau1 ?mem_zchar ?n1S1 // mulr1. rewrite scaler_sumr cfproj_sum_orthonormal // rmorphN addrAC. rewrite Dn rmorphM/= !Cint_normK ?rpred_nat // !rmorph_nat conj_Cint // -Dn. by rewrite -mulr2n mulrC mulrA -mulr_natr mulNr -mulrBr. have{a_even} Da: (a == 0) || (a == 2%:R). suffices (b := a - 1): b ^+ 2 == 1. by rewrite -!(can_eq (subrK 1) a) add0r addrK orbC -eqf_sqr expr1n. have S1gt0: (0 < size S1)%N by case: (S1) S1zeta. have: n * b ^+ 2 <= n *+ 3. have: 2%:R + n <= n *+ 3 by rewrite addrC lerD2l lerMn2r Dn ler1n. apply: le_trans; rewrite sqrrB1 -(mulr_natr a) -mulrBr mulrDr mulrA mulr1. rewrite lerD2r -(lerD2r (n ^+ 2 + '[X])) !addrA -nY -cfnormDd //. by rewrite -Dphi norm_FTtype345_bridge ?S1_1 // lerDl cfnorm_ge0. have Zb: b \in Cint by rewrite rpredB ?rpred1 ?Za. have nz_b: b != 0 by rewrite subr_eq0 (memPn _ a a_even) ?(dvdC_nat 2 1). rewrite eq_le sqr_Cint_ge1 {nz_b}//= andbT -Cint_normK // Dn -mulrnA. have /CnatP[m ->] := Cnat_norm_Cint Zb; rewrite -natrX -natrM leC_nat. by rewrite leq_pmul2l // lern1 -ltnS (ltn_sqr m 2) (leq_sqr m 1). have{nY Da} defX: X = eta_ i j - eta_ i 0. have{nY Da} /eqP-nY: '[Y] == n ^+ 2. by rewrite -subr_eq0 nY addrK -mulrA !mulf_eq0 !subr_eq0 Da orbT. have coh_zeta_phi := FTtype345_bridge_coherence _ _ Szeta _ coh_tau1. have:= Dphi; rewrite addrC => /coh_zeta_phi->; rewrite ?S1_1 ?deltaZ //. rewrite defY scaler_sumr big_seq rpredB ?rpred_sum // => [xi Sxi|]. by rewrite rpredZ_Cint ?mem_zchar ?map_f. by rewrite Dn rpredZnat ?mem_zchar ?map_f. have{col0_beta} a0: a = 0. rewrite cfdot_suml big1 // in col0_beta => k _. rewrite -(betaE i j) // /beta_ -/phi Dphi -defX addrK defY subrK. rewrite cfdotZr cfdot_sumr big1_seq ?mulr0 // => xi S1xi. by rewrite cfdotC oS1eta ?conjC0. by rewrite Dphi defY defX a0 ?inE ?eqxx // scale0r sub0r addrC. pose theta := mu_ j - d%:R *: zeta. have /andP/=[red_muj S2muj]: mu_ j \in [predD S2 & irr M]. by rewrite memS2red image_f. have HUtheta: theta \in 'CF(M, HU^#). rewrite cfun_onD1 !cfunE mu_1 ?S1_1 // Dd mulrC natrM subrr eqxx. by rewrite rpredB ?rpredZ ?(seqInd_on _ S1zeta) ?(seqInd_on _ S2muj). have Dtheta: theta = mu_ 0 - zeta + \sum_i alpha_ i j. rewrite !sumrB -scaler_sumr delta1 scale1r. rewrite [X in _ = X]addrC -!addrA -/(mu_ 0); congr (_ + _). rewrite [X in _ = _ + X]addrC !addrA addNr add0r -opprD; congr (- _). rewrite sumr_const nirrW1 -scaler_nat scalerA mulrC. by rewrite divfK ?neq0CG // delta1 addrC scalerBl scale1r subrK. have tau_theta: tau theta = eta_col j - d%:R *: zeta1. pose psi1 i := eta_ i j1 - eta_ i 0 - n *: zeta1. have Dpsi1 i: tau (alpha_ i j) = psi1 i by apply: tau_alpha. rewrite Dtheta [tau _]raddfD raddf_sum (eq_bigr psi1) //= {Dpsi1}/psi1 -/psi. rewrite Dpsi !sumrB [X in X = _]addrC -!addrA; congr (_ + _). rewrite -opprB -opprD -[LHS]opprB -/(eta_col 0) addrA addrK; congr (- _). rewrite sumr_const nirrW1 -scaler_nat scalerA mulrC. by rewrite divfK ?neq0CG // delta1 scalerBl scale1r subrK. have [tau2 coh_tau2] := cohS2. without loss tau2muj: tau2 coh_tau2 / tau2 (mu_ j) = eta_col j; last first. case: FTtype34_noncoherence; rewrite H0_1 -joinGE join1G. have uS12: uniq (S2 ++ S1). by rewrite cat_uniq ?seqInd_uniq ?andbT //=; apply/hasPn. have /perm_coherent: perm_eq (S2 ++ S1) (S_ C); last apply. apply: uniq_perm; rewrite ?seqInd_uniq // => xi; rewrite mem_cat. apply/idP/idP=> [/orP | /seqIndP[i /setDP[kCi k'HUi] ->]]. by case; apply/seqIndS/Iirr_kerDS; rewrite ?joing_subr. by rewrite !mem_seqInd // inE orbC inE kCi k'HUi andbT orbN. move: tau_theta; rewrite -tau2muj // -raddfZnat. apply: (bridge_coherent scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2' _. by rewrite (cfun_onS _ HUtheta) ?setSD // rpredZnat ?Z_S1. move=> IHtau2; apply: (IHtau2 tau2 coh_tau2); have [IZtau2 Dtau2] := coh_tau2. have{IHtau2} /hasP[xi S2xi /=irr_xi]: has [mem irr M] S2. apply/hasPn=> redS2 {tau2 coh_tau2 IZtau2 Dtau2}. have muS2: {subset S2 <= Smu} by move=> xi S2xi; rewrite -memS2red !inE redS2. have [_ [tau2 tau2mu coh_tau2]] := uniform_prTIred_coherent pddM nz_j1. have S2uniform: {subset S2 <= uniform_prTIred_seq pddM j}. move=> _ /muS2/imageP[k nz_k ->]; apply: image_f. by rewrite !inE [_ != 0]nz_k /= !mu_1. apply: (IHtau2 tau2); first exact: subset_coherent_with coh_tau2. have [_ /(_ _ nz_j1) Ez _ _] := FTtype345_constants maxM MtypeP notMtype2. by have:= tau2mu j; rewrite Ez -/delta delta1 scale1r. suffices: '[tau2 (mu_ j), eta_col j] != 0. have:= FTtypeP_coherent_TIred sS20 coh_tau2 irr_xi S2xi S2muj. case=> _ -> [[-> ->] | [-> -> _] /eqP[]]; first by rewrite deltaZ. rewrite -[cyclicTIiso _]/sigma cfdot_sumr big1 ?mulr0 // => i _. rewrite cfdotZl proj_col_eta -(inj_eq irr_inj) conjC_IirrE eq_sym. by rewrite odd_eq_conj_irr1 ?mFT_odd // irr_eq1 (negPf nz_j1) mulr0. pose gamma := xi 1%g *: mu_ j - mu_ j 1%g *: xi. have: '[tau2 gamma, tau theta] != 0. have [Txi Tzeta] := (seqInd_subT S2xi, seqInd_subT S1zeta). have S2gamma: gamma \in 'Z[S2, HU^#] by apply: sub_seqInd_zchar. rewrite Dtau2 ?zcharD1_seqInd //; move/zchar_on in S2gamma. rewrite Dade_isometry ?(cfun_onS sHU_A0) // cfdotBr cfdotZr !cfdotBl !cfdotZl. rewrite cfnorm_prTIred omuS1 // (seqInd_ortho _ _ S2muj) ?(memPn red_muj) //. rewrite (seqInd_ortho _ Txi) ?(memPn (sS1S2' _)) // !(mulr0, subr0) mulf_eq0. by rewrite char1_eq0 ?irrWchar // -cfnorm_eq0 irrWnorm ?oner_eq0 ?neq0CG. apply: contraNneq => o_muj_etaj; rewrite {}tau_theta !{gamma}raddfB subr_eq0 /=. have /CnatP[xi1 ->]: xi 1%g \in Cnat by rewrite Cnat_char1 ?irrWchar. rewrite mu_1 // cfdotZr !cfdotBl !raddfZnat !cfdotZl {}o_muj_etaj cfdot_sumr. have /orthogonalP oS2_S1: orthogonal (map tau2 S2) (map tau1 S1). exact: (coherent_ortho scohM) sS20 coh_tau2 sS10 coh_tau1 sS1S2'. rewrite !oS2_S1 ?map_f // big1 ?(mulr0, subr0) // => k _. exact: (coherent_ortho_cycTIiso _ _ coh_tau2). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10)