proposition: Lemma prDade_subcoherent (G L K H W W1 W2 : {group gT}) A A0 S (defW : W1 \x W2 = W) (ddA : prime_Dade_hypothesis G L K H A A0 defW) (w_ := fun i j => cyclicTIirr defW i j) (sigma := cyclicTIiso ddA) (mu := primeTIred ddA) (delta := fun j => primeTIsign ddA j) (tau := Dade ddA) : let dsw j k := [seq delta j *: sigma (w_ i k) | i : Iirr W1] in let Rmu j := dsw j j ++ map -%R (dsw j (conjC_Iirr j)) in cfConjC_subset S (seqIndD K L H 1) -> ~~ has cfReal S -> {R | [/\ subcoherent S tau R, {in [predI S & irr L] & irr W, forall phi w, orthogonal (R phi) (sigma w)} & forall j, R (mu j) = Rmu j ]}.
proof: Proof. pose mu2 i j := primeTIirr ddA i j. set S0 := seqIndD K L H 1 => dsw Rmu [uS sSS0 ccS] nrS. have nsKL: K <| L by have [[/sdprod_context[]]] := prDade_prTI ddA. have /subsetD1P[sAK notA1]: A \subset K^# by have [_ []] := prDade_def ddA. have [_ _ defA0] := prDade_def ddA. have defSA: 'Z[S, L^#] =i 'Z[S, A]. have sS0A1: {subset S0 <= 'CF(L, 1%g |: A)}. move=> _ /seqIndP[i /setDP[_ kerH'i] ->]; rewrite inE in kerH'i. exact: (prDade_Ind_irr_on ddA) kerH'i. move=> phi; have:= zcharD1_seqInd_Dade nsKL notA1 sS0A1 phi. rewrite !{1}(zchar_split _ A, zchar_split _ L^#) => eq_phiAL. by apply: andb_id2l => /(zchar_subset sSS0) S0phi; rewrite S0phi in eq_phiAL. have Itau: {in 'Z[S, L^#], isometry tau, to 'Z[irr G, G^#]}. apply: sub_iso_to sub_refl (Dade_Zisometry _) => phi; rewrite defSA => SAphi. rewrite defA0; apply: zchar_onS (subsetUl _ _) _ _. by apply: zchar_sub_irr SAphi => ? /sSS0/seqInd_vcharW. have orthoS: pairwise_orthogonal S. exact: sub_pairwise_orthogonal sSS0 uS (seqInd_orthogonal nsKL _). pose S1 := filter (mem (irr L)) S. have sS1S: {subset S1 <= S} by apply/mem_subseq/filter_subseq. have sZS1S: {subset 'Z[S1, L^#] <= 'Z[S, L^#]}. by apply: zchar_subset sS1S; apply: orthogonal_free. have [||R1 cohR1] := irr_subcoherent _ _ (sub_iso_to sZS1S sub_refl Itau). - split=> [|phi|phi]; rewrite ?mem_filter ?filter_uniq //; try case/andP=> //. by case/irrP=> i {2}-> /=/ccS->; rewrite cfConjC_irr. - by apply/hasPn=> phi /sS1S/(hasPn nrS). have{cohR1} [[charS1 _ _] _ _ R1ok R1ortho] := cohR1. pose R phi := oapp Rmu (R1 phi) [pick j | phi == mu j]. have inS1 phi: [pred j | phi == mu j] =1 pred0 -> phi \in S -> phi \in S1. move=> mu'phi Sphi; rewrite mem_filter Sphi andbT /=. have{Sphi} /seqIndP[ell _ Dphi] := sSS0 _ Sphi; rewrite Dphi. have [[j Dell] | [] //] := prTIres_irr_cases ddA ell. by have /=/eqP[] := mu'phi j; rewrite Dphi Dell cfInd_prTIres. have Smu_nz j: mu j \in S -> j != 0. move/(hasPn nrS); apply: contraNneq => ->. by rewrite /cfReal -(prTIred_aut ddA) aut_Iirr0. have oS1sigma phi: phi \in S1 -> orthogonal (R1 phi) (map sigma (irr W)). move=> S1phi; have [zR1 oR1] := R1ok _ S1phi; set psi := _ - _=> Dpsi. suffices o_psi_sigma: orthogonal (tau psi) (map sigma (irr W)). apply/orthogonalP=> aa sw R1aa Wsw; have:= orthoPl o_psi_sigma _ Wsw. have{sw Wsw} /dirrP[bw [lw ->]]: sw \in dirr G. have [_ /(cycTIirrP defW)[i [j ->]] ->] := mapP Wsw. exact: cycTIiso_dirr. have [|ba [la Daa]] := vchar_norm1P (zR1 _ R1aa). by have [_ -> //] := orthonormalP oR1; rewrite eqxx. rewrite Daa cfdotZl !cfdotZr cfdot_irr. case: eqP => [<-{lw} | _ _]; last by rewrite !mulr0. move/(congr1 ( *%R ((-1) ^+ (ba (+) bw))^*)); rewrite mulr0 => /eqP/idPn[]. rewrite mulrA -rmorphM -signr_addb {bw}addbK -cfdotZr -{ba la}Daa. rewrite Dpsi -(eq_bigr _ (fun _ _ => scale1r _)). by rewrite cfproj_sum_orthonormal ?oner_eq0. apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i [j ->]] ->]; rewrite -/w_. pose w1 := #|W1|; pose w2 := #|W2|. have minw_gt2: (2 < minn w1 w2)%N. have [[_ ntW1 _ _] [ntW2 _ _] _] := prDade_prTI ddA. rewrite -(dprod_card defW) oddM => /andP[oddW1 oddW2]. by rewrite leq_min !odd_gt2 ?cardG_gt1. apply: contraTeq (minw_gt2) => ntNC; rewrite -leqNgt. pose NC := cyclicTI_NC ddA. have /andP[/=/irrP[l Dphi] Sphi]: phi \in [predI irr L & S]. by rewrite mem_filter in S1phi. have Zpsi: psi \in 'Z[S, L^#]. rewrite sub_aut_zchar ?mem_zchar_on ?orthogonal_free ?ccS ?cfun_onG //. by move=> ? /sSS0/seqInd_vcharW. have NCpsi_le2: (NC (tau psi) <= 2)%N. have{Itau} [Itau Ztau] := Itau. suff: '[tau psi] <= 2%:R by apply: cycTI_NC_norm; apply: zcharW (Ztau _ _). rewrite Itau // cfnormBd; first by rewrite cfnorm_conjC Dphi cfnorm_irr. have /pairwise_orthogonalP[_ -> //] := orthoS; first exact: ccS. by rewrite eq_sym (hasPn nrS). apply: leq_trans (NCpsi_le2). have: (0 < NC (tau psi) < 2 * minn w1 w2)%N. rewrite -(subnKC minw_gt2) (leq_ltn_trans NCpsi_le2) // andbT lt0n. by apply/existsP; exists (i, j); rewrite /= topredE inE. apply: cycTI_NC_minn (ddA) _ _ => x Vx. rewrite Dade_id; last by rewrite defA0 inE orbC mem_class_support. rewrite defSA in Zpsi; rewrite (cfun_on0 (zchar_on Zpsi)) // -in_setC. by apply: subsetP (subsetP (prDade_supp_disjoint ddA) x Vx); rewrite setCS. exists R; split=> [|phi w S1phi irr_w|j]; first 1 last. - rewrite /R; case: pickP => [j /eqP Dphi | _ /=]. by case/nandP: S1phi; right; rewrite /= Dphi (prTIred_not_irr ddA). apply/orthoPr=> aa R1aa; rewrite (orthogonalP (oS1sigma phi _)) ?map_f //. by rewrite mem_filter andbC. - by rewrite /R; case: pickP => /= [k /eqP/(prTIred_inj ddA)-> | /(_ j)/eqP]. have Zw i j: w_ i j \in 'Z[irr W] by apply: irr_vchar. have{oS1sigma} oS1dsw psi j: psi \in S1 -> orthogonal (R1 psi) (dsw _ j). move/oS1sigma/orthogonalP=> opsiW. apply/orthogonalP=> aa _ R1aa /codomP[i ->]. by rewrite cfdotZr opsiW ?map_f ?mem_irr ?mulr0. have odsw j1 j2: j1 != j2 -> orthogonal (dsw _ j1) (dsw _ j2). move/negPf=> j2'1; apply/orthogonalP=> _ _ /codomP[i1 ->] /codomP[i2 ->]. by rewrite cfdotZl cfdotZr (cfdot_cycTIiso ddA) j2'1 andbF !mulr0. split=> // [|phi Sphi|phi xi Sphi Sxi]. - by split=> // phi /sSS0; apply: seqInd_char. - rewrite /R; case: pickP => [j /eqP Dphi /= | /inS1/(_ Sphi)/R1ok//]. have nz_j: j != 0 by rewrite Smu_nz -?Dphi. have [Isig Zsig]: {in 'Z[irr W], isometry sigma, to 'Z[irr G]}. exact: cycTI_Zisometry. split=> [aa | |]. - rewrite mem_cat -map_comp. by case/orP=> /codomP[i ->]; rewrite ?rpredN rpredZsign Zsig. - rewrite orthonormal_cat orthogonal_oppr odsw ?andbT; last first. rewrite -(inj_eq (prTIred_inj ddA)) (prTIred_aut ddA) -/mu -Dphi. by rewrite eq_sym (hasPn nrS). suffices oNdsw k: orthonormal (dsw j k). by rewrite map_orthonormal ?oNdsw //; apply: in2W; apply: opp_isometry. apply/orthonormalP; split=> [|_ _ /codomP[i1 ->] /codomP[i2 ->]]. rewrite map_inj_uniq ?enum_uniq // => i1 i2 /(can_inj (signrZK _))/eqP. by rewrite (cycTIiso_eqE ddA) eqxx andbT => /eqP. rewrite cfdotZl cfdotZr rmorph_sign signrMK (cfdot_cycTIiso ddA). by rewrite -(cycTIiso_eqE ddA) (inj_eq (can_inj (signrZK _))). have [Tstruct [tau1 Dtau1 [_ Dtau]]] := uniform_prTIred_coherent ddA nz_j. have{Tstruct} [/orthogonal_free freeT _ ccT _ _] := Tstruct. have phi1c: (phi 1%g)^* = phi 1%g := conj_Cnat (Cnat_seqInd1 (sSS0 _ Sphi)). rewrite -[tau _]Dtau; last first. rewrite zcharD1E !cfunE/= phi1c subrr Dphi eqxx andbT. by rewrite rpredB ?mem_zchar ?ccT ?image_f ?inE // nz_j eqxx. rewrite linearB Dphi -(prTIred_aut ddA) !Dtau1 -/w_ -/sigma -/(delta j). by rewrite big_cat /= !big_map !raddf_sum. rewrite /R; case: pickP => [j1 /eqP Dxi | /inS1/(_ Sxi)S1xi]; last first. case: pickP => [j2 _ _ | /inS1/(_ Sphi)S1phi]; last exact: R1ortho. by rewrite orthogonal_catr orthogonal_oppr !oS1dsw. case: pickP => [j2 /eqP Dphi | /inS1/(_ Sphi)S1phi _]; last first. by rewrite orthogonal_sym orthogonal_catr orthogonal_oppr !oS1dsw. case/andP=> /and3P[/= /eqP o_xi_phi /eqP o_xi_phi'] _ _. have /eqP nz_xi: '[xi] != 0 := cfnorm_seqInd_neq0 nsKL (sSS0 _ Sxi). have [Dj1 | j2'1] := eqVneq j1 j2. by rewrite {2}Dxi Dj1 -Dphi o_xi_phi in nz_xi. have [Dj1 | j2c'1] := eqVneq j1 (conjC_Iirr j2). by rewrite {2}Dxi Dj1 /mu (prTIred_aut ddA) -/mu -Dphi o_xi_phi' in nz_xi. rewrite orthogonal_catl orthogonal_oppl !orthogonal_catr !orthogonal_oppr. by rewrite !odsw ?(inv_eq (@conjC_IirrK _ _)) ?conjC_IirrK. 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)