proposition: Theorem uniform_prTIred_coherent k (calT := uniform_prTIred_seq ptiWL k) : k != 0 -> [/\ pairwise_orthogonal calT, ~~ has cfReal calT, cfConjC_closed calT, 'Z[calT, L^#] =i 'Z[calT, A] & exists2 psi, psi != 0 & psi \in 'Z[calT, A]] /\ (exists2 tau1 : {linear 'CF(L) -> 'CF(G)}, forall j, tau1 (mu_ j) = delta_ k *: (\sum_i sigma (w_ i j)) & {in 'Z[calT], isometry tau1, to 'Z[irr G]} /\ {in 'Z[calT, L^#], tau1 =1 tau}).
proof: Proof. have uniqT: uniq calT by apply/dinjectiveP; apply: in2W; apply: prTIred_inj. have sTmu: {subset calT <= codom mu_} by apply: image_codom. have oo_mu: pairwise_orthogonal (codom mu_). apply/pairwise_orthogonalP; split=> [|_ _ /codomP[j1 ->] /codomP[j2 ->]]. apply/andP; split; last by apply/injectiveP; apply: prTIred_inj. by apply/codomP=> [[i /esym/eqP/idPn[]]]; apply: prTIred_neq0. by rewrite cfdot_prTIred; case: (j1 =P j2) => // -> /eqP. have real'T: ~~ has cfReal calT. by apply/hasPn=> _ /imageP[j /andP[nzj _] ->]; apply: prTIred_not_real. have ccT: cfConjC_closed calT. move=> _ /imageP[j Tj ->]; rewrite -prTIred_aut image_f // inE aut_Iirr_eq0. by rewrite prTIred_aut cfunE/= conj_Cnat ?Cnat_char1 ?prTIred_char. have TonA: 'Z[calT, L^#] =i 'Z[calT, A]. have A'1: 1%g \notin A by apply: contra (subsetP sAA0 _) _; have [] := ddA0. move=> psi; rewrite zcharD1E -(setU1K A'1) zcharD1; congr (_ && _). apply/idP/idP; [apply: zchar_trans_on psi => psi Tpsi | exact: zcharW]. have [j /andP[nz_j _] Dpsi] := imageP Tpsi. by rewrite zchar_split mem_zchar // Dpsi prDade_TIred_on. move=> nzk; split. split=> //; first exact: sub_pairwise_orthogonal oo_mu. have Tmuk: mu_ k \in calT by rewrite image_f // inE nzk /=. exists ((mu_ k)^*%CF - mu_ k); first by rewrite subr_eq0 (hasPn real'T). rewrite -TonA -rpredN opprB sub_aut_zchar ?zchar_onG ?mem_zchar ?ccT //. by move=> _ /mapP[j _ ->]; rewrite char_vchar ?prTIred_char. pose f0 j := delta_ k *: (\sum_i eta_ i j); have in_mu := codom_f mu_. pose f1 psi := f0 (iinv (valP (insigd (in_mu k) psi))). have f1mu j: f1 (mu_ j) = f0 j. have in_muj := in_mu j. rewrite /f1 /insigd /insubd /= insubT /=; [idtac]. by rewrite iinv_f //; apply: prTIred_inj. have iso_f1: {in codom mu_, isometry f1, to 'Z[irr G]}. split=> [_ _ /codomP[j1 ->] /codomP[j2 ->] | _ /codomP[j ->]]; last first. by rewrite f1mu rpredZsign rpred_sum // => i _; apply: cycTIiso_vchar. rewrite !f1mu cfdotZl cfdotZr rmorph_sign signrMK !cfdot_suml. apply: eq_bigr => i1 _; rewrite !cfdot_sumr; apply: eq_bigr => i2 _. by rewrite cfdot_cycTIiso cfdot_prTIirr. have [tau1 Dtau1 Itau1] := Zisometry_of_iso (orthogonal_free oo_mu) iso_f1. exists tau1 => [j|]; first by rewrite Dtau1 ?codom_f ?f1mu. split=> [|psi]; first by apply: sub_iso_to Itau1 => //; apply: zchar_subset. rewrite zcharD1E => /andP[/zchar_expansion[//|z _ Dpsi] /eqP psi1_0]. rewrite -[psi]subr0 -(scale0r (mu_ k)) -(mul0r (mu_ k 1%g)^-1) -{}psi1_0. rewrite {psi}Dpsi sum_cfunE mulr_suml scaler_suml -sumrB !raddf_sum /=. apply: eq_big_seq => _ /imageP[j /andP[nzj /eqP eq_mujk_1] ->]. rewrite cfunE eq_mujk_1 mulfK ?prTIred_1_neq0 // -scalerBr !linearZ /=. congr (_ *: _); rewrite {z}linearB !Dtau1 ?codom_f // !f1mu -scalerBr -!sumrB. rewrite !linear_sum; apply: eq_bigr => i _ /=. have{eq_mujk_1} eq_mu2ijk_1: mu2_ i j 1%g = mu2_ i k 1%g. by apply: (mulfI (neq0CG W1)); rewrite !prTIirr_1 -!prTIred_1. by rewrite -(prDade_TIsign_eq eq_mu2ijk_1) prDade_sub_TIirr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)